Presentation

file

Visible to the public Formal Verification of Production Distributed Protocols

Byzantine fault-tolerant (BFT) protocols underlie many highly scalable distributed services. For example, distributed databases and blockchain applications both use BFT protocols to ensure that, despite the absence of any central authority, all participants agree on the global state of the database or blockchain.
file

Visible to the public Integration Challenges in Static Analysis and Verification

What would it take to reach a point where 80% of developers at DoD Primes and Fortune 500 companies are using formal methods based tools? Certainly tool capabilities, efficiency, and usability play an important role here. But scaling formal methods is not just about scaling analysis techniques to handle more code or more complex specifications, but also about developing the infrastructure to allow analysis tools to deliver value in larger, more complex organizations, and ensuring that analysis processes and workflows can handle systems that evolve over time.

file

Visible to the public A Verified Optimizer for Quantum Circuits

Programming quantum computers will be challenging, at least in the near term. Qubits will be scarce, and gate pipelines will need to be short to prevent decoherence. Fortunately, optimizing compilers can transform a source algorithm to work with fewer resources. Unfortunately, there is a risk that such compilers will operate incorrectly, potentially in a way that is hard to detect; the result could be wrong answers or even security vulnerabilities.

file

Visible to the public Run-Time Assurance Architecture for Learning-Enabled Systems

There has been much publicity surrounding the use of machine learning technologies in self-driving cars and the challenges this presents for guaranteeing safety. These technologies are also being investigated for use in manned and unmanned aircraft. However, systems including "learning-enabled components" (LECs) and their software implementations are not amenable to verification and certification using current methods.

file

Visible to the public Actionable definition of Safety Design Patterns using AADLv2, ALISA and the Error Modeling Annex

Demonstrating safety of critical systems is achieved by the careful examination of evidences built from software, hardware, functional, and non-functional properties and the architecture that combines them to form the overall system. Formal methods (model checking, theorem proving) provide evidences that are later combined to form a system’s assurance case.

file

Visible to the public Cryptographic Protocol Verification in AWS

In this talk, I will describe how Amazon Web Services verifies the cryptographic protocols that are used to secure its cloud platform. This verification is accomplished through the mechanization of cryptographic security proofs in the computational model. In some cases, we mechanize proofs in existing tools, such as EasyCrypt.

file

Visible to the public Beyond "Bots" and "Trolls": Understanding Disinformation as Collaborative Work

ABSTRACT

file

Visible to the public Building Trust in an Untrustworthy World

ABSTRACT