Correct-by-construction Cryptographic Hardware via Explicit Staging Transformations
Correct-by-construction Cryptographic Hardware via Explicit Staging Transformations* HCSS 2024: Program Transformation Theme Bill Harrison & Yakir Forman Two Six Technologies Cryptographic algorithms are generally speci ed in detailed design documents (e.g, Blake [4] or Salsa20 [1]) including pseudocode for the algorithms themselves. The approach we present in this talk starts from these informal C-style pseudocodes reflected into Haskell and transforms them semi-automatically into formally veri ed hardware implementations. We use staging annotations [5, 3] to partition the Haskellized algorithm temporally into distinct \pipeline" phases. (1) (3) (5) (2) (4)
Figure 1 illustrates the transformation pro- cess from pseudocode to veri ed hardware. From a Haskell rendering of the imperative pseudocode (1), we introduce staging anno- tations (2) that partition the rendering temporally into distinct phases (3). The annotated rendering is now a ReWire program, where ReWire is a functional high-level synthesis language embedded in Haskell. The ReWire compiler (4) translates this annotated design directly into Verilog and thence to gates (5). We use a previously developed ReWire formalization [2] to verify correctness. Although staging annotation (step (3)) is performed manually, it is straightforward as we illustrate in several non-trivial examples. The staging annotations themselves are ReWire functions with simple semantics, and, hence, relating the initial Haskell rendering (1) to the ReWire hardware design (3) is also straightforward.
*This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA). The views, opinions and/or ndings expressed are those of the author and should not be interpreted as representing the o cial views or policies of the Department of Defense or the U.S. Government.
References
[1] Daniel Bernstein. Salsa20 speci cation. https://cr.yp.to/snuffle/spec.pdf, 2005. Ac- cessed: 2024-01-04.
[2] William L. Harrison, Ian Blumenfeld, Eric Bond, Chris Hathhorn, Paul Li, May Torrence, and Jared Ziegler. Formalized high level synthesis with applications to cryptographic hardware. In NASA Formal Methods Symposium (NFM23), 2023.
[3] Jun Inoue and Walid Taha. Reasoning about multi-stage programs. Journal of Functional Programming, 26, 2016.
[4] Markku-Juhani O. Saarinen and Jean-Philippe Aumasson. The BLAKE2 Cryptographic Hash and Message Authentication Code (MAC). RFC 7693, November 2015.
[5] Walid Taha. A Gentle Introduction to Multi-stage Programming, pages 30{50. Springer Berlin Heidelberg, Berlin, Heidelberg, 2004.
Dr. William Harrison received his BA in Mathematics from Berkeley in 1986 and his doctorate from the University of Illinois at Urbana-Champaign in 2001 in Computer Science. From 2000-2003, he was a post-doctoral research associate at the Oregon Graduate Institute in Portland, Oregon. Until recently, Dr Harrison was on the faculty in the Electrical Engineering and Computer Science department at the University of Missouri. Currently, he is a Senior Principal Research Scientist at Two Six Technologies, Inc., transitioning his research on high assurance hardware into practice. His research interests include all aspects of programming languages research (e.g., language-based computer security, semantics, design and implementation), reconfigurable computing, formal methods and malware analysis.
Dr. Yakir Forman is a Senior Research Scientist on the High Assurance Solutions team at Two Six Technologies, Inc. He received his BA in Physics and Mathematics from Yeshiva University in 2017 and completed his PhD work in mathematical physics at Yale University's Department of Mathematics in 2022. At Two Six, his research focuses on formal methods for software and hardware verification and development, especially in cryptographic contexts.