Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper presents an approach and a tool, CASM-VERIFY, to automatically check the equivalence of highly optimized assembly implementations of cryptographic algorithms. The key idea of this paper is to decompose the equivalence checking problem into several small sub-problems using a combination of concrete and symbolic evaluation. Given a reference and an optimized implementation, CASM-VERIFY concretely executes the two implementations on randomly generated inputs and identifies likely equivalent variables. Subsequently, it uses symbolic verification using an SMT solver to determine whether the identified variables are indeed equivalent. Further, it decomposes the original query into small sub-queries using a collection of optimizations for memory accesses. These techniques enable CASM-VERIFY to verify the equivalence of assembly implementations (e.g., x86 and SSE) of various algorithms such as SHA-256, ChaCha20, and AES-128 for a message block.

Original languageEnglish (US)
Title of host publicationCGO 2019 - Proceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization
EditorsTipp Moseley, Alexandra Jimborean, Mahmut Taylan Kandemir
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages37-49
Number of pages13
ISBN (Electronic)9781728114361
DOIs
StatePublished - Mar 5 2019
Event17th IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2019 - Washington, United States
Duration: Feb 16 2019Feb 20 2019

Publication series

NameCGO 2019 - Proceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization

Conference

Conference17th IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2019
CountryUnited States
CityWashington
Period2/16/192/20/19

All Science Journal Classification (ASJC) codes

  • Software
  • Control and Optimization

Keywords

  • Cryptography
  • Formal verification

Fingerprint Dive into the research topics of 'Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries'. Together they form a unique fingerprint.

  • Cite this

    Lim, J. P., & Nagarakatte, S. (2019). Automatic Equivalence Checking for Assembly Implementations of Cryptography Libraries. In T. Moseley, A. Jimborean, & M. T. Kandemir (Eds.), CGO 2019 - Proceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization (pp. 37-49). [8661180] (CGO 2019 - Proceedings of the 2019 IEEE/ACM International Symposium on Code Generation and Optimization). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CGO.2019.8661180