This two-day workshop is organised by the Pip Development Team funded by the ODSI European project and with the kind participation of Orange Labs. It will bring together researchers and practitioners in Operating Systems (OS) and Formal Methods (FM), interested in system design and machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4, including research that focuses on proof methods, as well as research targeting OS architecture, thus making it both a low-level system and a mathematical gathering.

Most applications running on digital devices rely on OS kernels. In contrast with user applications, OS kernel software runs in privileged CPU mode and it is thus highly critical. Its asynchronous code presents a high potential for failure and exposure to attacks. Large projects have thus invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are generally quite delicate in terms of safety as well as security, insofar as any vulnerability in the unproven Trusted Computing Base (TCB) can result in negative and invalidating consequences on the stability and functioning of a verified software system, by allowing for invariants and assumptions on which proofs are based to be broken in case of adversarial attack or error.

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 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.

Program Committee

• Julien Cartigny, University of Lille
• Gilles Grimaud, University of Lille
• David Nowak, CNRS
• Vicente Sanchez-Leighton, Orange Labs
• Paolo Torrini, University of Lille

Invited speakers

• Reynald Affeldt, AIST, Japan
• June Andronick, Data61/NICTA, Australia
• Christoph Baumann, KTH Royal Institute of Technology, Sweden
• Adam Chlipala, MIT, United States
• David Cock, ETH Zurich, Switzerland
• Mads Dam, KTH Royal Institute of Technology, Sweden
• Alexandre Miquel, University of the Republic, Uruguay
• Magnus Myreen, Chalmers University of Technology, Sweden
• Francesco Zappa Nardelli, INRIA, France
• Alastair Reid, Arm Ltd, United Kingdom
• Zhong Shao, Yale University, United States