RESEARCH TALK: Interactive Proof Assistants for Verification

UMBC Cyber Defense Lab presents

Many advances have been made in software and hardware assurance using automated tooling.  Constraint-based solving tools like SAT and SMT solvers have proved very useful proving functional correctness in the world of software, while the hardware world relies heavily on the use of industrial-strength model checkers to provide formal verification of important properties like liveness and non-interference.  Sometimes, however, push-button tools are simply not enough. In this talk, we will discuss formal mathematical reasoning using interactive proof assistants, particularly Isabelle. While Isabelle is often thought of as a tool for checking the work of mathematicians, it is, in fact, a powerful engine for reasoning about software and hardware security.  We will work through an example of the verification of a multi-precision arithmetic software library using Isabelle. This talk is aimed at total beginners in the realm of automated theorem proving, and seeks to provide an overview of the fundamental techniques and ideas. 

Ian Blumenfeld is a Principal Research Mathematician at Two Six Labs.  He currently is the principal investigator of TwoSix’s efforts on the DARPA SafeDocs program, attempting to help do type-theoretic reasoning about document specification formats.  He is a former employee of Apple where he worked on the formal verification team, ensuring the security of the iPhone SEP chip. He has done extensive work verifying cyber-physical systems at Johns Hopkins APL.  Mr. Blumenfeld’s interest in formal methods began with his time working as an Applied Research Mathematician in NSA’s Research Directorate. He’s also a pretty good swing dancer.

Host: Alan T. Sherman, sherman@umbc.edu

Support for this event was provided in part by the National Science Foundation under SFS grant DGE-1753681. 

The UMBC Cyber Defense Lab meets biweekly Fridays.  All meetings are open to the public.