Detail

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

In this talk we will take a look on a foundationally verified implementation of a reliable communication library for asynchronous client-server communication,
and a stack of formally verified components on top thereof. The library is implemented in OCaml on top of UDP and features characteristic traits of
existing communication protocols, such as a simple handshaking protocol, bidirectional channels, and retransmission/acknowledgement mechanisms.
We will see how this library is verified and specified 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. To verify OCaml programs, we have implemented a simple compiler that translates programs written in a subset of OCaml to AnerisLang, the formally defined
programming language that Aneris is proved sound for. I will show how our specification of the reliable communication library simplifies formal reasoning
about applications, such as a remote procedure call library, which in turn is used to verify a lazily replicated key-value store with leader-followers and some clients
thereof. Importantly, the development is highly modular — each component is verified relative to specifications of the components it uses (not the implementation).