Published: 26th November 2012
DOI: 10.4204/EPTCS.102
ISSN: 2075-2180

EPTCS 102

Proceedings Seventh Conference on
Systems Software Verification
Sydney, Australia, 28-30 November 2012

Edited by: Franck Cassez, Ralf Huuck, Gerwin Klein and Bastian Schlich

Preface
Franck Cassez, Ralf Huuck, Gerwin Klein and Bastian Schlich
Invited Talk: Copilot: a Do-It-Yourself High-Assurance Compiler
Lee Pike
1
Invited Talk: Program Analysis and Verification based on the Construction and Checking of Automata
Andreas Podelski
2
Automatic Verification of Message-Based Device Drivers
Sidney Amani, Peter Chubb, Alastair F. Donaldson, Alexander Legg, Leonid Ryzhyk and Yanjin Zhu
4
Lessons Learned From Microkernel Verification — Specification is the New Bottleneck
Christoph Baumann, Bernhard Beckert, Holger Blasum and Thorsten Bormer
18
A Formal Model of a Virtual Filesystem Switch
Gidon Ernst, Gerhard Schellhorn, Dominik Haneberg, Jörg Pfähler and Wolfgang Reif
33
Automatic Function Annotations for Hoare Logic
Daniel Matichuk
46
Distributed Priority Synthesis
Chih-Hong Cheng, Rongjie Yan, Saddek Bensalem and Harald Ruess
57
On the Use of Underspecified Data-Type Semantics for Type Safety in Low-Level Code
Hendrik Tews, Marcus Völp and Tjark Weber
73
CTGEN - a Unit Test Generator for C
Tatiana Mangels and Jan Peleska
88
Static Analysis of Lockless Microcontroller C Programs
Eva Beckschulze, Sebastian Biallas and Stefan Kowalewski
103
Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications
Chris Hathhorn, Michela Becchi, William L. Harrison and Adam Procter
115
A Forward Reachability Algorithm for Bounded Timed-Arc Petri Nets
Alexandre David, Lasse Jacobsen, Morten Jacobsen and Jiří Srba
125
Time-Darts: A Data Structure for Verification of Closed Timed Automata
Kenneth Y. Jørgensen, Kim G. Larsen and Jiří Srba
141
Chiefly Symmetric: Results on the Scalability of Probabilistic Model Checking for Operating-System Code
Christel Baier, Marcus Daum, Benjamin Engel, Hermann Härtig, Joachim Klein, Sascha Klüppelholz, Steffen Märcker, Hendrik Tews and Marcus Völp
156
Verifying Probabilistic Correctness in Isabelle with pGCL
David Cock
167

Preface

This volume contains the papers accepted at the 7th Systems Software Verification Conference (SSV 2012), held in Sydney, November 28-30, 2012.

Industrial-strength software analysis and verification has advanced in recent years through the intro- duction of model checking, automated and interactive theorem proving, and static analysis techniques, as well as correctness by design, correctness by contract, and model-driven development. However, many techniques are working under restrictive assumptions that are invalidated by complex embedded systems software such as operating system kernels, low-level device drivers, or micro-controller code.

The aim of SSV workshops and conference series is to bring together researchers and developers from both academia and industry who are facing real software and real problems with the goal of finding real, applicable solutions.

This year we received 25 submissions and the Program Committee selected 13 submissions for pre- sentation at the conference. Each submission was reviewed by 3 Program Committee members. We wish to thank the Program Committee members and their sub-reviewers for their competent and timely reviews in the short allotted time-frame. We also thank the two invited speakers, Andreas Podelski (Uni- versity of Freiburg, Germany) and Lee Pike (Galois, Inc., USA) for accepting our invitation to give a presentation at SSV 2012.

SSV 2012 used the EasyChair conference system to manage the reviewing process. We are indebted to the EPTCS staff who provided flawless support in the preparation of this EPTCS volume. Finally, the SSV program chairs and organizers gratefully acknowledge the sponsorship of National ICT Australia Ltd (NICTA), Australia's Information and Communications Technology Research Centre of Excellence, and Red Lizard Software (www.redlizards.com).

F. Cassez, R. Huuck, G. Klein and B. Schlich
November 2012, Sydney, Australia

Organizing Committee and Program Committee Chairs

Franck Cassez NICTA, Sydney, Australia
Ralf Huuck NICTA and UNSW, Sydney, Australia
Gerwin Klein NICTA and UNSW, Sydney, Australia
Bastian Schlich ABB Corporate Research, Ladenburg, Germany

Program Committee

Cyrille Artho AIST, RISEC, Japan
Stefan Berghofer Secunet, Germany
Frédéric Boniol ONERA, France
Alessandro Coglio Kestrel, USA
Joe Hurd Intel, USA
Stefan Kowalewski RWTH Aachen University, Germany
Thomas Kropf Robert Bosch GmbH and University of Tübingen, Germany
Kim G. Larsen CISS, Aalborg University, Denmark
Toby Murray NICTA, Sydney, Australia
Jan Peleska Verified Systems Int. GmbH and University of Bremen, Germany
John Regehr University of Utah, USA
Natarajan Shankar SRI, USA
Zhong Shao Yale, USA
Konrad Slind Rockwell Collins, USA
Jun Sun Singapore University of Technology and Design, Singapore

Additional Reviewers

Sidney Amani NICTA, Sydney, Australia
Sebastian Biallas RWTH Aachen University, Germany
Marc Förster RWTH Aachen University, Germany
Volker Kamin RWTH Aachen University, Germany
Guan Jun Liu Singapore University of Technology and Design, Singapore
Hongjin Liang Research Center for High-Confidence Software, USTC-Yale, China
Tahina Ramananandro Yale, USA

Copilot: a Do-It-Yourself High-Assurance Compiler

Lee Pike (Galois, Inc.)

The "do-it-yourself" (DIY) culture encourages individuals to design and craft objects on their own, without relying on outside experts. DIY construction should be inexpensive with easy-to-access ma- terials. Ranging from hobbyist electronics to urban farming to fashion, DIY is making somewhat of a resurgence across the United States. We see no reason why DIY culture should not also extend to compilers, and in particular, to high-assurance compilers.

From 2009-2011, NASA contracted Galois, Inc. to research the possibility of augmenting complex aerospace software systems with runtime verification. Our answer to the contract goals was Copilot, an embedded domain-specific language (EDSL) to generate embedded monitorsThe Copilot language itself, focusing on its RV uses for NASA, has been described [1, 2, 3].

Our assurance challenge in the project was phrased as, "Who watches the watchmen?" meaning that if the RV monitor is the last line of defense, then it must not fail or worse, introduce unintended faults itself. Nonetheless, because the primary goal of the project was to implement an RV system and to field- test it, few resources were available for assuring the correctness of the Copilot compiler. Our approach was born out of necessity. Specifically, we employ three not-so-secret weapons from the functional languages and formal meth- ods communities in our work including building EDSLs, building sub-Turing complete languages, and taking a verifying compiler approach to assurance. This talk summarizes our experiences on this work and provides recommendations for lightweight assurance methods for domain-specific compiler design.


Program Analysis and Verification based on the Construction and Checking of Automata

Andreas Podelski (University of Freiburg, Germany)

A recent approach to the verification of programs constructs a correctness proof in the form of a finite automaton. The automaton recognizes a set of traces. Here, a trace is any sequence of statements (not necessarily feasible and not necessarily on a path in the control flow graph of the program).

A trace can be formalized as a word over the alphabet of statements. A trace can also be viewed as as special case of a program. Applying static analysis or a symbolic method (e.g., SMT solving with interpolant generation) to a single trace, a correctness proof for the trace can be obtained in the form of a sequence of consecutive Hoare triples (or, phrased differently, an inductive sequence of assertions).

Given a program and n traces of the program, we can construct an automaton from the n different correctness proofs for the traces. The automaton recognizes a set of correct traces. We still need to check whether this set includes all the traces on a path in the control flow graph of the program. The check is an automata-theoretic operation (which is reducible to non-reachability in a finite graph). That is, the two steps of constructing and checking a proof neatly separate the two concerns of data and control in program verification. The construction of a proof in the form of an automaton accounts for the interpretation of statements in data domains. The automaton, however, has a meaning that is oblivious to the interpretation of statements: a set of words over a particular alphabet. The check of the proof uses this meaning of the automaton and accounts for the control flow of the program. The implementation of the check of the proof as an automata-theoretic inclusion check is reminiscent of model checking (the finite control flow graph defines the model, the automaton defines the property).

The resulting verification method is not compositional in the syntax of the program; it is compositional in a new, semantics-directed sense where modules are sets of traces; the sets of traces are constructed from mutually independent correctness proofs and intuitively correspond to different cases of program executions. Depending on the verification problem (the correctness property being safety or termination for sequential, recursive, or concurrent programs), the approach uses non-deterministic automata, nested-word automata, Büchi automata, or alternating automata as proofs.