We are happy to announce the first formal release of Crux, a new open-source verification tool from Galois. This new tool aims to improve software assurance using symbolic testing, a technique that allows for smooth migration from testing to verification. Crux builds on the same infrastructure as our Software Analysis Workbench (SAW), but with a […]
The Software Analysis Workbench (SAW) is one of Galois’s flagship verification tools. SAW has been used to verify important, real-world cryptographic algorithms, such as AES block cipher, the Secure Hash Algorithm (SHA), and Elliptic Curve Digital Signature Algorithm (ECDSA). We have used this to verify existing, widely used libraries such as libgcrypt and Bouncy Castle. […]
We’re pleased to announce Galois’s LINK project, part of DARPA’s Computable Models (COMPMods) program. The project aims to make it easier for scientists to build multiphysics models with an end-to-end, automatic, and portable solution. Multiphysics models are challenging to create, customize, and reuse. One problem is the software and hardware are often outdated, which makes […]
After four and a half years of work on the DARPA I2O Brandeis Program, we are excited to announce the completion of Jana, a project which set out to develop accessible privacy-preserving data as a service (PDaaS) to protect the privacy of data subjects while retaining data utility to users. The Galois-led Jana project aimed […]
One of our previous projects explored how flaws in the design and implementation of systems can introduce “weird machines” that make them vulnerable to exploitation. Now we have begun a follow-up project, Synthesizing Evidence of Emergent Computation (SEEC). SEEC is part of DARPA’s Artificial Intelligence Mitigations of Emergent Execution (AIMEE) program, whose goal is to […]
We wanted to update our April 2020 blog post which discussed the goal of creating open and accessible COVID 19 data models. I’m pleased to report that Galois’s Agile Metamodel Inference using Domain-specific Ontological Languages (AMIDOL) project began its third phase in May 2020. The entire AMIDOL project has been a great success. The project funding […]
I’m happy to share something new the Galois cryptography verification team is working on in collaboration with the Ethereum Foundation, Protocol Labs, and Supranational. However, I’m sorry to inform you that Galois has sold out to dramatic live-blogging. We’ve sold out so much that I, unrequested by anyone, took the liberty of making us a […]
A zero-knowledge proof (ZKP) is a mathematical tool that provides irrefutable proof of a claim’s validity, without revealing anything else about the claim or the data used to prove it. Today, the application of ZKPs often gravitates towards cryptocurrency transactions, where they can be used to prove that a transaction is valid without revealing details […]
Since the onset of working remotely, we’ve built a program at Galois called Coffeebot to help facilitate virtual “coffee chats” in support of maintaining our culture through spontaneous exchanges. Today we’re releasing Coffeebot, and we’re happy to share it along with simple instructions on how to set-up your own! Percolating the idea As a result […]
Machine learning has revolutionized cyber-physical systems (CPS) in multiple industries – in the air, on land, and in the deep sea. And yet, verifying and assuring the safety of advanced machine learning is difficult because of the following reasons: State-Space Explosion: Autonomous systems are characteristically adaptive, intelligent, and/or may incorporate learning capabilities. Unpredictable Environments: The […]
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.