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

Safely Detecting Cats with Crux: A Tutorial

A while back, we announced that we were open-sourcing Crux, a software verification tool. I’d like to work through a slightly more involved example in this post than those presented in the original announcement. In particular, I’d like to give an example of how one might apply Crux to verify functional properties of a system […]

Read More

Under-Constrained Symbolic Execution with Crucible

UC-Crux is an open-source command-line tool and Haskell library for performing under-constrained symbolic execution on LLVM code for the sake of exposing bugs or verifying the absence of certain types of undefined behavior. It requires only LLVM bitcode as input. It is built on Galois’s Crucible library for symbolic execution. Under-constrained symbolic execution (developed by […]

Read More

Cryptographic Assurance with Cryptol

Field arithmetic code is important and has edge cases lurking everywhere. Cryptol is a tool that can guarantee you’ve got the edge cases right! In this post, we continue reproducing an NCC Group Post about programming in z3. In our last post, we checked the implementation of part of the QUIC protocol. Now we’ll explore […]

Read More

Building a Concurrency Verifier Using Crucible

Many of the verification and static analysis tools we build at Galois are based on the same technology: a symbolic execution engine for a language called Crucible. There are a lot of advantages to doing this. It’s what makes it possible for SAW to reason about C, C++, Rust, and x86 assembly, all through the […]

Read More

Of Protocols and Pythons

We’ve been working to improve usability for SAW, our tool for verification of C and Java programs. The primary way that users interact with SAW is its specification and scripting language. In order to make SAW as accessible as possible, Python can now be used as that language for SAW! We’ve built an example to […]

Read More

The Dog Ate My Protocol Spec; A Demo

One of the key understandings of growing up is beginning to appreciate the difference between “should” and “do”. We should eat a balanced diet full of green leafy vegetables, but life happens, and ice cream tastes really good. As engineers and software developers … same thing, different day. We should write good data and protocol […]

Read More