Colloquium Details
**Special Day/Time: Tues 10/28 @ 2pm ** Ironclad: End-to-End Security via Automated Full-System Verification
Speaker: Jon Howell, Microsoft Research
Location: Warren Weaver Hall 1302
Date: October 28, 2014, 2 p.m.
Host: Michael Walfish
Synopsis:
Collaborators: Chris Hawblitzel, Jon Howell, Bryan Parno, Brian Zill
The aim of the MSR Ironclad project is to expand the boundaries of existing verification work to encompass automated full-system verification, with the goal of providing meaningful security properties to remote users. By combining cryptography, secure hardware, and automated software verification, we aim to build Ironclad services: services that allow a user to securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a high-level specification. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the service will behave at all times.
As a first milestone, we built several basic Ironclad services: one to eliminate offline dictionary attacks on passwords, one to provide trusted notary and TrInc-like services, and one to support a differentially-private database.
To achieve complete verification of these apps and the software supporting them, we developed a set of new and modified tools, a collection of techniques and engineering disciplines, and a methodology focused on rapid development of verified systems software. This software encompasses a verified microkernel, verified drivers, verified network stack, verified system libraries, and verified crypto libraries, including SHA, HMAC, and RSA.
Moving forward, we plan to build more complex services, such as a Microsoft SQL database that operates on encrypted data, or a provably consistent, provably reliable, datacenter-scale name server. Ultimately, our aim is to advance the state of the art in verification of real systems, and to drive progress in verification tools towards better support for building practical systems.
Speaker Bio:
Jon Howell is a distributed systems researcher at Microsoft Research. Recently he is involved in pushing verification into practical systems applications. Past work includes Embassies, a general isolation model for web-like software distribution; and Farsite, a scalable Byzantine-fault-tolerant file system.
Notes:
In-person attendance only available to those with active NYU ID cards.