Foundational Integration Verification of a Cryptographic Server
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-reason...
| Main Authors: | , , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery
2024
|
| Online Access: | https://hdl.handle.net/1721.1/155516 |
| _version_ | 1811087842758098944 |
|---|---|
| author | Erbsen, Andres Philipoom, Jade Jamner, Dustin Lin, Ashley Gruetter, Samuel Pit-Claudel, Clément Chlipala, Adam |
| author_facet | Erbsen, Andres Philipoom, Jade Jamner, Dustin Lin, Ashley Gruetter, Samuel Pit-Claudel, Clément Chlipala, Adam |
| author_sort | Erbsen, Andres |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T13:52:50Z |
| format | Article |
| id | mit-1721.1/155516 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T13:52:50Z |
| publishDate | 2024 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | mit-1721.1/1555162024-09-09T04:40:32Z Foundational Integration Verification of a Cryptographic Server Erbsen, Andres Philipoom, Jade Jamner, Dustin Lin, Ashley Gruetter, Samuel Pit-Claudel, Clément Chlipala, Adam 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. 2024-07-09T15:43:16Z 2024-07-09T15:43:16Z 2024-06-20 2024-07-01T07:59:25Z Article http://purl.org/eprint/type/JournalArticle 2475-1421 https://hdl.handle.net/1721.1/155516 Erbsen, Andres, Philipoom, Jade, Jamner, Dustin, Lin, Ashley, Gruetter, Samuel et al. 2024. "Foundational Integration Verification of a Cryptographic Server." Proceedings of the ACM on Programming Languages, 8 (PLDI). PUBLISHER_CC en 10.1145/3656446 Proceedings of the ACM on Programming Languages Creative Commons Attribution https://creativecommons.org/licenses/by/4.0/ The author(s) application/pdf Association for Computing Machinery Association for Computing Machinery |
| spellingShingle | Erbsen, Andres Philipoom, Jade Jamner, Dustin Lin, Ashley Gruetter, Samuel Pit-Claudel, Clément Chlipala, Adam Foundational Integration Verification of a Cryptographic Server |
| title | Foundational Integration Verification of a Cryptographic Server |
| title_full | Foundational Integration Verification of a Cryptographic Server |
| title_fullStr | Foundational Integration Verification of a Cryptographic Server |
| title_full_unstemmed | Foundational Integration Verification of a Cryptographic Server |
| title_short | Foundational Integration Verification of a Cryptographic Server |
| title_sort | foundational integration verification of a cryptographic server |
| url | https://hdl.handle.net/1721.1/155516 |
| work_keys_str_mv | AT erbsenandres foundationalintegrationverificationofacryptographicserver AT philipoomjade foundationalintegrationverificationofacryptographicserver AT jamnerdustin foundationalintegrationverificationofacryptographicserver AT linashley foundationalintegrationverificationofacryptographicserver AT gruettersamuel foundationalintegrationverificationofacryptographicserver AT pitclaudelclement foundationalintegrationverificationofacryptographicserver AT chlipalaadam foundationalintegrationverificationofacryptographicserver |