Demo: Control SAW From Any Language

  • David Christiansen

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

Read More

LINK: A $1M DARPA Contract to Help Scientists Build Better Multiphysics Models

  • Charisee Chiw

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

Read More

Galois Team Wraps Up the Jana Project

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

Read More

Discovering and Mitigating Emergent Computations With Innovative Program Synthesis

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

Read More

Galois’s AMIDOL Wins $2.7M From DARPA, and Aims To Make COVID-19 Modeling Actionable In Real-Time

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

Read More

Announcing the ‘blst’ BLS Verification Project

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

Read More

Project Fromager: $12M Project to Apply Zero-Knowledge Proofs to Software Assurance

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

Read More

Coffeebot: a tool for having hallway conversations while working remotely

  • Annie Cherkaev

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

Read More

Providing Safety and Verification for Learning-Enabled Cyber-Physical Systems

  • Matthew Clark

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

Read More

Creating an Assurance Model for Secure Embedded Systems

In 2019, Galois and its spinout Tangram Flex were awarded a $5 million contract for the DARPA I2O Cyber Assured Systems Engineering (CASE) program. We wanted to present an update for the project’s progress.  Introducing Cyber-Assured Plugins to embedded computer systems “The problem is not in our stars … but in ourselves,” is a paraphrase […]

Read More