Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface

Co-located with EuroS&P'19

AIM AND SCOPE

Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue.

The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions.

The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4.

This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018.

TOPICS OF INTEREST

Specific topics include, but are not limited to:

• Verified kernels and hypervisors
• Verified security architectures and models
• Tools and frameworks for hardware security analysis
• Tools and frameworks for security analysis
• Formal hardware models and model validation techniques
• Theorem prover based tools and frameworks for verification of low level code
• Combinations of static analysis and theorem proving
• Theories and techniques for compositional security analysis
• Case studies and industrial experience reports
• Proof maintenance techniques and problems
• Compositional models and verification techniques
• Proof oriented design

The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome.

INVITED SPEAKERS

• Dominique Bolignano, Prove & Run
• Gernot Heiser, University of New South Wales
• Frank Piessens, KU Leuven
• Peter Sewell, Univ. Cambridge

IMPORTANT DATES

Paper submission: March 11, 2019 March 15, 2019

Author notification: April 10, 2019

Camera-ready versions: April 22, 2019 (strict)

Workshop: 16 June 2019

SUBMISSION AND PUBLICATION

There are two categories of submissions:

1. Regular papers describing fully developed work and complete results (10 pages, references included, IEEE format)
2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE format)

All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings.

Papers must be typeset in LaTeX in A4 format (not "US Letter") using the IEEE conference proceeding template with the appropriate options [LaTeX template, Template instructions, IEEE Template Repository]. Failure to adhere to the page limit and formatting requirements can be grounds for rejection.

Submission URL: https://easychair.org/conferences/?conf=entropy2019.

PROGRAM CHAIRS

• Mads Dam, KTH Royal Institute of Technology
• David Nowak, CNRS and University of Lille

PROGRAM COMMITTEE

• Christoph Baumann, Ericsson AB
• Gustavo Betarte, Univ. de la República, Uruguay
• David Cock, ETH Zurich
• Mads Dam, KTH Royal Institute of Technology (chair)
• Anthony Fox, ARM
• Deepak Garg, MPI Saarbrucken
• Ronghui Gu, Columbia University
• Samuel Hym, Univ. Lille
• Thomas Jensen, INRIA and Univ. Rennes
• Toby Murray, Univ. Melbourne
• David Nowak, CNRS and Univ. Lille (chair)
• Vicente Sanchez-Leighton, Orange Labs
• Thomas Sewell, Chalmers