Vehicle E/E Architectures – The Last Ten Years and the Future

Before diving in, I’d like to acknowledge our amazing partners in this research, DGTech and Transportation Research Center Inc., and share a quick disclaimer. This material is based upon work done in partnership with DGTech and Transportation Research Center Inc., and supported by National Highway Traffic Safety Administration (NHTSA). Any opinions, findings, conclusions, or recommendations expressed […]

Read More

Identifying Design Choices That Increase a System’s Exploitability

We know that software flaws can create vulnerabilities within a system. But a system’s design often impacts whether a software flaw can be exploited. For example, subtle differences between a system’s ideal design and its implementation can lead to different emergent run-time behaviors. These emergent behaviors can act like a “programmable weird machine” – making […]

Read More

ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification

I’m excited to announce our paper “ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification” has been accepted to PLDI 2022.  Programs often need to reveal information about private or sensitive data. For example, consider an advertiser who wants to send an advertisement to users near a restaurant. To accomplish this, the advertiser could write […]

Read More

Room for Disagreement

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

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

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

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

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