GULPHAAC

In partnership with Reduced Energy Microsystems and the University of Southern California, Galois’s GULPHAAC project used high-level synthesis from formally verified mathematical specifications to design the world’s first correct-by-construction, asynchronous cryptographic accelerator.

‍

Traditional hardware designs are either developed by hand in a hardware description language like SystemVerilog, or synthesized from software written in a high-level programming language like C. It is difficult to verify the correct operation of such designs, and as a result hardware development teams typically spend more than half their effort on verification tasks while not catching all the bugs.

In many hardware designs, some defects can be dealt with after fabrication by working around them with microcode, firmware, or software; however, such workarounds can incur significant performance and efficiency costs, making it especially important to avoid them in accelerators, whose main purpose is to speed up repeatedly used arithmetic or cryptographic operations. Testing cryptographic accelerators is especially difficult, because strong cryptographic algorithms—by their nature—have incredibly large state spaces that cannot be efficiently tested.

In addition to the verification difficulties cryptographic circuits present, minimizing their power consumption is critically important; battery-operated mobile devices must be capable of almost continuous cryptographic operations to communicate with modern cellular and WiFi networks, yet must also be lightweight and run for extended periods of time, potentially at very low supply voltages. Designing and implementing correct cryptographic accelerators that can function within these strict power limitations is particularly challenging.

‍Synthesizing high assurance, low power hardware

To address these problems, in GULPHAAC we developed a synthesis tool capable of generating high-assurance, ultra-low-power, power-invariant hardware implementations of cryptographic algorithms and used it to generate implementations of the Simon and Speck lightweight block ciphers. The synthesis tool targets both FPGAs and ASICs and is fabrication-process-neutral. In order to compare lightweight and heavyweight cryptographic algorithm implementations within a single design method, Galois also developed an ultra-low-power AES implementation using the same techniques.

The resulting chips are usable in threshold voltage scenarios, such as energy-harvesting and micro-embedded systems with extremely low power budgets, as well as for high-performance throughput when more power is available.

‍Utilizing proven assurance tools‍

To achieve this, we leveraged Cryptol and SAW, two proven open source tool suites that enable 1) precise specification of cryptographic software, and 2) verification that implementations match the underlying specifications.

For GULPHAAC, Cryptol was extended to automatically synthesize SystemVerilog-CSP implementations of cryptographic algorithms, automatically synthesize SystemVerilog validation and verification test benches for said algorithms, and automatically rigorously validate, and quantitatively measure, non-functional properties like throughput and energy use in-simulation and in-silico using runtime verification.

Concurrent with and leveraging some of this work, Cryptol and SAW were extended to automatically synthesize C- and LLVM-based software implementations of cryptographic algorithms in the same manner, complete with runtime verification test suites and SAW verification proof scripts.

For more information, see this presentation given at the Lightweight Cryptography Workshop.

‍Summary of results

• We fabricated AES, Simon, Speck ASICs in the IBM 130 nm process
• Energy/bit ranges between 4.2 and 7.5 pJ/b (comparable to best hand-written RTL).
• Static load varies between 0.0012 mA and 0.0029 mA (extremely low due to asynchronous design).
• Power varies between 0.05 mW and 10 mW and is in close alignment with (post place and route) simulation.
• Safe minimum operating voltage is the process threshold (~625mV) and operation is power invariant.
• We estimate that our energy use would be 1.5 pJ/bit in 65nm, and in the fJ/bit in the latest processes.