A carregar...
Publicação
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 393.38 KB | Adobe PDF |
Orientador(es)
Resumo(s)
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.
Descrição
Publisher Copyright: © 2023 Owner/Author. We are grateful to Chet Murthy for helpful discussions. This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.
Palavras-chave
concurrency Distributed systems formal verification higher-order logic refinement separation logic Software Safety, Risk, Reliability and Quality