This post focuses on Galois’s silicon projects and related research efforts around asynchronous circuit design as we approach the 27th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2021), to be hosted by Galois as a virtual conference September 7–10, 2021. Since our founding, most of Galois’s R&D projects have focused on software and […]

Proofs are our bread and butter at Galois – we apply proofs to many different assurance problems, from compiler correctness to hardware design. Proofs and the theorem proving technologies that apply them are very powerful, but that power comes with a cost. In our experience, proofs can be difficult to maintain over time as systems […]

The title of our blog post may sound like a directive from a Dungeon Master, but it’s firmly rooted in Galois’s forward-thinking computer science.  C/C++ code is the foundation of our most critical systems – even “new” systems nearly always incorporate legacy code. But this type of component reuse carries its own dangers because we […]

The world was taken by storm when the International Consortium of Investigative Journalists (ICIJ), along with other media bodies, released millions of documents exposing financial chicanery and political corruption. The leaks detailed how prominent people, such as Icelandic Prime Minister Sigmundur Davíð Gunnlaugsson, used offshore entities for illegal activities. Perhaps the most famous of these […]

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

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

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

Building secure communication systems requires both secure cryptographic primitives and also secure cryptographic protocols that build messaging schemes on top of those primitives. Well-designed protocols are the backbone of almost all modern digital communication, enabling key exchange, entity authentication, secure channels, and anonymous messaging. On the other hand, improperly designed protocols can render the best […]

Microsoft Research recently published a pre-release of Lean 4.  Prior versions of Lean focused on being a proof assistant – a software tool that facilitates the development of rigorous mathematical proof through a form of interactive human-machine teaming. The main application of Lean so far has been to digitize theoretical mathematics. A major goal of […]

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