Confidence in the reliability and security of complex critical systems.
In the world of highly complex, non-uniform critical systems, domain area experts are challenged with understanding the system in a way in which they can have confidence in its reliability and security. One solution Galois employs to address this challenge is the development of domain-specific languages (DSL) to translate the system language to the problem-space language in terms that can be understood by both sides.
High performance, formally correct, rapid development:
Cryptol, the Language of Cryptography
Designing cryptographic hardware correctly, while trading off time, space, and power, is expensive and time-consuming. Verifying that a hardware implementation implements a cryptographic algorithm specification correctly is equally challenging. The Cryptol domain-specific language (DSL) tool suite offers a means of rapidly developing high performance hardware implementations, along with formal evidence of their correctness. The tool suite supports the generation of standard VHDL and Verilog hardware description languages.
Develop functional-style embedded code:
Copilot is a domain-specific, embedded stream language for monitoring the correctness of safety-critical guidance, navigation, and control software at run-time. It is specifically developed to write embedded software monitors for more complex embedded systems, but it can be used to develop a variety of functional-style embedded code.
High-level, hierarchical, security and information flow policies:
This security policy configuration language lets you turn a policy statement to the code that configures the machine. Configure large networks to be secure.
Identify network configuration problems:
Improperly configured computer networks can exhibit poor performance, are subject to attack by malicious agents, and are vulnerable to outages. The Nettle technology tests implementations against policies and identifies common misconfigurations.
Simplify concurrent programming:
Orc allows you to orchestrate multiple tasks simultaneously, e.g., pulling data from multiple websites. This workflow language makes it easy to write concurrent programs in a high-level way. Galois has implemented Orc as an embedded language in Haskell and has improved it by adding new features to the language itself.