Presentation

file

Visible to the public KEYNOTE: Take a SEAT: Security-Enhancing Architectural Transformations

System architecture models in a language such as AADL provide a high-level setting in which existing implementations, new design features, high-level requirements, and verifications can be combined. We have recently been developing selected architecture-to-architecture transformations as a way to enhance the security of a system. The transformations are formally specified at a high level and mapped to implementations by a sequence of correctness-preserving (and deductively justified) compilation steps.
file

Visible to the public Trustworthy AI: New Properties for New Complex Systems

Recent years have seen an astounding growth in deployment of AI systems in critical domains such as autonomous vehicles, criminal justice, healthcare, hiring, housing, human resource management, law enforcement, and public safety, where decisions taken by AI agents directly impact human lives. Consequently, there is an increasing concern if these decisions can be trusted to be correct, reliable, fair, and safe, especially under adversarial attacks.
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.