High-Assurance Cryptography
Abstract
The implementation of secure and efficient cryptographic libraries is a complex task that requires deep knowledge from various branches of mathematics and computer science. Because of this inherent complexity, developing secure cryptographic software is a daunting task, that is carried by a selected group of experts. A recent stream of highly publicized attacks on widely used cryptographic protocols, libraries, and software: Lucky Thirteen (2013), HeartBleed (2014), Freak (2014), Logjam (2015), CacheBleed (2016), Drown (2016), and RoCA (2017) highlights shortcomings of existing cryptographic software. While many of these attacks are implementation-specific, shortcomings permeate through all levels of cryptographic design and implementation. Most notably, the correctness and verifiability of security proofs has been a repeated source of concern. Our vision is that implementation and design issues can be addressed together, through new methods and tools that help domain experts deliver efficient and high-assurance implementations. The project will contribute to the emergence of high-assurance cryptography through the design and security analysis of key components for a high-assurancecryptographic toolbox (in particular, RNGs, proof systems). In addition, this project will develop new tools and methods for building high-assurance cryptographic implementations. The HACrypt project is a continuation of the Autocrypt and SynCrypt projects and will build on the results developed in those projects.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Aug 15, 2019
- Source ID
- N000141912292
Entities
People
- Dan Boneh
Organizations
- Office of Naval Research
- Stanford University
- United States Navy