Verifying an HTTP key-value server with interaction trees and VST
The 12th Conference on Interactive Theorem Proving, 2021•research.ed.ac.uk
We present a networked key-value server, implemented in C and formally verified in Coq.
The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and
verified using interaction trees and the Verified Software Toolchain. The codebase includes
a reusable and fully verified C string library that provides 17 standard POSIX string functions
and 17 general purpose non-POSIX string functions. For the KVServer socket system calls,
we establish a refinement relation between specifications at user-space level and at …
The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and
verified using interaction trees and the Verified Software Toolchain. The codebase includes
a reusable and fully verified C string library that provides 17 standard POSIX string functions
and 17 general purpose non-POSIX string functions. For the KVServer socket system calls,
we establish a refinement relation between specifications at user-space level and at …
Abstract
We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchain. The codebase includes a reusable and fully verified C string library that provides 17 standard POSIX string functions and 17 general purpose non-POSIX string functions. For the KVServer socket system calls, we establish a refinement relation between specifications at user-space level and at CertiKOS kernel-space level.
research.ed.ac.uk
以上显示的是最相近的搜索结果。 查看全部搜索结果