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

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

Galois is open-sourcing MATE, a suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code. MATE unifies application-specific and low-level vulnerability analysis using code property graphs (CPGs), enabling the discovery of highly application-specific vulnerabilities that depend on both implementation details and the high-level semantics of target […]

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

We are pleased to announce the release of Cryptol 2.13.0. Cryptol is a language for writing and specifying cryptographic algorithms. This release brings a variety of improvements, including: The sortBy function is now implemented using merge sort instead of insertion sort. This improves both asymptotic and observed performance on sorting tasks. “Type mismatch” errors now […]

We are happy to announce the first formal release of Crux, a new open-source verification tool from Galois. This new tool aims to improve software assurance using symbolic testing, a technique that allows for smooth migration from testing to verification. Crux builds on the same infrastructure as our Software Analysis Workbench (SAW), but with a […]