Tue 17 Jan 2023 14:00 - 14:22 at Studio 1 - Applications Chair(s): Yoonseung Kim

FastVer (Arasu et al. SIGMOD’21) is a protocol that uses a variety of memory-checking techniques to monitor the integrity of key-value stores with only a modest runtime cost. Arasu et al. formalize the high-level \emph{design} of FastVer in the F* proof assistant and prove it correct. However, their formalization did not yield a provably correct \emph{implementation}—FastVer is implemented in unverified C++ code.

In this work, we present FastVer2, a low-level, concurrent implementation of FastVer in Steel, an F* DSL based on concurrent separation logic that produces C code, and prove it correct with respect to Arasu et al.’s high-level specification. Our proof is the first end-to-end system proven using Steel, and in doing so we contribute new ghost-state constructions for reasoning about monotonic state. Our proof also uncovered a few bugs in the implementation of FastVer.

We evaluate FastVer2 by comparing it against FastVer. Although our verified monitor is slower in absolute terms than the unverified code, its performance also scales linearly with the number of cores, yielding a throughput of more that 10M op/sec. We identify several opportunities for performance improvement and expect to address these in the future.

Tue 17 Jan

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:30
ApplicationsCPP at Studio 1
Chair(s): Yoonseung Kim Yale University
14:00
22m
Talk
FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Storesremote presentation
CPP
Arvind Arasu Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Aymeric Fromherz Inria, Kesha Hietala University of Maryland, Bryan Parno Carnegie Mellon University, Ravi Ramamurthy Microsoft Research
14:22
22m
Talk
Formalising Decentralised Exchanges in Coq
CPP
Eske Hoy Nielsen Aarhus University, Danil Annenkov Concordium, Bas Spitters Concordium Blockchain Research Center, Aarhus University
14:45
22m
Talk
Semantics of Probabilistic Programs using S-Finite Kernels in Coq
CPP
Reynald Affeldt National Institute of Advanced Industrial Science and Technology (AIST), Cyril Cohen Inria, Ayumu Saito Tokyo Institute of Technology
15:07
22m
Talk
Formalising Sharkovsky's Theorem (Proof Pearl)
CPP
Bhavik Mehta University of Cambridge