Concepedia

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

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, William Mansky, Benjamin C. Pierce, Steve Zdancewic

DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2021 · 20 citations · 0 references

DOI Full text

Open access

Concepts

ComputingComputer ScienceComputer SystemsCryptographyFormal MethodsOperating SystemsApplication Programming InterfacesHttp ProtocolInternet Protocol SuiteProtocol VerificationWeb AuthenticationWeb ProtocolsFormal Verification Tools For Cryptographic ProtocolsKernel-user Space BoundaryRefinementSpecification-based Security

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.