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

Announcing the Release of Crux 0.6

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

Read More

Announcing the Release of Cryptol 2.13.0

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

Read More

An Essential Tool for Cryptography Development

Cryptography continues to rapidly transform our world. It seems like every day there’s a new story about fully homomorphic encryption, blockchains, and how these technologies secure billions and even trillions of dollars in assets.  We’ve talked about cryptographic algorithms and twice about cryptographic assurance. People who work with these concepts every day have been the […]

Read More

Crux in SV-COMP 2022: A Retrospective

This year Galois participated in the annual Competition on Software Verification (SV-COMP) for the first time with our verification tool, Crux. Preparing Crux to be in competition shape has been a project several years in the making, and we are very pleased to have reached this milestone. In this post, we will take a closer […]

Read More