Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

@article{10.1145/3607859,
 author = {Gondelman, L\'{e}on and Hinrichsen, Jonas Kastberg and Pereira, M\'{a}rio and Timany, Amin and Birkedal, Lars},
 title = {Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols},
 year = {2023},
 issue_date = {August 2023},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 volume = {7},
 number = {ICFP},
 url = {https://doi.org/10.1145/3607859},
 doi = {10.1145/3607859},
 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.},
 journal = {Proc. ACM Program. Lang.},
 month = {aug},
 articleno = {217},
 numpages = {31},
 keywords = {concurrency, refinement, separation logic, formal verification, Distributed systems, higher-order logic}
}