Galois Technologies

We provide software assurance and cyber security at all levels of the stack.

 

Galois provides you with access to world-class high assurance software engineers and researchers. We understand your most difficult problems from a single layer to the whole stack: 

  • Hardware Design
  • OS Kernels, Microvisors and Virtualization
  • Systems, Device Drivers, Network Stacks and WiFi
  • Programming Language and Compiler Design
  • Applications Design and Implementation
  • User Identity Management and Authentication
  • Web Browser Security
  • Systems-of-Systems Configuration and Validation

By addressing performance, trust relationships, and security at all levels of the software stack, we provide you with multiple active defense and protection mechanisms built on a solid foundation of math and computer science. Our technology solutions enable flexible security strategies at an architectural or component level, help address insider threats and detect attack "command and control" patterns.

And, with our safety and security verification and validation (V&V) tools, you can feel confident that our technologies meet specifications and fulfill their intended purpose:

  • Information Flow Analysis
  • Hardware Verification
  • Driver Systems, Kernel Design
  • Type Systems and Formal Mathematical Analysis of Software
  • Automated Software Analysis for a Wide Range of Properties
  • Custom V&V and Analysis Tools

At Galois, we embrace open innovation.  Unlike a large research and development laboratory, where specialists work within siloed groups, our staff works across discipline areas: our networking engineers work closely with our language designers, our operating systems engineers work closely with our web application designers. The result is a unique ability to combine cutting-edge technologies from various layers to build custom solutions and disruptive innovations in computing.

Helping to Standardize Theory Engineering by Archiving Proofs as Theory Packages

This is a short video about theory engineering techniques to support interactive theorem proving for tackling large formalization and verification projects. The OpenTheory project has developed standards for packaging theories of the higher order logic implemented by the HOL family of theorem provers. This talk will present a standard theory library for higher order logic represented as an OpenTheory package. We identify the core theory set of the HOL family of theorem provers, and describe the process of instrumenting the HOL Light theorem prover to extract a standardized version of its core theory development. We profile the axioms and theorems of our standard theory library and investigate the performance cost of separating the standard theory library into coherent hierarchical theory packages.

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.

Let's Work TogetherStart the Conversation >>