Formal Verification of Hardware Support for Advanced Encryption Standard

The advanced encryption standard (AES), approved by National Institute of Standards and Technology, specifies a cryptographic algorithm that can be used to protect electronic data. The next generation of Intel micro-processor introduces a set of instructions known as AES-NI, that promises multi-folded acceleration of the AES encryption and decryption process. In this paper, we report about the formal verification of hardware support for these new instructions. The verification is based on use of symbolic trajectory evaluation that lies at the base of formal verification methodology used by Intel Corporation. To our knowledge, this is the first formal verification of AES hardware support.