We are a leader in the ground-breaking process of computing on data while it remains encrypted, and in the automated generation, validation and synthesis of high assurance cryptographic solutions.Explore
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 to have important properties. We use functional programming language technologies that facilitate such formal analysis as well as providing flexibility to build specialized languages for solving and analyzing domain-specific problems.
Our researchers and engineers also apply this formalized approach to the design of software systems where a high degree of trust is placed in the systems to do exactly what they are intended, and no more. And in the realm of embedded systems, our researchers build on their expertise in language design, static analysis, and formal methods in order to build tools that increase the reliability and simplify the design of complex embedded systems.
More About Our Approach
- Formal Methods
- Functional Programming
- Domain-specific Languages
- Embedded Systems
- Systems Software
Galois' formal methods team has world-class expertise in using theorem provers, model checkers, rewriters, and other formal methods tools to develop high assurance software.×
Galois’ programming languages research is built on functional programming concepts and provides insights and techniques to address the problems stemming from the complexity of business- and mission-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.×
Galois provides a range of services in high-assurance embedded system development. We leverage our expertise in formal verification, run-time monitoring, security, and safety to bring new approaches to the area.×
Galois' systems software offer trusted and assured implementations of many systems components — network stacks, hypervisors, file systems, and device drivers — allowing you to step away from bugging/legacy systems components and replace them with our systems written in high-level languages.×
Our Technical Areas
We design capabilities to make the “human in the loop” work effectively in complex systems.Explore
Our software correctness tools guarantee the confidentiality, integrity, and availability of your systems.Explore
We investigate key questions in ensuring the safety and security of mobile networks and devices.Explore
The world is drowning in data, but most of it goes unused. We create tools that turn data into insights.Explore
We build tools to increase reliability and simplify the design of complex embedded systems.Explore
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 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 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 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.
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 is a C/C++ library for solving certain integer linear programming (ILP) problems using techniques that come from the theory of lattices.