The Need for Speed: Revolutionizing CPS Design with AI

For more than two decades, the Need for Speed (NFS) video game franchise captured the hearts of young gamers across the globe with its high-octane thrills, heart-pounding car chases, and the adrenaline rush of illegal street racing. Yet for many, especially those who played the earliest iterations in the late ‘90s and early 2000s, NFS […]

Read More

Generative AI for Specifications 

System engineering involves a delicate interplay between three tasks: specification (what a system should do); implementation (what a system actually does); and verification (determining whether they agree). Already, novel generative AI technologies have emerged that can assist with implementation and verification (e.g., respectively, Microsoft’s CoPilot, and formal verification tools developed on DARPA’s PEARLS Artificial Intelligence […]

Read More

Prevent the Next XZ Incident: Galois’s LAGOON Tool Offers an Answer to Open-Source Software Threats

In March, 2024, researchers discovered a backdoor hidden in an update of open-source Linux tool XZ Utils – a vulnerability that appears likely to be the result of a multi-year, state-sponsored supply chain attack. This latest close call is only the most recent in a growing history of incidents underscoring the fragility of a modern […]

Read More

Is Your Technology Human-Ready?

 In 2014, Google Glass was released to the public to great fanfare. Just the previous year, in his 2013 TED Talk, Google co-founder Sergey Brin spoke about the human usability issues that Google Glass was designed to solve, and they sounded plausible enough. Who wants to be hunched over their phone all the time? Wouldn’t […]

Read More

Formal Verso: the Formal Methods Future of Smart Contract Security

In May 2016, the newly created Decentralized Autonomous Organization (DAO), an investor-directed venture capital fund built as a smart contract on the Ethereum blockchain, raised around $150 million worth of digital currency. Hopes were high. The fund was to be a fully transparent and decentralized organization, with investment decisions made collectively through member votes, and […]

Read More

Introducing Cheesecloth: A Tool for Proving Software Vulnerabilities in Zero Knowledge

In the world of cybersecurity, proving software vulnerabilities responsibly is a critical challenge.  Imagine a security analyst discovers a vulnerability and wants to tell a software company that their program can be hacked. Here, they face a common dilemma: when they tell the software company about the vulnerability, the company may choose to simply ignore […]

Read More

Galois / Twisp: Avoiding Foolishness in Distributed Systems

“Foolish consistency,” Emerson claimed, “… is the hobgoblin of little minds.” We agree! The problem, in both philosophy and distributed computing, is to figure out when consistency is foolish and when it is absolutely necessary. Fortunately, formal methods technologies can help us address this problem. Galois and our partner Twisp have been using the P language for […]

Read More

Galois Unlocks the Power of Private Set Intersection: A Game-Changer for Data Privacy

The US Department of Education (DOE) was in a quandary. Every few years, they were required to report to Congress on the state of undergraduate student financial aid in the United States, but the confidential data needed to create the report was divided between two different internal offices—offices forbidden by policy to share data with […]

Read More

Bringing Zero Knowledge Proofs to the Masses

The arcane world of cryptographic proofs seldom finds expression on the dashboard of your average automobile, but a partnership between Galois and Cybernetica is steering the state of the art in privacy-preserving technology towards the road less traveled—in Estonia, to be precise. In 2020, Estonia’s Environmental Investment Centre introduced a public program to encourage the […]

Read More