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

Verifying an HTTP Key-Value Server with Interaction Trees and VST
复制标题

DOI：
10.4230/lipics.itp.2021.32
复制
发表时间：
2021
期刊：
--
影响因子：
--
通讯作者：
Hengchu Zhang;Wolf Honoré;Nicolas C. H. Koh;Yao Li;Yishuai Li;Li-yao Xia;Lennart Beringer;William Mansky;B. Pierce;Steve Zdancewic
Hengchu Zhang;Wolf Honoré;Nicolas C. H. Koh;Yao Li;Yishuai Li;Li-yao Xia;Lennart Beringer;William Mansky;B. Pierce;Steve Zdancewic
中科院分区：
其他
文献类型：
--
作者：
Hengchu Zhang;Wolf Honoré;Nicolas C. H. Koh;Yao Li;Yishuai Li;Li-yao Xia;Lennart Beringer;William Mansky;B. Pierce;Steve Zdancewic

文献摘要

被引文献

相似文献

我们提出了一个网络键值服务器，用 C 实现并在 Coq 中进行正式验证。服务器使用 HTTP/1.1 协议的子集与客户端进行交互，并使用交互树和已验证软件工具链进行指定和验证。该代码库包括一个可重用且经过充分验证的 C 字符串库，该库提供 17 个标准 POSIX 字符串函数和 17 个通用非 POSIX 字符串函数。对于 KVServer 套接字系统调用，我们在用户空间级别和 CertiKOS 内核空间级别的规范之间建立了细化关系。
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.