The Secrets Must Not Flow: Scaling Security Verification to Large Codebases (extended version)

TL;DR

This paper introduces Diodon, a scalable security verification methodology that separates security-critical code from the rest, enabling semi-automated and fully-automated analysis to verify security properties in large codebases efficiently.

Contribution

Diodon's novel approach splits code into Core and Application, combining manual and automatic verification to scale security analysis to large codebases.

Findings

Successfully verified a large Go codebase with 100k+ lines of code.

Proved Diodon soundness through formal composition of verification techniques.

Achieved security guarantees in less than three person months.

Abstract

Existing program verifiers can prove advanced properties about security protocol implementations, but are difficult to scale to large codebases because of the manual effort required. We develop a novel methodology called *Diodon* that addresses this challenge by splitting the codebase into the protocol implementation (the *Core*) and the remainder (the *Application*). This split allows us to apply powerful semi-automated verification techniques to the security-critical Core, while fully-automatic static analyses scale the verification to the entire codebase by ensuring that the Application cannot invalidate the security properties proved for the Core. The static analyses achieve that by proving *I/O independence*, i.e., that the I/O operations within the Application are independent of the Core's security-relevant data (such as keys), and that the Application meets the Core's requirements. We have proved Diodon sound by first showing that we can safely allow the Application to perform I/O independent of the security protocol, and second that manual verification and static analyses soundly compose. We evaluate Diodon on two case studies: an implementation of the signed Diffie-Hellman key exchange and a large (100k+ LoC) production Go codebase implementing a key exchange protocol for which we obtained secrecy and injective agreement guarantees by verifying a Core of about 1% of the code with the auto-active program verifier Gobra in less than three person months.