Designing tunable, verifiable cryptographic hardware using cryptol

Abstract

Cryptographic functional units are increasingly being incorporated into microprocessor designs. In this chapter, we demonstrate how the Cryptol language can be used to produce efficient, high-performance, high-assurance circuits that implement cryptographic functions. By way of example, we develop several implementations of the Advanced Encryption Standard (AES) in Cryptol that are optimized for speed or area and proven equivalent to a high-level specification for AES. © 2010 Springer Science+Business Media, LLC.