[ICFP'23] Verifying Reliable Network Components in a Distributed Separation Logic with Dep...

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols (Video, ICFP 2023) Léon Gondelman, Jonas Kastberg Hinrichsen, Mário Pereira, Amin Timany, and Lars Birkedal (Aarhus University, Denmark; Aarhus University, Denmark; NOVA-LINCS, Portugal / NOVA School of Sciences and Tecnhology, Portugal; Aarhus University, Denmark; Aarhus University, Denmark) Abstract: We present a foundationally verified implementation of a reliable communication library for asynchronous client-server communication, and a stack of formally verified components on top thereof. Our library is implemented in an OCaml-like language on top of UDP and features characteristic traits of existing protocols, such as a simple handshaking protocol, bidirectional channels, and retransmission/acknowledgement mechanisms. We verify the library in the Aneris distributed separation logic using a novel proof pattern---dubbed the session escrow pattern---based on the existing escrow proof pattern and the so-called dependent separation protocols, which hitherto have only been used in a non-distributed concurrent setting. We demonstrate how our specification of the reliable communication library simplifies formal reasoning about applications, such as a remote procedure call library, which we in turn use to verify a lazily replicated key-value store with leader-followers and clients thereof. Our development is highly modular---each component is verified relative to specifications of the components it uses (not the implementation). All our results are formalized in the Coq proof assistant. Article: https://doi.org/10.1145/3607859 Supplementary archive: https://doi.org/10.5281/zenodo.8121688 (Badges: Artifacts Available, Artifacts Evaluated — Reusable) ORCID: https://orcid.org/0000-0001-8262-6397, https://orcid.org/0000-0001-6143-9031, https://orcid.org/0000-0002-7048-9425, https://orcid.org/0000-0002-2237-851X, https://orcid.org/0000-0003-1320-0098 Video Tags: Distributed systems, separation logic, refinement, higher-order logic, concurrency, formal verification, icfp23main-p142-p, doi:10.1145/3607859, doi:10.5281/zenodo.8121688, orcid:0000-0001-8262-6397, orcid:0000-0001-6143-9031, orcid:0000-0002-7048-9425, orcid:0000-0002-2237-851X, orcid:0000-0003-1320-0098, Artifacts Available, Artifacts Evaluated — Reusable Presentation at the ICFP 2023 conference, September 4–9, 2023, https://icfp23.sigplan.org/ Sponsored by ACM SIGPLAN, https://www.sigplan.org/