Galois, Inc.

Introducing GREASE: Our open-source tool for uncovering hidden vulnerabilities in binary code. Learn more in our latest article.

Great writeup from Tweede golf about their experience using Galois, Inc. and Immunant's c2rust tool to translate bzip2 from C code to a Rust implementation. Give it a read! https://lnkd.in/ev_mzsZ4

Galois, GE Aerospace, and the University of Vermont (UVM) are excited to announce a collaboration on the Anonymous Real-Time Speech (ARTS) program, which seeks to develop new technologies for anonymizing conversational speech to help safeguard individual speakers’ identities. Learn more in our latest article.

In a recent (excellent) The Wall Street Journal article, Journalist Belle Lin explored how Amazon is using automated reasoning to tackle the problem of AI hallucinations head-on. Galois's work proving correctness of AWS cryptography is mentioned! Automated reasoning is a subset of formal methods – Galois’s bread and butter. Since 2015, Galois has worked with AWS to help ensure the security of some of the key cryptographic systems that protect their cloud. AWS’s customers include?start-ups, large enterprises, and leading government agencies in more than 245 countries. Our work with AWS has yielded the highest possible level of continuous protection for a large percentage of the world’s most valuable and most critical data. That means that Galois has played a key role in securing financial transactions that keep the global economy churning, state secrets that keep citizens safe, and the privacy of personal communications. This is real, tangible impact at the highest level—all thanks to applied math. Now, Galois is working with DARPA to better understand the inner workings of Generative AI. Why it works when it works, why it fails when it fails, and how to achieve predictable, bounded AI behavior. Stay tuned.?

Galois's RDE framework revolutionizes defense system development, reducing timelines and increasing confidence. Learn how this model-based approach enables rapid capability deployment without compromising on quality or security.

Galois was awarded $12.6 million by DARPA for HEIMDALLR (Hybrid Electromagnetic side-channel and Interactive-proof Methods to Detect and Amend LogicaL Rifts) to support the COOP (Continuous-correctness On Opaque Processors) program. Today, although mission critical software (MCS) in DoD equipment may be heavily tested or even formally proven correct, the correct execution of that software remains at risk due to interactions with the physical and software environment on which it runs. Currently, it is very difficult to assure trust about that external environment, which includes the processor and memory on which the software runs, because you only have control over the MCS. It is also difficult to assure trust about other portions of the software stack, such as the operating system and other programs that run in the same environment, which are likely commercial or otherwise “off-the-shelf”. With HEIMDALLR, Galois aims to solve this problem through an alternative approach that combines the power of formally-verifiable computation, rather than formally verified software, with the use of electromagnetic side-channel sensing to assure that errors in program flow or computation are provably identified, isolated, and corrected during execution. Learn more in our latest!

Over the winter break, OpenAI announced their new model,?o3. Much of the media attention rightly focused on its impressive results on the?ARC-AGI benchmark, but for us at Galois, the most significant result was something else—the model’s?25% score?on a benchmark called Frontier Math. Learn more in our latest article by Mike Dodds:

Galois is excited to announce that we are kicking off a project to verify the frontend of the?Jolt zkVM, with financial support provided by a grant from the?Ethereum Foundation.

Complex systems, like aircraft, are notoriously difficult to modify quickly and safely. Could Rigorous Digital Engineering (RDE) offer a solution? We tested this approach on a SuperVolo UAV to see if it could help us swap out a component with full understanding of the impact of that change on safety and performance. If successful, this approach could be applied to bigger and more complicated cyber-physical systems, potentially save the DOD billions, and transform the future of engineering. Learn more in our latest animated video:

As 2024?comes to a close and a new year begins, we’re excited to reflect on a great year at Galois that saw groundbreaking research projects, innovative software releases, and impactful new collaborations. We love what we do, and it’s fun to share highlights made possible by working well together! Give our 2024 Highlights article a read to learn more about what we've been up to!