Along with Amazon Web Services, Galois is publishing a new paper titled “Verified Cryptographic Code for Everybody,” and we really do mean everybody. One benefit of the way we’ve done this work is that everyone who was using the code already is now using verified code. The library we’ve verified parts of is called AWS-LibCrypto. Much of that library is code that originated from BoringSSL, and BoringSSL is composed of code originating from OpenSSL. By almost any metric, these are the most-used cryptography libraries in the world, and we have verified some of the most critical code that they contain!

In the proof, we used SAW to verify hand-written cryptography safe and correct with regards to Cryptol specifications. The optimizations and details of the code we were verifying made the work very challenging but equally rewarding and important. We’re happy that our proofs have helped provide assurance for commonly used cryptography. The paper describes how our proofs work, and it also covers some of the challenges and engineering we did to accomplish such a challenging task. I hope you give it a read, and please reach out with your questions.

As secure multi-party computation (MPC) moves into the mainstream, users will expect it to support familiar data types such as IEEE-754 standard floating-point representations. Today, however, MPC typically does not support that standard. Instead, MPC implementations generally support alternative real number representations that are more amenable to MPC computation. In this paper, we compare performance of IEEE-754 floating point in MPC with those alternative representations, and we show that IEEE-754 may not perform well enough in MPC to be a wise choice.

PKCS#11, also known as Cryptoki, is a widely adopted C-language API and interoperability standard for communicating with cryptographic libraries. While comprehensive and prescriptive, the standard is also extremely complex. The base specification alone describes approximately 50 functions through over 100 pages of documentation. Add-on specifications provide additional functionality, but also impose additional complexity. As the standard evolves through collaboration and expansion, new areas of imprecision and ambiguity are introduced which make it difficult for vendors to implement libraries that are 100% functionally accurate and compliant with the specification. Users of cryptographic libraries are familiar with the industry reality that PKCS#11 libraries will not always interoperate flawlessly with each other. In the best case, these divergences result in development delays as build issues and functional deficiencies are root-caused and remedied. In the worst case, customers may face production outages or data corruption due to incorrect assumptions or imperfect testing.

To address this problem at its core, Galois has developed an API specification and testing framework that captures the complex behaviors of Cryptoki in a mathematical specification language. This specification, in turn, is used to automatically synthesize a test suite that enforces compliance with (a mathematical model of) the PKCS#11 standard. The approach, known as model-based testing, was used to generate a corpus of PKCS#11 compliance tests that provide complete test coverage over the formal model.

While model-generated tests are designed to enforce compliance with the PKCS#11 standard, they have also proven effective at keeping bugs out of production. Error handling scenarios defined in the standard often represent corner cases which, if not properly handled by implementation code, will cause program crashes or other serious defects. Because the aim of model-based testing is to generate test cases for all the behaviors in the standard, errors of this variety are naturally uncovered with compliance tests. As a result, assuring PKCS#11 libraries with model-generated compliance tests leads to client applications that are portable, more robust and have fewer security vulnerabilities.

Over the past 20 years, a variety of automated software diversity techniques have been proposed. Some techniques randomize aspects of the implementation that are left undefined by the source language specification, such as code layout, stack layout, or locations of heap-allocated objects. Others insert instrumentation or obfuscation that is transparent from an application perspective, e.g. using XOR masks to obscure data values in memory or hiding code pointers using jump tables. A common assumption is that layering these techniques improves security due to increased entropy in the resulting binary. In this paper we examine this assumption and show that it fails to hold in general. In particular, it fails in one of the strongest deployment models for software diversity—that of multiple diverse variants running together in a multi-variant execution environment (MVEE) where attacks manifest as detectable behavioral divergence. We present several examples of diversity combinations that are vulnerable to attack in an MVEE even when none of the component techniques are vulnerable in isolation. Based on these results, we present guidance on which techniques do combine well and suggestions for effective deployment of diversity in MVEEs.

Presented at the Layered Assurance Workshop (LAW), 2016
https://www.acsac.org/2016/workshops/law

We report our research on formal methods guided testing of autonomous systems. In particular, we looked at closed-loop control systems that incorporate neural network based reinforcement learning components. Typically reinforcement learning approaches train good control policies only after millions of experiments due to the sparsity of high reward actions. This may be unacceptable in online learning setting. Our solution to this problem is inspired by Imitation Learning, a learning from demonstrations framework, in which an agent learns a control policy by directly mimicking demonstrations delivered by an expert.

In 2007, Shacham introduced Return-oriented Programming (ROP), a mechanism whereby an attacker can string together small snippets of existing executable code—known as gadgets—in order to exploit programs without injecting new bits of code. Despite numerous proposed mechanisms for mitigating their effects, ROP attacks remain a widespread attack vector for modern software systems. Research on Control-Flow Integrity (CFI) has often shown that these protections incur significant slowdown which is understood to be too costly for general-purpose use.

We investigate the design space of minor hardware extensions with potentially large performance savings and relatively few semantic changes. These hardware extensions significantly reduce the number of gadgets usable by attackers while requiring only minimal changes to existing software, and could be augmented in critical software by stronger software CFI protections.

We present a simulated hardware platform implemented as a modification of the QEMU hardware emulator that features loose-grained forward-edge CFI enforcement and fine-grained backward-edge CFI enforcement built into the operation of the instruction set, as well as modified versions of the Linux operating system and GNU Compiler Collection (GCC) infrastructure that allow us to run a typical Linux installation with minimal changes. We show that these simple hardware extensions and the corresponding software modifications can reduce usable ROP gadgets by a significant amount, making attacks against this platform significantly more difficult. Additionally, we discuss the tradeoffs and challenges that surfaced in the course of this implementation.

Code-Reuse Attacks (CRAs) are well studied in the academic community. In this article, we provide a brief summary of notable attacks and mitigations with a focus on Return-oriented Programming (ROP). Our goal is to provide a roadmap for readers who may or may not be familiar with CRAs and who want to become more familiar with the research. As this is a roadmap, our aim is to be broad and concise with executive summaries, including citations, but otherwise defer to the original publications for a detailed account.

We have included a glossary at the end of technical terms and acronyms. In addition, our bibliography includes more articles than are covered and we recommend the enthusiastic reader to review the bibliography to discover additional reading material in this area.