Authors

Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chanhee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon and Bryan Parno

Venue

Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles (SOSP '24)

Links

[ .doi ] [ .pdf ] [ .bib ]

Abstract

Bibtex

@inproceedings{Lattuada:2024:VPF,
 abstract = {Formal verification is a promising approach to eliminate bugs at compile time, before they ship. Indeed, our community has verified a wide variety of system software. However, much of this success has required heroic developer effort, relied on bespoke logics for individual domains, or sacrificed expressiveness for powerful proof automation.Building on prior work on Verus, we aim to enable faster, cheaper verification of rich properties for realistic systems. We do so by integrating and optimizing the best choices from prior systems, tuning our design to overcome barriers encountered in those systems, and introducing novel techniques.We evaluate Verus's effectiveness with a wide variety of case-study systems, including distributed systems, an OS page table, a library for NUMA-aware concurrent data structure replication, a crash-safe storage system, and a concurrent memory allocator, together comprising 6.1K lines of implementation and 31K lines of proof. Verus verifies code 3--61\texttimes{} faster and with less effort than the state of the art.Our results suggest that Verus offers a platform for exploring the next frontiers in system-verification research. Because Verus builds on Rust, Verus is also positioned for wider use in production by developers who have already adopted Rust in the pursuit of more robust systems.},
 address = {New York, NY, USA},
 author = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jacob R. and Padon, Oded and Parno, Bryan},
 booktitle = {Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles},
 doi = {10.1145/3694715.3695952},
 id = {Lattuada:2024:VPF},
 isbn = {9798400712517},
 location = {Austin, TX, USA},
 numpages = {17},
 pages = {438–454},
 publisher = {Association for Computing Machinery},
 series = {SOSP '24},
 title = {Verus: A Practical Foundation for Systems Verification},
 url = {https://doi.org/10.1145/3694715.3695952},
 year = {2024}
}