Workshop on Formal Methods And Tools for Security (FMATS)

Venue: Microsoft Research Cambridge (map, miniBus)
Dates: December 7-8, 2011
Organisers: Mike Gordon (local arrangements), Andy Gordon, Bob Warne, Jim Woodcock

This is one of a series of workshops inspired by the grand challenge of software verification (particularly GC6). The goals were to: Most of the FMATS participants are listed here (this list may contain errors: email Mike if you'd like your name added or deleted).

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)

Additional material provided by participants


Maintained by Mike Gordon.
This page last updated on December 24, 2011.