Paper 2013/316

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, and François Dupressoir

Abstract

We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations in the style of code-based security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries providing complex arithmetic calculations or instantiating idealised components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework with the RSA-OAEP encryption scheme, as standardized in PKCS#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of assembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it is the first application of computer-aided cryptographic tools to real-world security, and the first application of CompCert to cryptographic software.

Note: Associated material (EasyCrypt libraries and proofs, C code and modified CompCert) is not yet available publicly.

Metadata
Available format(s)
PDF
Category
Public-key cryptography
Publication info
Published elsewhere. Unknown where it was published
Keywords
RSAOAEPimplementationcomputer-aided cryptographyside-channelscompilation
Contact author(s)
fdupress @ gmail com
History
2013-05-28: received
Short URL
https://ia.cr/2013/316
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2013/316,
      author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and François Dupressoir},
      title = {Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations},
      howpublished = {Cryptology ePrint Archive, Paper 2013/316},
      year = {2013},
      note = {\url{https://eprint.iacr.org/2013/316}},
      url = {https://eprint.iacr.org/2013/316}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.