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

2021/01/01 by Hengchu Zhang, Wolf Honoré, Nicolas Koh +7 · 1 voice · 1 citation
Computer Science · #Network Security and Intrusion Detection #Security and Verification in Computing #Service-Oriented Architecture and Web Services

paper · doi:10.4230/lipics.itp.2021.32

openalex publication_date 2021/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants

Discussions

• Verifying an HTTP Key-Value Server with Interaction Trees and VST [hn, 2 points, 0 comments]

Related

• From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
• Extending the Trusted Path in Client-Server Interaction
• Secure Shell (SSH): Public Key Authentication over Hypertext Transfer Protocol (HTTP)
• Verification of a Cryptographic Primitive
• Pretty-Simple Password-Authenticated Key-Exchange Protocol