Navy Awards Galois $2 Million Contract For Cryptographic Security

Open source cryptographic workbench aims to enable cryptographers to more easily meet evolving security needs

PORTLAND, Ore., Jan 17, 2018 – Galois today announced that it has been awarded a $2 million contract by the Office of Naval Research (ONR) to build a workbench that aims to ease the design process for cryptographic algorithms. For the ONR SBIR Phase II contract, Cryptographic Analysis, Verification, Exploration, and Synthesis (CAVES), Galois will build on tools and techniques created for defense and intelligence applications that verify the correctness of cryptographic software.

Cryptography is the cornerstone of privacy and security. Developing cryptographic algorithms involves specialized expertise, but even seasoned experts can miss a variety of subtle and hard-to-detect flaws. At the same time, many real world applications require either entirely new algorithms or variations on existing algorithms. The workbench aims to aid cryptographers in eliminating flaws and ensuring that the encryption software fits their performance requirements.

“Developing custom encryption algorithms is sometimes necessary, but it can be a difficult and error-prone process,” said Dr. Aaron Tomb, a Research Lead in Software Correctness at Galois. “We aim to augment cryptographic expertise with automated design exploration tools that include checks and verifications to assure that your cryptographic designs are safe and secure.”

The CAVES cryptographic workbench is an integrated suite of tools that aims to:

  • Help cryptographers 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.
  • Conclusively prove typical security properties, such as the fact that an authenticated encryption scheme provides both privacy and authenticity, as well as measuring quantitative properties with significant effects on security, such as an estimate of the probability that the output of an encryption routine is distinguishable from random data.

It will achieve these goals by building on Galois’ Cryptol language in tandem with the Software Analysis Workbench (SAW).

Once the fully functioning workbench is developed, and the efficacy of the tool for exploring selected types of cryptographic algorithms and corresponding design goals has been demonstrated, Galois aims to provide support in transitioning the cryptographic workbench so that it can be integrated into government system security frameworks. In addition, Galois plans to provide the workbench to industry partners that have to develop their own encryption software. The availability of the cryptographic workbench will also accelerate the discovery of various novel cryptographic capabilities such as homomorphic encryption, attribute-based-encryption, and post-quantum public-key algorithms at research institutes and universities around the world.

Dr. Tomb adds: “It can take years and years for the cryptographic community to determine an algorithm is secure. In this project, we will explore ways to automate some of that burden while increasing the assurance level of the testing and verification. Our goal is to allow cryptographers in the defense and enterprise space to reach necessary assurance levels far more quickly and with more confidence.”

Galois has been applying rigorous mathematical techniques to ensure provably secure and correct crypto since 1999. Galois has been and continues to be involved with numerous crypto projects in defense and intelligence, and works with leaders in the commercial sector to ensure their crypto is secure. In 2008 Galois made available to the public Cryptol, a domain specific language for the design, implementation and verification of cryptographic algorithms, developed by Galois over the past decade for the U.S. National Security Agency.

For additional information on the CAVES project, visit

About Galois

Galois has been performing computer science research and development since 1999. With many of the world’s foremost experts in computer science and mathematics and a world-class team of programmers and engineers, Galois is uniquely positioned to take on the world’s most difficult challenges in computer science. Galois is a trusted partner in the defense and intelligence industries, proving the feasibility of cutting edge research as it applies to critical systems. Technology companies turn to Galois to build reliability, safety and security into their product development efforts from day one. For additional information, visit

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.