Workshop on Formal Methods And Tools for Security (FMATS)

• overview the use of formal methods for security;
• categorise security properties together with the associated formalisms and tools that have been used to address them;
• identify key problems for the research community and priorities to stimulate interest;
• discuss the practical problems and difficulties that potential tool users might encounter.

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

• Formal analysis of the EMV protocol suite.
  Joeri de Ruiter and Erik Poll, Digital Security Group, Radboud University Nijmegen.

• François Dupressoir has provided links to tech report versions of CSF'11 and FAST'11 papers. He has also provided a link to a paper on using a verification by refinement approach, which he says may be a bit more applicable in an industrial development setting (where the spec could be given and proved secure, and the test/verification engineer only has to show that the code does not do what it is not supposed to do).