Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation
Authors: 
Anish Athalye, 
Henry Corrigan-Gibbs, Frans Kaashoek, Joseph Tassarotti, Nickolai ZeldovichAuthors Info & Claims
Anish Athalye, Henry Corrigan-Gibbs, Frans Kaashoek, Joseph Tassarotti, Nickolai ZeldovichAuthors Info & ClaimsPages 655 - 672
Abstract
Parfait is a framework for proving that an implementation of a hardware security module (HSM) leaks nothing more than what is mandated by an application specification. Parfait proofs cover the software and the hardware of an HSM, which catches bugs above the cycle-level digital circuit abstraction, including timing side channels. Parfait's contribution is a scalable approach to proving security and non-leakage by using intermediate levels of abstraction and relating them with transitive information-preserving refinement. This enables Parfait to use different techniques to verify the implementation at different levels of abstraction, reuse existing verified components such as CompCert, and automate parts of the proof, while still providing end-to-end guarantees. We use Parfait to verify four HSMs, including an ECDSA certificate-signing HSM and a password-hashing HSM, on top of the OpenTitan Ibex and PicoRV32 processors. Parfait provides strong guarantees for these HSMs: for instance, it proves that the ECDSA-on-Ibex HSM implementation---2,300 lines of code and 13,500 lines of Verilog---leaks nothing more than what is allowed by a 40-line specification of its behavior.
References
[1]
CVE-2004-0320. https://nvd.nist.gov/vuln/detail/CVE-2004-0320, September 2004.
[2]
YSA-2015-1. https://developers.yubico.com/ykneo-openpgp/SecurityAdvisory%202015-04-14.html, April 2015.
[3]
CVE-2018-6875. https://nvd.nist.gov/vuln/detail/CVE-2018-6875, February 2018.
[4]
YSA-2018-01. https://www.yubico.com/support/security-advisories/ysa-2018-01/, January 2018.
[5]
CVE-2019-18671. https://nvd.nist.gov/vuln/detail/CVE-2019-18671, November 2019.
[6]
CVE-2019-18672. https://nvd.nist.gov/vuln/detail/CVE-2019-18672, November 2019.
[7]
YSA-2020-04. https://www.yubico.com/support/security-advisories/ysa-2020-04/, July 2020.
[8]
CVE-2021-31616. https://nvd.nist.gov/vuln/detail/CVE-2021-31616, April 2021.
[9]
Dakshi Agrawal, Bruce Archambeault, Josyula R. Rao, and Pankaj Rohatgi. The EM side-channel(s). In Proceedings of the 2002 IACR Workshop on Cryptographic Hardware and Embedded Systems (CHES), Redwood City, CA, August 2002.
[10]
Eyad Alkassar, Wolfgang J. Paul, Artem Starostin, and Alexandra Tsyban. Pervasive verification of an OS microkernel: Inline assembly, memory consumption, concurrent devices. In Proceedings of the 3rd Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), pages 71--85, Edinburgh, United Kingdom, August 2010.
[11]
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying constant-time implementations. In Proceedings of the 25th USENIX Security Symposium, pages 53--70, Austin, TX, August 2016.
[12]
ARM Limited. ARM Cortex-M3 processor technical reference manual. https://developer.arm.com/documentation/100165/latest/, November 2016. Revision r2p1.
[13]
Anish Athalye. Formally Verifying Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation. PhD thesis, Massachusetts Institute of Technology, August 2024.
[14]
Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying hardware security modules with information-preserving refinement. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 503--519, Carlsbad, CA, July 2022.
[15]
Konstantinos Athanasiou, Byron Cook, Michael Emmi, Colm MacCárthaigh, Daniel Schwartz-Narbonne, and Serdar Tasiran. SideTrail: Verifying time-balancing of cryptosystems. In Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), pages 215--228, Oxford, United Kingdom, July 2018.
[16]
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, and Bryan Parno. SoK: Computer-aided cryptography. In Proceedings of the 42nd IEEE Symposium on Security and Privacy, pages 777--795, Virtual conference, May 2021.
[17]
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. Formal verification of a constant-time preserving C compiler. In Proceedings of the 47th ACM Symposium on Principles of Programming Languages (POPL), New Orleans, LA, January 2020.
[18]
Jean-Baptiste Bédrune and Gabriel Campana. Everybody be cool, this is a robbery! https://donjon.ledger.com/BlackHat2019-presentation/, August 2019.
[19]
William R. Bevier, Warran A. Hunt Jr., J. Strother Moore, and William D. Young. An approach to systems verification. Journal of Automated Reasoning, 5(4):411--428, December 1989.
[20]
Sandrine Blazy, David Pichardie, and Alix Trieu. Verifying constant-time implementations by abstract interpretation. Journal of Computer Security, 27(1):137--163, 2019.
[21]
Brett Boston, Samuel Breese, Josiah Dodds, Mike Dodds, Brian Huffman, Adam Petcher, and Andrei Stefanescu. Verified cryptographic code for everybody. In Proceedings of the 33rd International Conference on Computer Aided Verification (CAV), pages 645--668, Los Angeles, CA, July 2021.
[22]
Helena Brekalo, Raoul Strackx, and Frank Piessens. Mitigating password database breaches with Intel SGX. In Proceedings of the 1st Workshop on System Software for Trusted Execution (SysTEX), Trento, Italy, December 2016.
[23]
Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. Constant-time foundations for the new Spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 913--926, London, United Kingdom, June 2020.
[24]
Dominic Cheli. Apple iOS hardware assisted screen-lock bruteforce. https://www.mdsec.co.uk/2015/03/apple-ios-hardware-assisted-screenlock-bruteforce/, March 2015.
[25]
Yu-Fang Chen, Chang-Hong Hsu, Hsin-Hung Lin, Peter Schwabe, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang, and Shang-Yi Yang. Verifying Curve25519 software. In Proceedings of the 21st ACM Conference on Computer and Communications Security (CCS), pages 299--309, Scottsdale, AZ, November 2014.
[26]
David Costanzo, Zhong Shao, and Ronghui Gu. End-to-end verification of information-flow security for C and assembly programs. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 648--664, Santa Barbara, CA, June 2016.
[27]
Filippo Cremonese. Security analysis of the Solo firmware. https://blog.doyensec.com/2020/02/19/solokeys-audit.html, February 2020.
[28]
Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337--340, Budapest, Hungary, March-April 2008.
[29]
Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In Proceedings of the 40th IEEE Symposium on Security and Privacy, pages 73--90, San Francisco, CA, May 2019.
[30]
Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. Integration verification across software and hardware for a simple embedded system. In Proceedings of the 42nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Virtual conference, June 2021.
[31]
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, and Adam Chlipala. Foundational integration verification of a cryptographic server. In Proceedings of the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Copenhagen, Denmark, June 2024.
[32]
Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt. A programmable programming language. Communications of the ACM, 61(3):62--71, March 2018.
[33]
Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), pages 287--305, Shanghai, China, October 2017.
[34]
Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. Time protection: The missing OS abstraction. In Proceedings of the 14th ACM EuroSys Conference, Dresden, Germany, March 2019.
[35]
J. A. Goguen and J. Meseguer. Security policies and security models. In Proceedings of the 3rd IEEE Symposium on Security and Privacy, pages 11--20, Oakland, CA, April 1982.
[36]
Ronghui Gu, Jeremie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In Proceedings of the 42nd ACM Symposium on Principles of Programming Languages (POPL), pages 595--608, Mumbai, India, January 2015.
[37]
Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 653--669, Savannah, GA, November 2016.
[38]
Marco Guarnieri, Boris Köpf, Jan Reineke, and Pepe Vila. Hardware-software contracts for secure speculation. In Proceedings of the 42nd IEEE Symposium on Security and Privacy, pages 1868--1883, Virtual conference, May 2021.
[39]
Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. Ironclad Apps: End-to-end security via automated full-system verification. In Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 165--181, Broomfield, CO, October 2014.
[40]
Michael Hutter and Jörn-Marc Schmidt. The temperature side channel and heating fault attacks. In Proceedings of the 12th Smart Card Research and Advanced Application Conference (CARDIS), pages 219--235, Berlin, Germany, November 2013.
[41]
Jan Jancar, Vladimir Sedlacek, Petr Svenda, and Marek Sys. Minerva: The curse of ECDSA nonces (systematic analysis of lattice attacks on noisy leakage of bit-length of ECDSA nonces). IACR Transactions on Cryptographic Hardware and Embedded Systems, 2020(4): 281--308, 2020.
[42]
Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7): 107--115, July 2009.
[43]
Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. Design and verification of the Arm confidential compute architecture. In Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 465--484, Carlsbad, CA, July 2022.
[44]
lowRISC. OpenTitan: Open source silicon root of trust. https://opentitan.org.
[45]
lowRISC. Ibex RISC-V Core. https://github.com/lowRISC/ibex, 2015.
[46]
Nancy Lynch and Frits Vaandrager. Forward and backward simulations - Part I: Untimed systems. Information and Computation, 121(2):214--233, September 1995.
[47]
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. Verified compilation on a verified processor. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 1041--1053, Phoenix, AZ, June 2019.
[48]
Rita Mayer-Sommer. Smartly analyzing the simplicity and the power of simple power analysis on smartcards. In Proceedings of the 2000 IACR Workshop on Cryptographic Hardware and Embedded Systems (CHES), pages 78--92, Worcester, MA, August 2000.
[49]
Daniel Moghimi, Berk Sunar, Thomas Eisenbarth, and Nadia Heninger. TPM-FAIL: TPM meets timing and lattice attacks. In Proceedings of the 29th USENIX Security Symposium, pages 2057--2073, Virtual conference, August 2020.
[50]
Nicholas Mosier, Hanna Lachnitt, Hamed Nemati, and Caroline Trippel. Axiomatic hardware-software contracts for security. In Proceedings of the 49th Annual International Symposium on Computer Architecture (ISCA), pages 72--86, New York, NY, June 2022.
[51]
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, and Gerwin Klein. Noninterference for operating system kernels. In Proceedings of the 2nd International Conference on Certified Programs and Proofs, pages 126--142, Kyoto, Japan, December 2012.
[52]
Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. seL4: from general purpose to a proof of information flow enforcement. In Proceedings of the 34th IEEE Symposium on Security and Privacy, pages 415--429, San Francisco, CA, May 2013.
[53]
George C. Necula. Translation validation for an optimizing compiler. In Proceedings of the 21st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 83--94, Vancouver, Canada, June 2000.
[54]
Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 54(1):31--39, August 2020.
[55]
Nitrokey. Nitrokey HSM 2. https://shop.nitrokey.com/shop/nkhs2-nitrokey-hsm-2-7.
[56]
Amir Pnueli, Michael Siegel, and Eli Singerman. Translation validation. In Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 151--166, Lisbon, Portugal, March--April 1998.
[57]
Thomas Pornin. BearSSL constant-time mul. https://bearssl.org/ctmul.html.
[58]
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Catalin Hritcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified low-level programming embedded in F*. In Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming (ICFP), Oxford, United Kingdom, September 2017.
[59]
Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, and Santiago Zanella-Beguelin. EverCrypt: A fast, verified, cross-platform cryptographic provider. In Proceedings of the 41st IEEE Symposium on Security and Privacy, pages 983--1002, San Francisco, CA, May 2020.
[60]
Andrei Sabelfeld and Andrew Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, 2003.
[61]
Thomas Sewell, Magnus Myreen, and Gerwin Klein. Translation validation for a verified OS kernel. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 471--482, Seattle, WA, June 2013.
[62]
Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. Nickel: A framework for design and verification of information flow control systems. In Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 287--306, Carlsbad, CA, October 2018.
[63]
Robert Sison, Scott Buckley, Toby Murray, Gerwin Klein, and Gernot Heiser. Formalising the prevention of microarchitectural timing channels by operating systems. In Proceedings of the 25th International Symposium on Formal Methods (FM), pages 103--121, Lübeck, Germany, March 2023.
[64]
Richard M. Stallman. Using the GNU compiler collection. https://gcc.gnu.org/onlinedocs/gcc/.
[65]
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoué, and Santiago Zanella-Béguelin. Dependent types and multi-monadic effects in F*. In Proceedings of the 43rd ACM Symposium on Principles of Programming Languages (POPL), pages 256--270, St. Petersburg, FL, January 2016.
[66]
The Coq Development Team. The Coq Proof Assistant, version 8.17.1, June 2023.
[67]
Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 530--541, Edinburgh, United Kingdom, June 2014.
[68]
Jean-Baptiste Tristan. Formal verification of translation validators. PhD thesis, Paris Diderot University, France, 2009.
[69]
Florian Uekermann. Buggy OTP slot range check. https://github.com/Nitrokey/nitrokey-profirmware/issues/4, June 2016.
[70]
Dennis M. Volpano, Cynthia E. Irvine, and Geoffrey Smith. A sound type system for secure flow analysis. Journal of Computer Security, 4(2/3):167--188, 1996.
[71]
Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. Specification and verification of side-channel security for open-source processors via leakage contracts. In Proceedings of the 30th ACM Conference on Computer and Communications Security (CCS), pages 2128--2142, Copenhagen, Denmark, November 2023.
[72]
Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan. CT-wasm: type-driven secure cryptography for the web ecosystem. In Proceedings of the 46th ACM Symposium on Principles of Programming Languages (POPL), pages 77:1--77:29, Cascais, Portugal, January 2019.
[73]
Claire Xenia Wolf. Yosys Open SYnthesis Suite. https://github.com/YosysHQ/yosys, 2012.
[74]
Claire Xenia Wolf. PicoRV32 - a size-optimized RISC-V CPU. https://github.com/YosysHQ/picorv32, 2015.
[75]
Yubico. YubiHSM 2. https://www.yubico.com/product/yubihsm-2/.
[76]
Yongbin Zhou and Dengguo Feng. Side-channel attacks: Ten years after its publication and the impacts on cryptographic module security testing. Cryptology ePrint Archive, Paper 2005/388, October 2005.
[77]
Jean-Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. In Proceedings of the 24th ACM Conference on Computer and Communications Security (CCS), Dallas, TX, October--November 2017.
Index Terms
- Modular Verification of Secure and Leakage-Free Systems: From Application Specification to Circuit-Level Implementation
Index terms have been assigned to the content through auto-classification.
Recommendations
Formal semantics, modular specification, and symbolic verification of product-line behaviour
Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated ...
Comments
Information & Contributors
Information
Published In
November 2024
765 pages
ISBN:9798400712517
DOI:10.1145/3694715
- Chair:
- Emmett Witchel,
- Co-chair:
- Christopher J Rossbach,
- Program Chair:
- Andrea Arpaci-Dusseau,
- Program Co-chair:
- Kimberly Keeton
This work is licensed under a Creative Commons Attribution International 4.0 License.
Sponsors
In-Cooperation
- USENIX
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 November 2024
Check for updates
Badges
Qualifiers
- Research-article
Funding Sources
- NSF
Conference
SOSP '24
Sponsor:
SOSP '24: ACM SIGOPS 30th Symposium on Operating Systems Principles
November 4 - 6, 2024
TX, Austin, USA
Acceptance Rates
SOSP '24 Paper Acceptance Rate 43 of 245 submissions, 18%;
Overall Acceptance Rate 174 of 961 submissions, 18%
Upcoming Conference
SOSP '25
- Sponsor:
- sigops
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 107Total Downloads
- Downloads (Last 12 months)107
- Downloads (Last 6 weeks)81
Reflects downloads up to 03 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in