PLOS 2017 will be an all-day workshop on Saturday, Oct 28th, held in Shanghai, China, just before SOSP.
Location: Room Qingdao of Pudong Shangri-La Hotel
Registration is handled via SOSP (https://www.sigops.org/sosp/sosp17/reg.html).
Certified Preemptive OS Kernels. Prof. Xinyu Feng, University of Science and Technology of China (USTC) [Slides [PDF] ]
Abstract: In this talk, I’ll present a general framework for certifying preemptive OS kernels, and its application to certify key modules of μC/OS-II and a kernel deployed in some Chinese aerospace systems, both of which are practical systems with real-world applications. The framework consists of 1) a mechanized subset of C, with extensions to model thread management and interrupts; 2) a relational program logic for refinement verification of concurrent C programs at the kernel level, with multi-level hardware interrupts; and 3) some Coq tactics for automated development of Coq proofs. As applications of the framework, the key modules of the aforementioned kernels are certified with minimum changes of the code. The certified modules include schedulers, interrupt handlers, semaphores, message queues and other synchronization primitives. I’ll introduce some verification experience and some bugs found in the systems. I’ll also discuss some limitations and on-going work of our group.
About the speaker: Xinyu Feng is Professor in Computer Science at University of Science and Technology of China (USTC). Before joining USTC in 2010, he got his PhD at Yale University in 2007, and worked as a research assistant professor at Toyota Technological Institute at Chicago (TTIC). His research interests are in theories of programming languages, formal program verification, and concurrency. In particular, he is interested in developing theories, programming languages and tools to build certified system software, with rigorous guarantees of safety and correctness.
- The Cogent Case for Property-Based Testing. Zilin Chen, Liam O’Connor, Gabriele Keller, Gerwin Klein, and Gernot Heiser (Data61 and UNSW) [Slides [PDF] ]
- Towards Correct-by-Construction Interrupt Routing on Real Hardware. Lukas Humbel, Reto Achemann, David Cock, and Timothy Roscoe (ETH Zurich) [Slides [PDF] ]
- Programmable Elasticity for Actor-based Cloud Applications. Bo Sang (Purdue University), Srivatsan Ravi (University of Southern California), Gustavo Petri (IRIF - Université Paris Diderot), Mahsa Najafzadeh (Purdue University), Masoud Saeida Ardekani (Samsung Research America), and Patrick Eugster (Purdue University and TU Darmstadt) [Slides [PDF] ]
- Adaptable Actors: Just What The World Needs. Paul Harvey (National Institue of Informatics) and Joseph Sventek (University of Oregon)
- Theseus: a State Spill-free Operating System. Kevin Boos and Lin Zhong (Rice University) [Slides [PDF] ]
- Annotations in Operating Systems with Custom AspectC++ Attributes. Daniel Friesel, Markus Buschhoff, and Olaf Spinczyk (TU Dortmund) [Slides [PDF] ]
- Towards Fine-grained, Automated Application Compartmentalization. Nikos Vasilakis, Ben Karel, Nick Roessler, Nathan Dautenhahn, André Dehon, and Jonathan Smith (University of Pennsylvania) (talk + demo) [Slides [PDF] ]
- Sandcrust: Automatic Sandboxing of Unsafe Components in Rust. Benjamin Lamowski (N/A), Carsten Weinhold, Adam Lackorzynski, and Hermann Härtig (TU Dresden) [Slides [PDF] ]
8:45 -- Welcome
9:00 -- Keynote Talk
10:00 -- Break
10:45 -- Presentations I
12:00 -- Lunch
13:30 -- Presentations II
14:45 -- Break
15:30 -- Presentations III
16:35 -- Discussion
17:30 -- End