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 […]
At Galois, we’re always looking for better ways to build reliable systems. A big part of that is doing our own research. At 130 people, we’re one of the world’s largest formal methods research teams! But another part of our work is understanding new tools and techniques from the research community. We’re interested in solving […]
The mantra “don’t roll your own crypto” is widely known and accepted amongst programmers, but what does it actually mean? It turns out that such a simple statement is not so simple to follow. What many people take away from “don’t roll your own crypto” is that they shouldn’t create their own crypto algorithms. This […]
We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.