Architectural Security, the Ardennes, and Alfred the Great

This article originally appeared in the Spring 2018 edition of the U.S. Cybersecurity Magazine Much of cyber defense today relies on the same approach used in kinetic defense over the last few thousand years. We use hard perimeters (firewalls) to repel attacks, sentries (IDSs) to trigger incident response, and carefully guarded entry points (VPNs, websites) to […]

Read More

Secure pprzlink: encrypted communications for open source drones

Earlier this month, the Paparazzi team released Secure pprzlink, an encrypted communication protocol for UAVs. While developing Secure pprzlink was a community effort, Galois supported Secure Pprzlink in part as an internal research project I was involved in, and in part as my innovation week project. Secure Pprzlink is an encrypted version of pprzlink. Pprzlink […]

Read More

Galois: 2017 Highlights

2017 brought continued growth in concern about the trustworthiness of computing systems. The breadth of our work at Galois has grown correspondingly. We opened a third office in Dayton, Ohio, grew past 70 employees, and continue to actively hire. We are grateful to our partners and clients that have helped us successfully develop the projects […]

Read More

Revolution and Evolution: Fully Homomorphic Encryption

This article originally appeared in the Summer 2017 edition of the U.S. Cybersecurity Magazine More and more computation is being outsourced to public clouds such as Amazon’s GovCloud and Elastic Compute Cloud, RackSpace, and others. It’s the new “gig” economy for computer hardware. These cloud computers can be just as vulnerable as any other computer, […]

Read More

Formal Methods and the KRACK Vulnerability

On Monday, the KRACK vulnerability to WPA2 was revealed in a paper by Mathy Vanhoef and Frank Piessens. KRACK enables a range of attacks against the protocol, resulting in a total loss of the privacy that the protocol attempts to guarantee. For more technical details on the attack, the website and the Key Reinstallation Attacks […]

Read More

Matterhorn Experience Report

Since August 2016, Galois has been funding the development of Matterhorn, a Haskell terminal client for the MatterMost chat system. Recently, our core development team—Jonathan Daugherty, Jason Dagit and myself—made the first public release of Matterhorn. In this post we’ll discuss our experience building it. All three of us—as well as several other coworkers—were used […]

Read More

Simulating DDoS attacks with ddosflowgen

At Galois, we’ve been investigating new ways to defend against very large distributed denial of service (DDoS) attacks. Under the DHS-funded DDoS Defense program, we’re developing 3DCoP: software that creates a “community of peers” that can detect and mitigate attacks together. We’re interested in attacks that can exceed 1 Tbps (terabits per second) of total […]

Read More

Galois: 2016 highlights

2016 saw a remarkable increase in the awareness and impact of our work in provably secure software and high assurance critical systems. As the year comes to a close, we want to pause and reflect on the intellectual contributions that Galwegians have made as result of that work. Overview This year we partnered with Amazon […]

Read More

Part two: Specifying HMAC in Cryptol

This is the second in a series of three blog posts detailing the use of SAW and Cryptol to prove the correctness of the HMAC implementation in Amazon’s s2n TLS library. Part one: Verifying s2n HMAC with SAW. Part three: Proving Program Equivalence with SAW. In the first post, we described how we proved equivalence between a mathematical description […]

Read More