Abstracts

Reynald Affeldt, AIST, Japan

Generation of Code from Coq for Succinct Data Structures (slides)

In this talk, we report on an on-going effort to verify succinct data structures using the Coq proof-assistant. For that purpose, we have been developing a scheme to generate readable and customizable C code from Coq programs. We explain the implementation of the code extraction process as well as the formal guarantees that can be provided regarding its safety. We have organized our code generation scheme in a modular way, the extraction is partly certified, and the monadification process is automated. As a use-case, we generated C code for Jacobson's rank algorithm from a Coq program proved functionally correct, established formally the safety of the generated code using monads, and furthermore provided formal evidence of its complexity.

June Andronick, Data61/NICTA, Australia

seL4&Family: Fast, Trustworthy, Cheap, Deployed (slides)

Since the breakthrough of the world’s first formally verified OS kernel in 2009, seL4 has been extended with new features, ported to new platforms, embedded with high-assurance user-level software, demonstrated to protect against cyber attacks in unmanned helicopters, robot, autonomous trucks… In this talk we will give an overview of the latest achievements to make verified software a reality in real-world deployed systems and of the progress towards the remaining challenges to make verified software become mainstream.

Christoph Baumann, KTH Royal Institute of Technology, Sweden

The Semantics Stack of the Verisoft XT Project (slides)

The original Verisoft project (2004-2007) was a pioneering effort in system software verification, achieving pervasive verification of correctness for a realistic (albeit academic) operating system from the application level all the way down to gate level hardware. Its successor Verisoft XT (2007-2010) aimed to develop the underlying methodologies further and apply them on industry-scale systems, yet these initial aspirations were partly abandoned due to the adoption of a new automated code verification tool: Microsoft Research's VCC. By end of the project, attention of the participants at Saarland University focused on the underlying semantics stack again, in order to justify the soundness of verifying operating system code with VCC. This talk aims to shed light on some of the fundamental results that were produced throughout this effort over the last seven years.

Adam Chlipala, MIT, United States

Raising the Level of Abstraction in Systems Programming with Fiat and Extensible, Correct-by-Construction Compilers (slides)

Systems infrastructure components like OS kernels tend to be coded in low-level, "unsafe" languages like C. One common motivation is to eke out every last bit of performance, which may be worth the effort because these components are so widely used. However, there is a cost in programmer productivity. Many kinds of mistakes are possible that would be ruled out by high-level languages, and even high-level languages leave programmers with challenges in selecting data structures and algorithms. What if programming tools could support even higher levels of abstraction than in Java or OCaml, while at the same time delivering the kind of performance we associate with C? And what if it could all be done in a way that delivers first-principles proofs of correctness for assembly code? In this talk, I'll explain how our Fiat system meets that description.

David Cock, ETH Zurich, Switzerland

Modeling the OS/Hardware Interface with Sockeye (slides)

The Barrelfish research OS shares much with the seL4 microkernel: in particular, an emphasis on accurate modeling of the OS/Hardware interface, and automatic generation of correct-by-construction HW interface code. While the hardware on which seL4 was verified was relatively simple, Barrelfish targets very large-scale systems, with an enormous variety of quirky hardware. In this talk I will introduce Sockeye, our domain-specific language for the declarative modeling of hardware (including physical address spaces, and clock and power domains), and how we use it to automatically generate both static configuration (e.g. kernel page tables), and dynamic (allocating resources to device drivers, and configuring clock trees). As a specification language with clear semantics (formalised in Isabelle/HOL), Sockeye is a significant advance on the state of the art for hardware specification (e.g. Device Trees), and permits verifiable, correct-by-construction management of diverse and rapidly-evolving hardware interfaces.

Mads Dam, KTH Royal Institute of Technology, Sweden

The PROSPER Project: Verified Hypervisors at KTH (slides)

The PROSPER project was executed at KTH and SICS during 2011-2017, funded mainly by the Swedish Foundation for Strategic Research. During PROSPER, three hypervisor generations at increasing levels of sophistication were developed and formally verified to varying levels of detail. In the presentation I give an overview of results obtained during PROSPER and some of the challenges and directions we see for future work.

Narjes Jomaa, David Nowak and Paolo Torrini, University of Lille, France

Formal Development of the Pip Protokernel (slides)

Alexandre Miquel, University of the Republic, Uruguay

How to Use Formal Proofs to Detect Bugs (slides)

Magnus Myreen, Chalmers University of Technology, Sweden

Verification of the GCC-Generated Binary of the seL4 Microkernel (slides)

The GCC compiler is used to produce a binary from the verified C source code of the seL4 microkernel. This talk is about how Thomas Sewell and I have verified the correctness of the GCC-generated binary for GCC optimisation levels O1 and O2; GCC optimisation level O2 is used in production. The work includes use of a proof-producing decompiler and an elaborate SMT-based proof search which finds and then proves the correspondence between the C code and the machine code from the binary.

Francesco Zappa Nardelli, Inria, France

Tales from Binary Formats (slides)

Alastair Reid, ARM Ltd., United Kingdom

Specifications: the Next Verification Bottleneck (slides)

His current research focus is on formalizing the ARM architecture specifications and finding ways that those specifications can be used to make hardware and software better. He has 16 granted patents in Computer Architecture and is the author of over a dozen research papers in Formal Verification, Software Defined Radio, Operating Systems, and Lazy Functional Programming. In his spare time, he builds his own keyboards and enjoys trashing his body in cyclocross races.

Zhong Shao, Yale University, United States

CertiKOS: A Breakthrough toward Hacker-Resistant Operating Systems (slides)

Building certifiably hacker-resistant operating systems is widely considered a grand challenge. Many people believe that the combination of concurrency and an OS kernel’s functional complexity makes formal verification of functional correctness intractable, and even if it is possible, its cost would be prohibitive. In this talk, we present a novel compositional approach for building certified system software. We advocate abstraction over a particularly rich class of specification (called deep specification) and present new methodologies and tools for formally specifying, programming, verifying, and composing abstraction layers. Using these new technologies, we have successfully developed the CertiKOS certified OS kernel and verified its contextual functional correctness in the Coq proof assistant. CertiKOS is written in 6500 lines of C and x86 assembly and runs on stock x86 multicore machines. This is the world’s first proof of functional correctness of a complete, general-purpose concurrent OS kernel with fine-grained locking.