A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)
OPEN ACCESS
Loading...
Author / Producer
Date
2023-09-10
Publication Type
Working Paper
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.
Permanent link
Publication status
published
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
Cornell University
Event
Edition / version
v2
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: