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 […]
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 […]
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 […]
In the film Rocky Balboa, Rocky tells his son, “Nobody is gonna hit as hard as life. But it ain’t how hard you hit; it’s about how hard you can get hit and keep moving forward.” At Galois, we appreciate Rocky’s tenacity and inventiveness. Rocky is the ultimate underdog who perseveres despite overwhelming odds. We […]
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 […]
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 […]
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 […]
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 […]
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 […]
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 […]
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.