Verifying an HTTP Key-Value Server with Interaction Trees and VST

Authors :: Hengchu Zhang and Wolf Honoré and Nicolas Koh and Yao Li and Yishuai Li and Li-Yao Xia and Lennart Beringer and William Mansky and Benjamin Pierce and Steve Zdancewic
Zhang, Hengchu
Honoré, Wolf
Koh, Nicolas
Li, Yao
Li, Yishuai
Xia, Li-Yao
Beringer, Lennart
Mansky, William
Pierce, Benjamin
Zdancewic, Steve
Hengchu Zhang and Wolf Honoré and Nicolas Koh and Yao Li and Yishuai Li and Li-Yao Xia and Lennart Beringer and William Mansky and Benjamin Pierce and Steve Zdancewic
Zhang, Hengchu
Honoré, Wolf
Koh, Nicolas
Li, Yao
Li, Yishuai
Xia, Li-Yao
Beringer, Lennart
Mansky, William
Pierce, Benjamin
Zdancewic, Steve
Publication Year :: 2021
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.

Full Text Access

Tools