Future Work in Rust Co-Assurance

Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 2 Dancing Links 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.3 Dancing Links Theorems 7 Related Work 8 Conclusion 9 Acknowledgments and References 7 Related Work A number of domain-specific languages targeting both hardware and software realization, and providing support for formal verification, have been created. Cryptol [5], for example, has been employed as a “golden spec” for the evaluation of cryptographic implementations, in which automated tools perform equivalence checking between the Cryptol spec for a given algorithm, and the VHDL implementation. Formal verification systems for Rust include Creusot [8], based on WhyML; Prusti [3], based on the Viper verification toolchain; and RustHorn [20], based on constrained Horn clauses. AWS is developing a model-checker for Rust, Kani [2]. Additionally, Carnegie-Mellon University is developing Verus, an SMT-based tool for formally verifying Rust programs [19]. With Verus, programmers express proofs and specifications using Rust syntax, allowing proofs to take advantage of Rust’s linear types and borrow checking. It will be interesting to attempt the sorts of correctness proofs achievable on our system using these verification tools. 8 Conclusion We have developed a prototype toolchain to allow the Rust programming language to be used as a hardware/software co-design and co-assurance language for critical systems, standing on the shoulders of Russinoff’s team at Arm, and all the great work they have done on Restricted Algorithmic C. We have demonstrated the ability to establish the correctness of several practical data structures commonly found in high-assurance systems (e.g., array-backed singly-linked lists, doubly-linked lists, stacks, and dequeues) through automated formal verification, enabled by automated source-to-source translation from Rust to RAC to ACL2, and have detailed the specification and verification of one such data structure, a circular doubly-linked list employing Knuth’s “Dancing Links” optimization. We have also successfully applied our toolchain to cryptography and data format filtering examples typical of the sorts of algorithms that one encounters in critical systems development. In future work, we will continue to develop our toolchain, increasing the number of Rust features that we can support in the RAR subset, as well as continuing to improve the ACL2 verification libraries in order to increase the ability to discharge RAR correctness proofs automatically. We will also continue to work with our colleagues at Kansas State University on the direct synthesis and verification of RAR code from architectural models, as well as working with colleagues at the University of Kansas on verified synthesis of Rust code from high-level attestation protocol specifications written using the Coq theorem prover. 9 Acknowledgments Many thanks to Donald Knuth for his detailed study of exact cover problems in general, and the “Dancing Links” optimization in particular, that can now be found in Volume 4B of his seminal series, The Art of Computer Programming. It was a pleasure discovering this particular corner of Computer Science, beginning when the author accidentally stumbled upon a previously recorded Knuth “Christmas Lecture” on the subject in late 2022. Previous foundational work on hardware/software co-assurance in Rust was funded by DARPA contract HR00111890001. The views, opinions and/or findings expressed are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. Many thanks to David Russinoff of Arm for developing and improving the RAC toolchain, without which most of the current work would not be possible. Thanks also go to the anonymous reviewers for their insightful comments. References [1] Ron Amadeo (2021): Google is now writing low-level Android code in Rust. Available at https://arstechnica.com/gadgets/2021/04/ google-is-now-writing-low-level-android-code-in-rust/. [2] Amazon Web Services (2022): Announcing the Kani Rust Verifier Project. Available at https://model-checking.github.io/kani-verifier-blog/2022/ 05/04/announcing-the-kani-rust-verifier-project.html?fbclid=IwAR2M_ B1IEBfkVhIXSuuAxt3McC_QpUnTuzDq9jG40HOaJzxw8z1Nw9XU_i4. [3] V. Astrauskas, A. Bıly, J. Fiala, Z. Grannan, C. Matheja, P. Muller, F. Poli & A. J. Summers (2022): The Prusti Project: Formal Verification for Rust (invited). In: NASA Formal Methods (14th International Symposium), Springer, pp. 88–108, doi:10.1007/978-3-031-06773-0_5. Available at https://link.springer. com/chapter/10.1007/978-3-031-06773-0_5. [4] Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, LNCS 2257, Springer, pp. 9–27, doi:10.1007/3-540-45587-6_3. [5] Sally Browning & Philip Weaver (2010): Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In David S. Hardin, editor: Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, pp. 89–143, doi:10.1007/978-1-4419-1539-9_4. [6] Thomas Claburn (2023): Microsoft is busy rewriting core Windows code in memory-safe Rust. Available at https://www.theregister.com/2023/04/27/microsoft_windows_rust/. [7] Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer & John Shackleton (2022): Cyber Assured Systems Engineering at Scale. In: IEEE Security & Privacy, pp. 52–64, doi:10.1109/MSEC.2022.3151733. [8] Xavier Denis (2022): Creusot. Available at https://github.com/xldenis/creusot. [9] Peter H. Feiler & David P. Gluch (2012): Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edition. Addison-Wesley Professional. [10] David S. Hardin (2020): Put Me on the RAC. In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-20), pp. 142–145, doi:10.4204/eptcs.327.13. [11] David S. Hardin (2020): Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems. In: Proceedings of the 2020 IEEE Systems Conference, doi:10.1109/SysCon47679. 2020.9381831. [12] David S. Hardin (2022): Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero-Trust Architecture Development. ACM SIGAda Ada Letters 42(2), pp. 55–61, doi:10.1145/3591335. 3591340. [13] David S. Hardin (2022): Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. In: Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-22), pp. 202–216, doi:10.4204/EPTCS.359.16. [14] David S. Hardin & Konrad L. Slind (2021): Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. In: Proceedings of the Seventh Workshop on Language-Theoretic Security, 42nd IEEE Symposium and Workshops on Security and Privacy (LangSec 2021), doi:10.1109/ SPW53761.2021.00024. [15] Jane Street Group, LLC (2023): Hardcaml: An OCaml library for designing and testing hardware designs. Available at https://github.com/janestreet/hardcaml. [16] Steve Klabnik & Carol Nichols (2018): The Rust Programming Language. No Starch Press. [17] Donald E. Knuth (2022): The Art of Computer Programming. 4B: Combinatorial Algorithms, Part 2, Addison-Wesley. [18] Ramana Kumar, Magnus O. Myreen, Michael Norrish & Scott Owens (2014): CakeML: a verified implementation of ML. In Suresh Jagannathan & Peter Sewell, editors: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, ACM, pp. 179–192, doi:10.1145/2535838.2535841. [19] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno & Chris Hawblitzel (2023): Verus: Verifying Rust Programs Using Linear Ghost Types. Proc. ACM Program. Lang. 7(OOPSLA1), doi:10.1145/3586037. [20] Yusuke Matsushita, Takeshi Tsukada & Naoki Kobayashi (2021): RustHorn: CHC-Based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4), doi:10.1145/3462205. [21] Mentor Graphics Corporation (2016): Algorithmic C (AC) Datatypes. Available at https://www.mentor. com/hls-lp/downloads/ac-datatypes. [22] Mentor Graphics Corporation (2020): Catapult High-Level Synthesis. Available at https://www.mentor. com/hls-lp/catapult-high-level-synthesis/. [23] Eric Mercer, Konrad Slind, Isaac Amundson, Darren Cofer, Junaid Babar & David Hardin (2023): Synthesizing Verified Components for Cyber Assured Systems Engineering. In: Software and Systems Modeling, 22, pp. 1451–1471, doi:10.1007/s10270-023-01096-3. [24] Matt Miller (2019): A proactive approach to more secure code. Available at https://msrc-blog. microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/. [25] Shane Miller & Carl Lerche (2022): Sustainability with Rust. Available at https://aws.amazon.com/ blogs/opensource/sustainability-with-rust/. [26] Razvan Nane, Vlad-Mihai Sima, Christian Pilato, Jongsok Choi, Blair Fort, Andrew Canis, Yu Ting Chen, Hsuan Hsiao, Stephen Brown, Fabrizio Ferrandi, Jason Anderson & Koen Bertels (2016): A Survey and Evaluation of FPGA High-Level Synthesis Tools. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 35(10), pp. 1591–1604, doi:10.1109/TCAD.2015.2513673. [27] David M. Russinoff (2022): Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, second edition. Springer, doi:10.1007/978-3-030-87181-9. [28] Geoffry Song (2020): plex: a parser and lexer generator as a Rust procedural macro. Available at https:// github.com/goffrie/plex. [29] Jeff Vander Stoep & Stephen Hines (2021): Rust in the Android platform. Available at https://security. googleblog.com/2021/04/rust-in-android-platform.html. [30] Loup Vaillant (2022): Monocypher: Boring Crypto that Simply Works. Available at https://monocypher. org. [31] Xilinx, Inc. (2018): Vivado Design Suite User Guide: High-Level Synthesis. Available at https://www.xilinx.com/support/documentation/sw_manuals/xilinx2018_3/ ug902-vivado-high-level-synthesis.pdf. This paper is available on arxiv under CC BY 4.0 DEED license. Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Author: Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 1 Introduction 2 Dancing Links 2 Dancing Links 3 The Rust Programming Language 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5 Rust and RAR 5.1 Restricted Algorithmic Rust 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.2 Translation to ACL2 6.3 Dancing Links Theorems 6.3 Dancing Links Theorems 7 Related Work 7 Related Work 8 Conclusion 8 Conclusion 9 Acknowledgments and References 9 Acknowledgments and References 7 Related Work A number of domain-specific languages targeting both hardware and software realization, and providing support for formal verification, have been created. Cryptol [5], for example, has been employed as a “golden spec” for the evaluation of cryptographic implementations, in which automated tools perform equivalence checking between the Cryptol spec for a given algorithm, and the VHDL implementation. Formal verification systems for Rust include Creusot [8], based on WhyML; Prusti [3], based on the Viper verification toolchain; and RustHorn [20], based on constrained Horn clauses. AWS is developing a model-checker for Rust, Kani [2]. Additionally, Carnegie-Mellon University is developing Verus, an SMT-based tool for formally verifying Rust programs [19]. With Verus, programmers express proofs and specifications using Rust syntax, allowing proofs to take advantage of Rust’s linear types and borrow checking. It will be interesting to attempt the sorts of correctness proofs achievable on our system using these verification tools. 8 Conclusion We have developed a prototype toolchain to allow the Rust programming language to be used as a hardware/software co-design and co-assurance language for critical systems, standing on the shoulders of Russinoff’s team at Arm, and all the great work they have done on Restricted Algorithmic C. We have demonstrated the ability to establish the correctness of several practical data structures commonly found in high-assurance systems (e.g., array-backed singly-linked lists, doubly-linked lists, stacks, and dequeues) through automated formal verification, enabled by automated source-to-source translation from Rust to RAC to ACL2, and have detailed the specification and verification of one such data structure, a circular doubly-linked list employing Knuth’s “Dancing Links” optimization. We have also successfully applied our toolchain to cryptography and data format filtering examples typical of the sorts of algorithms that one encounters in critical systems development. In future work, we will continue to develop our toolchain, increasing the number of Rust features that we can support in the RAR subset, as well as continuing to improve the ACL2 verification libraries in order to increase the ability to discharge RAR correctness proofs automatically. We will also continue to work with our colleagues at Kansas State University on the direct synthesis and verification of RAR code from architectural models, as well as working with colleagues at the University of Kansas on verified synthesis of Rust code from high-level attestation protocol specifications written using the Coq theorem prover. 9 Acknowledgments Many thanks to Donald Knuth for his detailed study of exact cover problems in general, and the “Dancing Links” optimization in particular, that can now be found in Volume 4B of his seminal series, The Art of Computer Programming. It was a pleasure discovering this particular corner of Computer Science, beginning when the author accidentally stumbled upon a previously recorded Knuth “Christmas Lecture” on the subject in late 2022. The Art of Computer Programming. Previous foundational work on hardware/software co-assurance in Rust was funded by DARPA contract HR00111890001. The views, opinions and/or findings expressed are those of the authors and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. Many thanks to David Russinoff of Arm for developing and improving the RAC toolchain, without which most of the current work would not be possible. Thanks also go to the anonymous reviewers for their insightful comments. References [1] Ron Amadeo (2021): Google is now writing low-level Android code in Rust. Available at https://arstechnica.com/gadgets/2021/04/ google-is-now-writing-low-level-android-code-in-rust/. [2] Amazon Web Services (2022): Announcing the Kani Rust Verifier Project. Available at https://model-checking.github.io/kani-verifier-blog/2022/ 05/04/announcing-the-kani-rust-verifier-project.html?fbclid=IwAR2M_ B1IEBfkVhIXSuuAxt3McC_QpUnTuzDq9jG40HOaJzxw8z1Nw9XU_i4. [3] V. Astrauskas, A. Bıly, J. Fiala, Z. Grannan, C. Matheja, P. Muller, F. Poli & A. J. Summers (2022): The Prusti Project: Formal Verification for Rust (invited). In: NASA Formal Methods (14th International Symposium), Springer, pp. 88–108, doi:10.1007/978-3-031-06773-0_5. Available at https://link.springer. com/chapter/10.1007/978-3-031-06773-0_5. [4] Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In: Practical Aspects of Declarative Languages, 4th International Symposium, PADL 2002, Portland, OR, USA, January 19-20, 2002, Proceedings, LNCS 2257, Springer, pp. 9–27, doi:10.1007/3-540-45587-6_3. [5] Sally Browning & Philip Weaver (2010): Designing Tunable, Verifiable Cryptographic Hardware Using Cryptol. In David S. Hardin, editor: Design and Verification of Microprocessor Systems for High-Assurance Applications, Springer, pp. 89–143, doi:10.1007/978-1-4419-1539-9_4. [6] Thomas Claburn (2023): Microsoft is busy rewriting core Windows code in memory-safe Rust. Available at https://www.theregister.com/2023/04/27/microsoft_windows_rust/. [7] Darren Cofer, Isaac Amundson, Junaid Babar, David Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer & John Shackleton (2022): Cyber Assured Systems Engineering at Scale. In: IEEE Security & Privacy, pp. 52–64, doi:10.1109/MSEC.2022.3151733. [8] Xavier Denis (2022): Creusot. Available at https://github.com/xldenis/creusot. [9] Peter H. Feiler & David P. Gluch (2012): Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis & Design Language, 1st edition. Addison-Wesley Professional. [10] David S. Hardin (2020): Put Me on the RAC. In: Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-20), pp. 142–145, doi:10.4204/eptcs.327.13. [11] David S. Hardin (2020): Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems. In: Proceedings of the 2020 IEEE Systems Conference, doi:10.1109/SysCon47679. 2020.9381831. [12] David S. Hardin (2022): Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero-Trust Architecture Development. ACM SIGAda Ada Letters 42(2), pp. 55–61, doi:10.1145/3591335. 3591340. [13] David S. Hardin (2022): Hardware/Software Co-Assurance using the Rust Programming Language and ACL2. In: Proceedings of the Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-22), pp. 202–216, doi:10.4204/EPTCS.359.16. [14] David S. Hardin & Konrad L. Slind (2021): Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations. In: Proceedings of the Seventh Workshop on Language-Theoretic Security, 42nd IEEE Symposium and Workshops on Security and Privacy (LangSec 2021), doi:10.1109/ SPW53761.2021.00024. [15] Jane Street Group, LLC (2023): Hardcaml: An OCaml library for designing and testing hardware designs. Available at https://github.com/janestreet/hardcaml. [16] Steve Klabnik & Carol Nichols (2018): The Rust Programming Language. No Starch Press. [17] Donald E. Knuth (2022): The Art of Computer Programming. 4B: Combinatorial Algorithms, Part 2, Addison-Wesley. [18] Ramana Kumar, Magnus O. Myreen, Michael Norrish & Scott Owens (2014): CakeML: a verified implementation of ML. In Suresh Jagannathan & Peter Sewell, editors: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, ACM, pp. 179–192, doi:10.1145/2535838.2535841. [19] Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno & Chris Hawblitzel (2023): Verus: Verifying Rust Programs Using Linear Ghost Types. Proc. ACM Program. Lang. 7(OOPSLA1), doi:10.1145/3586037. [20] Yusuke Matsushita, Takeshi Tsukada & Naoki Kobayashi (2021): RustHorn: CHC-Based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4), doi:10.1145/3462205. [21] Mentor Graphics Corporation (2016): Algorithmic C (AC) Datatypes. Available at https://www.mentor. com/hls-lp/downloads/ac-datatypes. [22] Mentor Graphics Corporation (2020): Catapult High-Level Synthesis. Available at https://www.mentor. com/hls-lp/catapult-high-level-synthesis/. [23] Eric Mercer, Konrad Slind, Isaac Amundson, Darren Cofer, Junaid Babar & David Hardin (2023): Synthesizing Verified Components for Cyber Assured Systems Engineering. In: Software and Systems Modeling, 22, pp. 1451–1471, doi:10.1007/s10270-023-01096-3. [24] Matt Miller (2019): A proactive approach to more secure code. Available at https://msrc-blog. microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/. [25] Shane Miller & Carl Lerche (2022): Sustainability with Rust. Available at https://aws.amazon.com/ blogs/opensource/sustainability-with-rust/. [26] Razvan Nane, Vlad-Mihai Sima, Christian Pilato, Jongsok Choi, Blair Fort, Andrew Canis, Yu Ting Chen, Hsuan Hsiao, Stephen Brown, Fabrizio Ferrandi, Jason Anderson & Koen Bertels (2016): A Survey and Evaluation of FPGA High-Level Synthesis Tools. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 35(10), pp. 1591–1604, doi:10.1109/TCAD.2015.2513673. [27] David M. Russinoff (2022): Formal Verification of Floating-Point Hardware Design: A Mathematical Approach, second edition. Springer, doi:10.1007/978-3-030-87181-9. [28] Geoffry Song (2020): plex: a parser and lexer generator as a Rust procedural macro. Available at https:// github.com/goffrie/plex. [29] Jeff Vander Stoep & Stephen Hines (2021): Rust in the Android platform. Available at https://security. googleblog.com/2021/04/rust-in-android-platform.html. [30] Loup Vaillant (2022): Monocypher: Boring Crypto that Simply Works. Available at https://monocypher. org. [31] Xilinx, Inc. (2018): Vivado Design Suite User Guide: High-Level Synthesis. Available at https://www.xilinx.com/support/documentation/sw_manuals/xilinx2018_3/ ug902-vivado-high-level-synthesis.pdf. This paper is available on arxiv under CC BY 4.0 DEED license. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv