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 […]
Modern formats, in brief By and large, when people share a document (whether it’s formatted text, visual media, or some combination), they believe that when they both look at it, they’re seeing the same thing. Modern users have arguably been taught/coerced into tolerating small differences (color pallets that are varying degrees of rich-to-washed-out, poop emojis […]
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 […]
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.