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).
12/04/2023 14:00
Software Systems
I am currently a post-doc researcher at Aarhus University, Denmark where I am working on modular specification and verification of distributed systems, focusing on problems such as distributed causal memory, partition-tolerant distributed systems, CRDTs among others. Previously, I was a post-doc at iCIS in Nijmegen, Netherlands, where I was working on formalisation of C language in Coq proof assistant with focus on building a program logic that comes with a semi-automated reasoning about non-determinism in C expressions. Before my post-docs, I defended my PhD at Université Paris Saclay in France. My PhD thesis entitled "A Pragmatic Type System for Deductive Verification" explored solutions that a type system based approach can bring to the deductive verification. It formalises some aspects of the type system of Why3 such as ghost code and static control of aliases.
