This is one of a series of workshops inspired by the grand challenge of software verification (particularly GC6). The goals were to:
Because the workshop participants had a wide range of backgrounds, we asked speakers to make their presentations sufficiently self-contained and tutorial to be accessible to those who are not familiar with particular security challenges, formal notations or tools.
Morning of December 7 Erik Poll Formal Methods for Security Joeri de Ruiter Formal analysis of the EMV protocol suite Dino Distefano Security applications of Monoidics' INFER Philippa Gardner Security applications of reasoning about Javascript Afternoon of December 7 Giampaolo Bella Interaction vs. Automation of Tools: Issue or Speculation? Bárbara Vieira Formal Verification of Cryptographic Software Implementations Graham Steel Cryptographic device APIs: formal specification and verification Graham Steel The Tookan device API analyser Bart Jacobs The VeriFast separation logic verifier Ernie Cohen The VCC verifier for concurrent C Morning of December 8 Mark Ryan Verifying security protocols involving persistent state Rod Chapman High assurance software development Rod Chapman SPARKSkein: a formal and fast reference implementation of Skein François Dupressoir Proving Security Properties of C Programs Using VCC Misha Aizatulin Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution Afternoon of December 8 BoF session chaired by Andy Jackson: - Role of Javascript in security (Adam Wright) - Overview of CESG/GCHQ and description of areas of interest (government participants) - Demo of Cryptol (Sean Weaver)