Ironclad

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.