ACM CCS ’23 Artifact Appendix: A Generic Methodology for the Modular Verification of Security Protocol Implementations
OPEN ACCESS
Loading...
Author / Producer
Date
2023
Publication Type
Other Conference Item
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol models, which is not sufficient to show that their implementations are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations. In this paper, we present a methodology for the modular verification of strong security properties directly on the level of the protocol implementations. Our methodology leverages state-of-the-art verification logics and tools to support a wide range of implementations and programming languages. We demonstrate its effectiveness by verifying memory safety and security of Go implementations of the Needham-Schroeder-Lowe, Diffie-Hellman key exchange, and WireGuard protocols, including forward secrecy and injective agreement for WireGuard. We also show that our methodology is agnostic to a particular language or program verifier with a prototype implementation for C. Hence, our work comprises a reusable verification library implementing our methodology in Go and prototypically in C, a pen-and-paper sketch of our soundness proof, and four verified implementations of security protocols: Needham-Schroeder-Lowe implemented in C and Go implementations of Needham-Schroeder-Lowe, the Diffie-Hellman key exchange, and WireGuard protocols.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
Event
30th ACM SIGSAC Conference on Computer and Communications Security (CCS 2023)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
protocol implementation verification; symbolic security; separation logic; automated verification; injective agreement; forward secrecy
Organisational unit
03653 - Müller, Peter / Müller, Peter
Notes
Funding
Related publications and datasets
Is supplement to: https://doi.org/10.3929/ethz-b-000643184