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

TL;DR

The paper tackles scaling security verification for protocol implementations by partitioning a codebase into a small Core that implements the protocol and an Application that contains the rest. It couples auto-active verification on the Core with automatic static taint analyses over the full codebase to enforce I/O independence and to discharge assumptions, enabling sound composition and full-codebase refinement to the protocol model. The authors demonstrate soundness and practical scalability on two Go-based case studies, including a large production codebase (~100k LoC) and a signed key-exchange implementation, achieving secrecy and injective agreement with the Core comprising roughly 1% of the code in under three person-months. This approach provides a feasible path to verify strong security properties at production scale, balancing rigorous formalism with automation to handle real-world software.

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.

Figures (8)

• Figure 1: The Diodon methodology. We partition the codebase (blue) into the module implementing a protocol (Core) and the remaining codebase (Application). We prove that the Core refines (trace inclusion on the right) a particular role of the verified protocol model (green) by auto-active verification. We apply static analyses to the entire codebase to enforce that secrets (red) do not influence (red arrows) the I/O operations (gray circles) of the Application and to ensure that the Application cannot invalidate the security properties proved for the Core. Consequently, Diodon guarantees that the entire codebase refines the protocol model (trace inclusion in the middle) and, thus, enjoys all security properties proved for that model.
• Figure 2: Sample Core for a simple MAC communication. In Go, function definitions take a list of input parameters and may have a second list for outputs. We omit the continuousRecv 's implementation that invokes the c.cb closure (if non-$\mathbf{nil}$) whenever a message has been received. We simplify the representation of I/O permissions, which describe permitted protocol-relevant I/O operations, and omit proof-related statements.
• Figure 3: Sample Application that is a client of Fig. \ref{['fig:sample-core']}. We omit parsing of command line arguments for presentation purposes and, thus, assume that psk stores the parsed pre-shared key.
• Figure 5: Diodon proves that the entire codebase (blue) refines a protocol model (green) by soundly composing auto-active verification with automatic static analyses. We auto-actively verify the Core based on its specification to show that the protocol-relevant I/O operations refine a protocol role (upper trace inclusion). This specification is partially generated from the protocol model, which is omitted. The static taint analysis proves that all other I/O operations within the entire codebase refine our attacker model (lower trace inclusion). Lastly, we discharge the Core's assumptions by applying automatic static analyses, proving that the Application satisfies the calling restrictions expressed in the Core's specification.
• Figure 6: Example of a signature and specification of a CoreAPI function.