Dig Deeper Button
Program Lang Use Cases

Use Cases

• Empower your domain experts

• Manage complexity through abstract modeling and simulation

• Make assurance tractable: apply best-fit techniques and tools, at the right level of abstraction

Programming Languages

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.

Read More >>

Develop functional-style embedded code:
Copilot

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.

Read More >>

High-level, hierarchical, security and information flow policies:
Lobster

This security policy configuration language lets you turn a policy statement to the code that configures the machine. Configure large networks to be secure.

Read More >>

Identify network configuration problems:
Nettle

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. 

Read More >>

Simplify concurrent programming:
Orc

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.

Read More >>