Understanding large code bases is hard. It can take months for an experienced engineer to get comfortable navigating and manipulating large software projects. At Galois, we’re developing tools to generate 3D representations of code bases visualized as cities to help engineers get oriented faster, and to develop a shared visual reference for team conversations and […]

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

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.