Presentation

file

Visible to the public Code-Level Model Checking in the Software Development Workflow

This experience report describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C-based systems, e.g., custom hypervisors, encryption code, boot loaders, and the FreeRTOS operating system. Using our methodology, we find that we can prove the correctness of industrial low-level C-based systems with reasonable effort and predictability.
file

Visible to the public One-click Automated Reasoning in Amazon Web Services

Amazon Web Services (AWS) recently launched IAM Access Analyzer, an automated reasoning service for auditing permissions to cloud resources. In this talk, we share the journey of bringing this formal methods technology to market. This includes wrestling with notions of correctness, getting users to specify correctness, and rethinking what correctness means.
file

Visible to the public Scalable Sound Static Analysis of Real-world C Applications using Abstract Interpretation.pdf

Much of critical software systems continues to be written in C, especially embedded and cyberphysical systems. Despite decades of research in formal verication and increases in the sophistication of bug-nding tools, C applications continue to be plagued by exploitable vulnerabilities. The problem: academic tools often don't scale; bug-nding tools are mostly based on heuristics and therefore inherently incapable of providing guarantees.
file

Visible to the public End-to-End Verification of Initial and Transition Properties of GR(1) Designs Generated by Salty in SPARK.pdf

Manual design of control logic for reactive systems is a time-consuming and error-prone process. An alternative is to automatically generate controllers from high-level specifications using “correct-by-construction” synthesis approaches. Recently, there has been interest in synthesizing controllers from Generalized Reactivity(1) or GR(1) specifications, since computational complexity is relatively low.
file

Visible to the public Verification is Engineering

In 2017, we gave a talk at HCSS on two formal Cryptography correctness proofs that we performed on Amazon Web Services production code. Those two proofs covered around 200 lines of security critical C. Since then, we have pushed our tools forward, and our proofs now cover nearly 3000 lines of AWS C code, including post-quantum algorithms.
file

Visible to the public Geometric Path Enumeration Methods for Verifying ReLU Neural Networks

Neural Networks are universal function approximation tools that learn from examples, and increasingly being used in perception and control applications. For safety and mission-critical needs, one needs assurance that a neural network will produce outputs that satisfy formal properties. Several recent methods have been proposed in this direction, including one class of geometric methods that propages sets of states through a neural network.
file

Visible to the public Adapting to demand- seL4 proofs and proof engineering practice

In this talk, we'll discuss some of our experiences scaling the formal verification of the seL4 microkernel to meet customer demand for increasingly complex requirements.

The formal verification of the seL4 microkernel [1] broke new ground, showing that comprehensive verification of a complex software system was possible. That initial effort required solutions to many proof engineering problems, for example, how to decompose refinement proofs so that the work could be distributed across a team [2].

file

Visible to the public 3C: Interactive Conversion of C to Checked C

Checked C1 is a freely available, backward compatible extension to C that aims to support spatial memory safety. Checked C defines annotations for pointer types that its compiler uses to verify, either statically or dynamically, that pointer accesses are safe. Such safety assurance is useful in itself (e.g., it precludes buffer overflows) and also sets a useful foundation for subsequent static analyzers.

file

Visible to the public Analysis of the Secure Remote Password Protocol Using CPSA

We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the rst formal analysis of SRP (specically, Version 3).

file

Visible to the public Verifying C++ at Scale

At BedRock Systems, we are developing and verifying a full virtualization stack from micro-hypervisor to user-land components developed on top of it using a formal-methods-first approach centered around modularity and automation. This ambitious task requires scaling in both the size and the complexity of the code. Formal-methods-first means that our Formal Methods team is working hand-in-hand with our systems developers to specify (and subsequently verify) the code.