Networked Server Verification Using Interaction Trees
This paper explores the process of specifying, testing, and verifying a networked server from C to interaction trees. It discusses the main contributions, including verifying a networked C program using VST and running in CertiKOS. The paper also delves into swap server specifications, observable behaviors, and network refinements in the context of server implementations. Written in Coq and C, the paper emphasizes the importance of validation and implementation models in server architecture.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Specifying, Testing and Verifying a Networked Server From C to Interaction Trees Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia Lennart Beringer, Wolf Honor , William Mansky Benjamin C. Pierce, Steve Zdancewic January 14, 2019 (CPP) 1
Verification from RFCs to transistors Application One theorem to verify OS and test! More projects at deepspec.org Hardware 01011... 2
Towards a verified web server HTTP Server OS Hardware 01011... 3
Towards a verified web server Swap Server Today: a simplified server OS Hardware 01011... 4
Main contributions Verifying a networked C program using VST, which can run in CertiKOS Specification describes what a client can observe over the network Testable specification, using QuickChick 5
Swap server specification Cat Bat Client 1 Bat Cat Dog Elk Dog Server Client 2 Cat Elk Client 3 Dog 6
Swap server: in the real world Cat Messages on different connections can be reordered Messages can be delayed indefinitely Dog Clients / Tester Bat Server Elk Dog 7
Network refinement Observable behavior by clients Specification Network semantics I network network- -refines refines Observable behavior by clients Implementation Network semantics Adaptation of Observational refinement/Linearizability 8
*: concepts defined in the paper Overview: proof architecture Specification* Written in Coq Written in C Socket API Server implementation CertiKOS 9
*: concepts defined in the paper Overview: proof architecture Linear Specification* VST-level Socket spec.* network-refines* validates* Implementation model* CertiKOS-level Socket spec.* refines* assumed by Written in Coq implements Written in C Socket API Server implementation CertiKOS 10
Interaction trees *: concepts defined in the paper A unifying specification language Different spec. styles Different abstraction levels Linear Specification* testing VST-level Socket spec.* network-refines* validates* Implementation model* CertiKOS-level Socket spec.* refines* network-refines* assumed by Written in Coq implements Written in C Socket API Server implementation CertiKOS 11
Interaction trees: example (aka. Free monads) One branch for each possible result ReadBit 0 1 WriteBit 0 ReadBit Shorthand notation for two or more branches tt b2 : bit Ret 1 Ret b2 Type of effects ioE: Inductive ioE : Type -> Type := | ReadBit : ioE bit | WriteBit : bit -> ioE unit . Result type 12
Interaction trees: definition (aka. Free monads) Type of effects (e.g.,ioE) Type of results CoInductive itree (E : Type -> Type) (R : Type) : Type := | Vis : Y, E Y -> (Y -> itree E R) -> itree E R | Ret : R -> itree E R | Tau : itree E R -> itree E R . Effect Continuation 13
Interaction trees *: concepts defined in the paper A unifying specification language Different spec. styles Different abstraction levels Linear Specification* testing VST-level Socket spec.* network-refines* validates* Implementation model* CertiKOS-level Socket spec.* refines* network-refines* assumed by Written in Coq implements Written in C Socket API Server implementation CertiKOS 14
The Swap server linear specification CoFixpoint loop (open_conns : list conns) (last_msg : bytes) : itree serverE unit := c <- choose open_conns ;; new_msg <- recv_msg c ;; send_msg c last_msg ;; loop open_conns new_msg. Simplified version (see paper) 15
Interaction trees *: concepts defined in the paper Overview: proof architecture Linear Specification* testing VST-level Socket spec.* network-refines* validates* Implementation model* CertiKOS-level Socket spec.* refines* network-refines* assumed by Written in Coq implements Written in C Socket API Server implementation CertiKOS 16
Refinement: from C to ITrees Hoare triple: { pre1 * * preN } C_program { post1 * * postN } Separating conjunction Interactions allowed by the environment Assertions on C memory { ITree(impl_model) * } C_program { } Example of a networked C program with its implementation model: { ITree(msg <- Recv c ;; Send c msg ;; t) * } recv(c, buf, len); . send(c, buf, len); . { ITree(t) * } Implementation model (itree) C implementation Simplified triples (see paper) 17
The Swap server correctness theorem { ITree(impl_model) } C_prog { } Theorem correct_server : exists impl_model, refines C_prog impl_model /\ network_refines impl_model linear_spec. I 18
Complete connection Summary and next steps Verifying a networked C program using VST, which can run in CertiKOS The specification describes a client can observe over the network The specification is testable, using QuickChick and Interaction trees Scale up: Swap server -> HTTP Server Improve proof and testing techniques Add more interfaces: filesystem, encryption New library https://github.com/DeepSpec/InteractionTrees 20
