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

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

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

Building DaeDaLus and ICARUS As We All Try to Stay Out of the Sun

Document and protocol formats are the languages in which computing systems exchange information. The notion of a “document-format” certainly isn’t foreign to most computer users: everyday, vast swaths of users directly create, edit, and share documents and media in formats such as PDF, JPEG, and Word. But in principle, the concept of a “format” is […]

Read More

What4: New Library to Help Developers Build Verification and Program Analysis Tools

At Galois, we develop formal verification tools that rely on a variety of automated solvers for answering mathematical queries. The main solvers we use are called Satisfiability Modulo Theories (SMT) solvers.  These solvers offer the ability to answer questions such as “find me inputs for which a mathematical property holds.”  We have found these tools […]

Read More

PIRATE: $7.5M DARPA Contract To Accelerate Secure Application Development

I’m excited to announce we’ve been awarded a  $7.5 million contract by the Defense Advanced Research Projects Agency (DARPA) to work on PIRATE, a set of software development tools for designing and building high-performance, physically-partitioned applications that protect sensitive information.  PIRATE stands for Partitioning Information via Resource-Aware Transformations for Everyone.  The project is part of […]

Read More

Measuring the Privacy of Computations

Secure computation enables users to compute some result without revealing the inputs. Privacy schemes that are shown to only reveal outputs are said to have input privacy. However, learning these outputs still tells you something about the private inputs. The important question is: “how much?” The Defense Advanced Research Projects Agency (DARPA) Brandeis program aims […]

Read More