Cryptographers develop algorithms designed to keep mission-critical information secret. They deal in mathematical equations, proofs, and circuits, all of which are a long ways from an implementation. Galois developed the Cryptol language as a specification language for cryptographic algorithms, capturing the circuits in a fully executable specification. Code generators produce implementations for a variety of hardware and software platforms, and symbolic simulators for the basis of our verification capabilities. Current research directions for Cryptol include expanding the number of supported implementation platforms, and improving our verification capabilities for those platforms.
Homomorphic encryption allows calculations/programs to be executed on encrypted data, thereby eliminating the need to unencrypt sensitive data in environments that require security.
Galois has been awarded by the Defense Advanced Research Projects Agency (DARPA) to act as research integrator for the PROCEED program (Programming Computation on Encrypted Data), whose goal is to make it homomorphic encryption feasible. This group of researchers is working toward the goal of making fundamental progress in the science and mathematics of computing on encrypted data, while at the same time increasing the efficiency of implementations of the new techniques by several orders of magnitude.
While the Cryptol language was developed specifically for cryptography, it can be used to specify a broader class of stream processing algorithms, and to produce high performance, high-assurance hardware and software implementations. We are working jointly with Galois’ scientific computing research area to extend the Cryptol capabilities beyond cryptography.
Collaborate with Us
Licensing - Obtain a license for one of our advanced technologies.
Research & Development - Solve your toughest problems by exploring new approaches with us.
Training - Learn how to use cutting-edge tools to increase trustworthiness in your critical systems.