A Generic Methodology for the Modular Verification of Security Protocol Implementations
OPEN ACCESS
Loading...
Author / Producer
Date
2022-12-05
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 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
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
2212.02626
Publisher
Cornell University
Event
Edition / version
v1
Methods
Software
Geographic location
Date collected
Date created
Subject
Cryptography and Security (cs.CR); Programming Languages (cs.PL); FOS: Computer and information sciences
Organisational unit
03653 - Müller, Peter / Müller, Peter
Notes
Funding
Related publications and datasets
Is previous version of: