After four and a half years of work on the DARPA I2O Brandeis Program, we are excited to announce the completion of Jana, a project which set out to develop accessible privacy-preserving data as a service (PDaaS) to protect the privacy of data subjects while retaining data utility to users.  The Galois-led Jana project aimed […]

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

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

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

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

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

This is the third 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 two: Specifying HMAC in Cryptol. In the second post, we left off with the Cryptol specification for HMAC. That’s […]

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

In June 2015, Amazon introduced its s2n library, an open-source TLS library that prioritizes simplicity. A stated benefit of this simplicity is ease of auditing and testing. Galois recently collaborated with Amazon to show that this benefit extends to verifiability by proving the correctness of s2n’s implementation of the keyed-Hash Message Authentication Code (HMAC) algorithm. To construct this […]

A new release of the Software Analysis Workbench (SAW) is now available! This release includes a large collection of new features and bug fixes enabling verification of a wider variety of Java and LLVM programs. A list of changes is available here, along with binaries for a variety of platforms. Additionally, this release changes the […]