Networked Server Verification Using Interaction Trees

 
From C
to Interaction Trees
 
Specifying, Testing and Verifying a Networked Server
 
January 14, 2019
 (CPP)
 
Nicolas Koh, Yao Li, Yishuai Li, 
Li-yao Xia
Lennart Beringer, Wolf Honoré, William Mansky
Benjamin C. Pierce, Steve Zdancewic
 
 
1
Verification from RFCs to transistors
Application
OS
Hardware
01011...
2
 
 
… and test!
 
More projects at deepspec.org…
 
One theorem to verify…
 
Towards a verified web server
HTTP Server
OS
Hardware
 
01011...
 
3
 
 
Towards a verified web server
Swap Server
OS
Hardware
 
01011...
 
4
 
 
Today: a simplified server
 
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
Server
Client 1
 
Cat
 
Dog
 
Bat
 
Cat
Client 2
Client 3
 
Elk
 
Dog
6
 
Cat
 
Bat
 
Dog
 
Elk
Swap server: in the real world
Server
Clients
/
Tester
 
Cat
 
Dog
 
Dog
 
Bat
 
Elk
7
 
Messages on different
connections can be
reordered
Messages can be
delayed indefinitely
Network refinement
8
Specification
Observable behavior
by clients
 
Network semantics
 
I
n
e
t
w
o
r
k
-
r
e
f
i
n
e
s
Adaptation of Observational refinement/Linearizability
Implementation
Observable behavior
by clients
 
Network semantics
Overview:
 
proof architecture
CertiKOS
Socket API
Server implementation
Specification*
*: concepts defined in the paper
9
Written in Coq
Written in C
Overview:
 
proof architecture
CertiKOS
Socket API
Server implementation
Linear Specification*
Implementation model*
CertiKOS-level
Socket spec.*
VST-level
Socket spec.*
 
implements
 
validates*
refines*
network-refines*
10
assumed by
 
*: concepts defined in the paper
Written in Coq
Written in C
A unifying specification language
CertiKOS
Socket API
Server implementation
Linear Specification*
Implementation model*
CertiKOS-level
Socket spec.*
VST-level
Socket spec.*
implements
validates*
refines*
network-refines*
11
network-refines*
assumed by
 
*: concepts defined in the paper
Written in Coq
Written in C
testing
Different abstraction levels
Different spec. styles
 
Interaction trees
Interaction trees: example
ReadBit
WriteBit 0
ReadBit
Ret
 1
b2 : bit
tt
Ret
 b2
0
1
 
Shorthand notation for two or more
branches
12
(aka. Free monads)
 
One branch for each possible result
Inductive 
ioE
 : Type -> Type :=
| ReadBit  : 
ioE 
bit
| WriteBit : bit -> 
ioE 
unit
.
 
Type of effects 
ioE
:
 
Result type
Interaction trees: definition
 
CoInductive 
itree 
(
E
 : Type -> Type) (R : Type) :
Type :=
Vis 
: 
 
Y
E
 
-> (
Y
 -> 
itree 
E R) -> 
itree 
E R
| 
Ret 
: R -> 
itree 
E R
| 
Tau 
: 
itree 
E R -> 
itree 
E R
.
13
 
Effect
 
Continuation
(aka. Free monads)
 
Type of effects
 (e.g.,
 
ioE
)
 
Type of results
 
A unifying specification language
CertiKOS
Socket API
Server implementation
Linear Specification*
Implementation model*
CertiKOS-level
Socket spec.*
VST-level
Socket spec.*
 
implements
 
validates*
refines*
network-refines*
14
network-refines*
assumed by
 
 
*: concepts defined in the paper
 
Written in Coq
 
Written in C
testing
Different abstraction levels
Different spec. styles
 
Interaction trees
 
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
 
Overview:
 
proof architecture
CertiKOS
Socket API
Server implementation
Linear Specification*
Implementation model*
CertiKOS-level
Socket spec.*
VST-level
Socket spec.*
 
implements
 
validates*
refines*
network-refines*
 
16
network-refines*
assumed by
 
 
*: concepts defined in the paper
 
Written in Coq
 
Written in C
 
testing
 
Interaction trees
Refinement: from C to ITrees
17
 
{ 
ITree
(msg <- Recv c ;;
        Send c msg ;;
        t) * … }
    
 recv(c, buf, len); 
.
    
 send(c, buf, len); 
.
{ 
ITree
(t) * … }
Hoare triple:
{ pre1 * … * preN }
 C_program 
{ post1 * … * postN }
Separating conjunction
Assertions on C memory
 
Implementation model (itree)
 
C implementation
 
Interactions 
allowed
 by
the environment
Simplified triples (see paper)
 
Example of a networked C program with its implementation model:
 
{ 
ITree
(
impl_model
) * … }
 C_program 
{ … }
The Swap server correctness theorem
18
Theorem
 correct_server :
  
exists
 
impl_model
,
            refines 
C_prog
 
impl_model
 /\
    network_refines 
impl_model 
linear_spec
.
 
{ 
ITree
(
impl_model
) }
 C_prog 
{ … }
 
The Swap server correctness theorem
 
19
 
Theorem
 correct_server :
  
exists
 
impl_model
,
            refines 
C_prog
 
impl_model
 /\
    network_refines 
impl_model 
linear_spec
.
 
{ 
ITree
(
impl_model
) }
 C_prog 
{ … }
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
20
Scale up:
Swap server ->
HTTP Server
Complete
connection
Improve proof
and testing
techniques
New library
 
https://github.com/DeepSpec/InteractionTrees
Add more interfaces:
filesystem, encryption…
Slide Note

Our work towards verifying a networked server

Embed
Share

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.


Uploaded on Jul 30, 2024 | 0 Views


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


  1. 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

  2. Verification from RFCs to transistors Application One theorem to verify OS and test! More projects at deepspec.org Hardware 01011... 2

  3. Towards a verified web server HTTP Server OS Hardware 01011... 3

  4. Towards a verified web server Swap Server Today: a simplified server OS Hardware 01011... 4

  5. 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

  6. Swap server specification Cat Bat Client 1 Bat Cat Dog Elk Dog Server Client 2 Cat Elk Client 3 Dog 6

  7. 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

  8. 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

  9. *: concepts defined in the paper Overview: proof architecture Specification* Written in Coq Written in C Socket API Server implementation CertiKOS 9

  10. *: 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

  11. 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

  12. 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

  13. 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

  14. 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

  15. 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

  16. 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

  17. 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

  18. 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

  19. 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

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#