QSAFE

The Internet of Things (IoT) is becoming ubiquitous in commercial and governmental applications. Unfortunately, organizations that design and manufacture low-cost and prolific devices often sacrifice security. The U.S. government is committed to not only enhancing IoT device security, but also hardening it against attacks in a post-quantum (“PQ”) computing world. 

In QSAFE, Galois is working with PQSecure Technologies to create high-quality, Literate Cryptol specifications for all future U.S. Government-blessed, NIST standardized, post-quantum cryptographic algorithms. PQSecure Technologies is implementing several flavors of low resource, side channel-free software and hardware implementations of NIST-approved post-quantum cryptographic algorithms, such as AES, SHA-3, DILITHIUM, and XMMS. Galois complements PQSecure’s efforts by spearheading research in the formal specification of PQ algorithms, and demonstrating how those specifications can be used to assure implementations. 

Updating Cryptographic Algorithmic Standards

Many current cryptographic algorithms are long past due for an update. The National Security Agency (NSA)’s Suite B Cryptography was implemented in 2005 before it was replaced by the Commercial National Security Algorithm Suite (CNSA) in 2018. Some of the algorithms in CNSA, however, would not be sufficient to withstand attacks from a quantum computer. Additionally, many current reasoning tools are not well-suited for reasoning about post-quantum algorithms. For example, some post-quantum algorithms have extremely large key sizes.  

In 2016, the National Institute of Standards and Technology (NIST) called for post-quantum cryptography standardization. The challenge was designed to update cryptographic standards for a post-quantum world. By mid-2022, four finalist algorithms were chosen for standardization and deployment. The selected algorithms have already been included in a new version of the CNSA recommendation announced in September 2022, called CNSA 2.0.  

These types of new algorithms require new hardware implementations – some of which operate in both commercial and DoD environments. Deployment of an implementation in a sensitive government setting requires implementations that can pass NSA certification  – this requires rigorous validation and sometimes formal verification.

NIST’s finalist algorithms are general purpose and not targeted toward a particular deployment scenario. In QSAFE, PQSecure and Galois had to assess which algorithms were fit for IoT use cases.  At the moment, this analysis is largely driven by crypto-engineering wisdom at PQSecure. But in the future, we expect it to be realized by a more rigorous formal trade space study, driven by Galois’s R&D on CHARIOT and other sister DARPA programs.

PQSecure wrote implementations of algorithms by directly reading the NIST English specifications. Galois formally specified the algorithms by writing new (or evolving existing) Cryptol specifications. To make these specifications as close to the original source documents describing the algorithms as possible, Galois obtained the documents from the algorithms’ authors. Galois then “wove” into them formal specifications written in Cryptol, turning them into “Literate Cryptol” specifications. 

The documents are now both a semi-formal, English specification as NIST has been demanding and using all along (e.g., they can be turned into hyperlinks PDFs) and they are formal, executable specifications, about and with which we can reason.

 Blessing Post-Quantum Algorithm Specifications

The Literate Cryptol specifications for the NIST algorithms are “reasonable” – we can formally reason about the specifications, not just with the specifications. We often find errors in the original English specifications and the pseudo-code that they contain. In fact, nearly every government standard blessed specification that we have ever formalized has revealed errors. This precise analysis allows the algorithm’s creator to go back and fix the errors, which is vital for a post-quantum world. 

Galois’s Literate Cryptol specifications may become the U.S. government’s “blessed” final specifications for these algorithms as part of NIST’s new governmental cryptographic standard.  

Galois’s work with QSAFE is also versatile. These types of formal specifications can be used for several purposes: (1) simulation of a system (in this case, an algorithm and its constituent pieces; but in general, a system’s components, subsystems, or the whole system that is specified – what is colloquially known as a Digital Twin); (2) generation of test vectors; (3) generation of a model-based test bench which includes property-based tests for software, firmware, or hardware implementations; and (4) as the formal specification used to formally verify the correctness of a software, firmware, or hardware implementation.  

By formal verification, we mean that we can prove that an implementation perfectly conforms to its specification for all possible inputs, and that it does nothing else.

The entire cryptographic community will benefit from our work on this project – not just our specification writing, but also on the engineering side as well. Our demonstrations of how these Literate Cryptol specifications can be used for rigorous assurance are as reusable as the specifications themselves.

Demonstrating Rigorous Digital Engineering for Post-Quantum Cryptography

QSAFE represents another Rigorous Digital Engineering project for Galois. The formal specifications for this project are a critical component of RDE, as they define either/both Digital Twins of components of a system. Galois’s high-quality Literate Cryptol specifications of the U.S. government’s “blessed” post-quantum cryptographic algorithms demonstrate only “the tip of the iceberg” for what RDE can accomplish. 

Work inspired by, or based upon, QSAFE will continue into the future. Many companies are implementing PQ algorithms now, and need to demonstrate to NIST, the NSA, and many branches of the DoD, that their implementations are correct. Galois will likely be involved in some of these efforts, and we hope that NIST uses our work to strengthen its CAVP and CMVP programs in the future to assure that blessed PQ implementations really are the blessed PQ algorithms we think they are.