I first attended POPL, the ACM SIGPLAN Symposium on Principles of Programming Languages, in Rome, as a first-year grad student in 2013. It was my first real experience in the programming languages (PL) community. My undergraduate advisor presented a paper I had co-authored at a co-located workshop. I attended the programming languages mentoring workshop (PLMW), […]
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 […]
Prior to spinning out of Galois, engineers from Niobium Microsystems completed work on the 21st Century Cryptography DARPA project. This project developed a proof-of-concept ASIC containing high-performance, low-energy, side-channel resistant implementations of AES-256 cryptographic primitives. These implementations were developed in correct-by-construction fashion, by directly translating formal models of the cryptographic constructs into a hardware implementation […]
2021. Wow. There it went. And far more interesting than most of us anticipated. While weathering the various world storms, we also managed to keep advancing the cause of building trustworthy computing systems. Galois continued pioneering work in formal methods, high-assurance cryptography, machine learning, data science, rigorous digital engineering, and more. From our virtual perch, […]
This blog post derived from a presentation given 2021-11-12 at a workshop for the University of Southern California’s Center for Autonomy and Artificial Intelligence. Black-box machine learning (ML) methods, often criticized as difficult to explain, can derive results with an accuracy that matches or exceeds human ability on real-world tasks. This has been demonstrated in […]
We recently hosted the 2021 Galois Balloween Workshop. This year it was held virtually, but we hope to have attendees join us in one of our offices next time. We have all attended so many virtual events in the last year and a half, so we wanted to make this workshop fun, hence the name Balloween. […]
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 […]
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.