Cryptol, SAW, and the Galois Origin Story

Among the many tales of innovation and impact to come from Galois over the years, the origin story of Cryptol and SAW is perhaps the most closely tied with that of the company itself. Today, these open-source verification tools have been used in national security, fintech, and cloud computing applications to keep citizens, systems, and […]

Read More

The Impact of Provable Security: AWS and Supranational

Galois’s mission is to help make the critical systems that the world relies on more secure and trustworthy. Over the years, we’ve put our team’s deep expertise in software correctness, cryptography, digital engineering, and machine learning to work, providing formal assurance for complex systems in high stakes contexts for both government and commercial clients. From […]

Read More

Making a scalable, SMT-based machine code memory model

In this post, we describe a new memory model that we have added to our Macaw binary analysis framework which dramatically improves its performance when dealing with large binaries. Galois continues to invest in our binary analysis tools because they address a significant problem: many developers distribute closed source binaries that cannot be analyzed with […]

Read More

Proof Assistance and Repair in Crux

Overview We have added support for semi-automated proof assistance and repair to Crux, Galois’s symbolic testing tool for C/C++ and Rust. These new capabilities build on support for logical abduction provided by the cvc5 SMT solver that suggests possible facts for failed proof goals, that, when assumed, make the proof goals provable. This feature can […]

Read More

cclyzer++: Scalable and Precise Pointer Analysis for LLVM

We are pleased to announce that Galois is open-sourcing cclyzer++, a new pointer analysis for languages that compile to LLVM, including C and C++.  Pointer analysis is a foundational static analysis with applications to the problems of program optimization, verification, bug finding, and many others. At Galois, we designed cclyzer++ with two main use cases […]

Read More

Taphos: Modernizing the Approach to Modifying Large Scale Legacy Software in Cyber-Physical Systems

Following our previous blog post, The Next Assembly Line, Galois continues our quest to invent tooling that can transform the DevOps process for developing and maintaining software. One of the unwritten pieces of common knowledge in software is that software rarely meets the models of design as implemented. As such, the notion of utilizing modern, […]

Read More

LAGOON: An Analysis Tool for Open Source Communities

At the Mining Software Repositories (MSR2022) conference in May, we presented our LAGOON tool resulting from the DARPA SocialCyber AIE, and led a discussion session on reducing complexity of machine learning. LAGOON provides a comprehensive platform for analyzing and investigating open-source software (OSS) communities for potentially malicious contributors. This is accomplished by ingesting multiple types […]

Read More