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

To commemorate the public release of the Software Analysis Workbench (SAW), it seemed fitting to blog about some recent work specifying algorithms in Cryptol and proving properties, leveraging SAW along the way. Cryptol, Galois’s domain specific language for describing cryptographic algorithms, has frequently been demonstrated over individual algorithms and toy problems. Our blog is covered […]

We are pleased to announce a public preview of the Software Analysis Workbench. The Software Analysis Workbench (SAW) provides the ability to formally verify properties of code written in C, Java, and Cryptol. It leverages automated SAT and SMT solvers to make this process as automated as possible, and provides a scripting language, called SAW […]

“Formal verification methods…should be considered the prime choice for verification of complex and mission-critical software ecosystems.” New vulnerabilities in the software infrastructure we all depend on for privacy are discovered frequently. Thus it was not surprising when an INRIA, MSR, and IMDEA team announced discovery of a significant TLS/SSL vulnerability. The surprise in this announcement was […]