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

That’s right, you. The software engineer who hasn’t taken a logic or formal methods course. You already know formal methods. Sure, you might not be able to build a fancy new proof tool this month, but skills you apply every day are the building blocks of formal methods. What gives? People do PhDs in formal […]

At Galois, we are interested in expanding the capabilities of privacy-preserving technologies, as we believe such technology will play a vital role in our future privacy-sensitive world. One such technology that we’ve been exploring is Homomorphic Encryption (HE), a cryptographic mechanism that allows someone to perform computation on encrypted data. In a previous project, we’ve […]

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. In a recent blog post, we shared Galois’s interest in asynchronous circuit design. […]

In 1913 Henry Ford invented the assembly line and forever changed the way the world made physical products. For more than 100 years, the industrial society launched new technologies, new industries, and educational programs focused on perfecting manufacturing and scaling automation via incremental improvements over time.  Process improvement techniques that utilize statistics and mathematical concepts, […]

Distributed protocols enable components such as blockchain validator nodes, cloud servers, or IoT devices to coordinate and cooperate toward a common goal. However, in such a diverse environment, a lot of things can go wrong: hardware can fail, software can be buggy, network links can be unreliable, attackers may compromise components, and so on. Due […]

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