Foundational Integration Verification of a Cryptographic Server

Citations Over TimeTop 11% of 2024 papers

Abstract

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.

Related Papers

• Algebra model and security analysis for cryptographic protocols(2004)
• → A Study on Fine-Grained Security Properties of Cryptographic Protocols for Formal Analysis Method with Reasoning(2018)2 cited
• → Primitive Constituent Elements of Cryptographic Protocols(2018)
• → A Simple and Efficient Approach to Verifying Cryptographic Protocols(2000)
• → A New Security Proof of Practical Cryptographic Devices Based on Hardware, Software and Protocols(2011)