Ian Blumenfeld
Principal Research Mathematician
Two Six Labs
12:00noon–1pm
Friday, January 31, 2020
ITE 227
Abstract:
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 in 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.
About the Speaker:
Ian Blumenfeld is a Principal Research Mathematician at Two Six Labs. His 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.
E-mail: ian.blumenfeld@twosixlabs.com
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.