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 […]

There has been a lot of chatter recently about large language models, including GPT-4 and LLaMa. At Galois, we have been experimenting with GPT-4, the most capable available large language model. One group of intriguing results that I am excited to present is in the creation of SAWScript memory safety proofs. Using a very simple […]

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 […]

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 […]

Then the program makes a few stack allocations before the first call to @mk: Conclusion Pointer analysis is a foundational static analysis. We hope you’ve enjoyed learning a bit more about it! More information about cclyzer++ can be found in the project documentation.

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 […]

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, […]

Conclusion You’ve now seen most of the essential features of cclyzer++. The next post will explore some more advanced topics and bring it all together with a larger example.

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 […]

We are pleased to announce the release of Crux 0.6. Crux is a tool for verifying programs containing inline specifications. Crux works with both C/C++ code (via Crux-LLVM) and Rust code (via Crux-MIR). This release brings a variety of improvements, including: Crux-LLVM now has improved support for LLVM debug metadata when the debug-intrinsics option is […]