Established: October 2, 2014

An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app’s behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times.

Our specifications, code, proofs, and tools for our projects Ironclad Apps (verifying the security an a complete software stack) and IronFleet (verifying the safety and liveness of distributed systems) are now available on GitHub.  Comments, suggestions, and pull requests are welcome!

One of the key verification tools we use is Dafny.  Try it out on Rise4Fun!  Learn more from the official Dafny site.  Dafny, in turn, relies on Boogie, which relies on the Z3 SMT solver.  We also employ SymDiff to verify relational properties.



Portrait of Brian Zill

Brian Zill

Senior Research Software Development Engineer

Portrait of Chris Hawblitzel

Chris Hawblitzel

Senior Researcher

Portrait of Jay Lorch

Jay Lorch

Senior Principal Researcher

Portrait of Srinath Setty

Srinath Setty

Principal Researcher