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

Creating Open and Accessible COVID-19 Data Models

Projections based on data models for COVID-19 are serving as a critical foundation for Federal, state and local government policy makers charged with making rapid and informed decisions to fight the spread of the novel coronavirus.  Data models like the model presented by researchers at Imperial College London on March 16, which many believe led […]

Read More

2019: Year in review

2019 marked another eventful year for Galois, publishing 15 papers, sharing 26 talks, and announcing several large project awards. It seems cliche, but it’s true: our partners and collaborators play a central role in all of our work. We’re very grateful to be part of such a great community. Below, we highlight some of the […]

Read More

Protecting Election Integrity with ElectionGuard

Today, Microsoft announced our joint work on ElectionGuard and the upcoming release of the software development kit. This SDK will be freely available, and can be used to enable end-to-end verifiable (E2E-V) elections around the world. An E2E-V election uses cryptography to produce proofs that an election has been run correctly. In a properly implemented […]

Read More

2018: Year in Review

2018 was a year of growth and impact at Galois. We furthered our work from cryptography to software and hardware assurance through both our R&D efforts and our spin-out companies. Our team grew significantly, and like most everyone in this industry, we continue to hire. We’ve been fortunate to work with many great partners and […]

Read More

The Zimmerman Telegram, Enigma, and Inter-Agency Data Sharing

This article originally appeared in the Fall 2018 edition of the U.S. Cybersecurity Magazine When obdurate isolationist Woodrow Wilson won 1916 re-election under the slogan, “He kept us out of the war!”, he hadn’t anticipated a simple act of data sharing. On January 17, 1917, Room 40 (British Naval Intelligence) finally decrypted the infamous German “Zimmerman […]

Read More

Protecting Applications with Automated Software Diversity

On the DARPA CFAR program, the Galois “RADSS” team is developing new ways to mitigate memory corruption attacks against legacy C/C++ systems without requiring finding and fixing each individual bug. CFAR is about “Cyber Fault-tolerant Attack Recovery” and our general approach is: Given some application to defend, generate multiple variants of that application such that […]

Read More