Our R&D Capabilities

At​ ​Galois,​ ​we​ ​believe​ ​trustworthy​ ​systems​ ​are​ ​built​ ​on​ ​a​ ​formal​ ​mathematical​ ​foundation.​ ​Core to​ ​this​ ​is​ ​the​ ​application​ ​of​ ​formal​ ​analysis​ ​techniques​ ​that​ ​allow​ ​systems​ ​to​ ​be​ ​modeled, analyzed,​ ​and​ ​proven​ ​correct.​

​Our​ ​researchers​ ​and​ ​engineers​ ​apply​ ​this​ ​formalized​ ​approach​ ​to the​ ​design​ ​of​ ​critical​ ​software​ ​systems,​ ​systems​ ​that​ ​must​ ​do​ ​exactly​ ​what​ ​they​ ​are​ ​intended, and​ ​no​ ​more.​ ​This​ ​rigorous​ ​systems​ ​engineering​ ​method​ ​allows​ ​us​ ​to​ ​mathematically​ ​prove​ ​that a​ ​system​ ​behaves​ ​exactly​ ​as​ ​we​ ​intend​ ​under​ ​all​ ​circumstances.

More About Our Approach

  • Formal verification

    • Our team has world-class expertise in using logical frameworks, automated theorem provers, model checkers, rewriters, and other formal methods tools to gain measurable proof that software is correct and secure.

    ×
  • Code that is correct and secure by default

    • Our tools automatically generate code based on high level specifications. This allows us to gain measurable guarantees that the resulting software does only what it is intended to do, and is free of a wide range of errors and vulnerabilities.

    ×
  • Powerful programming languages

    • Our programming languages research and development provides unique advantages to address the problems of highly complex, non-uniform critical systems. We also develop domain-specific languages (DSLs) that enable domain area experts to express their goals in problem-space language, and have confidence in the systems’ reliability and security.

    ×
  • Focus on fundamentals

    • By focusing on fundamental components that are critical to security and reliability—like network stacks, operating systems, hypervisors, and file systems—we enable our clients to cement trustworthiness in the foundation of critical systems.

    ×

Our Technical Areas

Semiconductor Design

We design secure, reliable, efficient bespoke semiconductor solutions to your most difficult computing problems for systems from the network edge to the data center.

Explore

Advanced Cryptography and Privacy

We focus on the groundbreaking processes of securely linking and computing on private data; securely proving computation is done correctly; and on the creation, validation, and synthesis of high-assurance cryptographic solutions, including quantum-resilient (“post-quantum”) schemes.

Explore

Open Source

The open source culture, much like Galois’ own organizational model, thrives on the power of collaboration. Galois benefits from advances made in the open source community and we strive to continually give back, making much of our software freely available to others.

Select Repositories

  • SAW

    The Software Analysis Workbench (SAW) is a set of tools developed for extracting formal models from existing code, enabling developers and security analysts to reason about and prove program properties. SAW is able to show that a program satisfies a functional spec and avoids undefined behavior.

  • SMACCMPilot

    SMACCMPilot is an embedded systems software research project where we are building open-source autopilot software for small unmanned aerial vehicles (UAVs) using new high-assurance software methods.

  • Copilot

    Copilot is a domain-specific language for writing embedded C code. The package includes an interpreter, a compiler, and uses a model-checker to check the correctness of your program. Copilot can be used to develop a variety of functional-style embedded code.

  • Cryptol

    Cryptol is a domain-specific language for specifying cryptographic algorithms. Cryptol version 2 is now released as open source under a 3-clause BSD license. Our goal is that it becomes a widely adopted standard for expressing cryptographic algorithms.

  • HaLVM

    The HaLVM is a port of the GHC runtime system to the Xen hypervisor, allowing programmers to create Haskell programs that run directly on Xen’s “bare metal.”

  • BLT

    BLT is a C/C++ library for solving certain integer linear programming (ILP) problems using techniques that come from the theory of lattices.