A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version)

TL;DR

This paper introduces a modular verification methodology that directly checks security properties of protocol implementations across various languages, demonstrated on Go and C code for protocols like Needham-Schroeder-Lowe and WireGuard.

Contribution

It presents a novel, language-agnostic approach for verifying security properties directly on protocol implementations, overcoming limitations of model-based verification.

Findings

Verified memory safety and security of Go implementations

Confirmed forward secrecy and injective agreement for WireGuard

Demonstrated applicability across multiple programming languages

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.