CAVES: Cryptographic Analysis, Verification, Exploration, and Synthesis
Galois is working with ONR to develop an integrated suite of tools that will allow cryptographers to easily develop new algorithms, quickly compare alternative designs, evaluate relative security properties, and ultimately choose the algorithms that fit the specific tradeoffs of the application they have in mind. Building on powerful, automated theorem provers, the workbench will be able to conclusively prove typical security properties and measure quantitative properties with significant effects on security.
The development of secure cryptographic algorithms requires deep and rare expertise, and is prone to a variety of subtle and hard-to-detect flaws. At the same time, many real world circumstances require either entirely new algorithms or variations on existing algorithms.
The CAVES toolset will allow cryptographers to (1) quickly explore the design space of cryptographic algorithms, (2) choose those that have an appropriate balance of security properties for a given application, (3) have a high degree of confidence in their choice, and (4) synthesize new schemes by automatically exploring a design space. This will provide an easy and efficient way for cryptographers to both design and generate new secure cryptographic algorithms.
During the first phase of the project, we showed the feasibility of performing a collection of analyses in the context of the existing Cryptol and Software Analysis Workbench (SAW) tools. We showed that published approaches for automatically proving security properties about cryptographic algorithms could be replicated within Cryptol and SAW with less human effort and less computation time. We also identified several enhancements to Cryptol and SAW, as well as connections with other tools, that would make analyses of these types easier. Finally, we identified additional analyses of cryptographic security properties that we expect may be feasible to automate or partly automate within the same context.
In Phase II, we are working on two main goals: (1) make a wide variety of analyses, including and extending those explored in Phase I, conveniently available to cryptographers by inte- grating them within Cryptol and SAW and connecting these systems with other existing tools, and (2) develop a synthesizer that uses these tools to automatically generate secure cryptographic algorithms.
This material is based upon work supported by the Office of Naval Research under Contract No. N68335-17-C-0452. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Office of Naval Research.