Abstracts

For Invited Speakers

1:Refinement-based CFG Reconstruction from Executable Files
 Sebastien Bardin
 Abstract: Automatic analysis of programs from their executable files has many potential industrial applications, for example: automatic analysis of mobile code and malware, security testing, third-party certification or worst case execution time estimation. Control-Flow Graph reconstruction appears to be a cornerstone of safe binary-level analysis: if the recovery is unsafe, subsequent analyses will be unsafe too; if it is too rough, they will be blurred by too many unfeasible branches and instructions. We address the issue of recovering a both safe and precise approximation of the CFG of a program given as an executable file. The problem is tackled in an original way, with a refinement-based static analysis working over finite sets of constant values. Requirement propagation allows the analysis to automatically adjust the domain precision only where it is needed, resulting in precise CFG recovery at moderate cost. First experiments, including an industrial case study, show that the method outperforms standard analyses in terms of precision, efficiency or robustness.
2:VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java
 Bart Jacobs
 Abstract: VeriFast is a verifier for single-threaded and multithreaded C and Java programs annotated with preconditions and postconditions written in separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma functions, i.e., functions that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma functions terminate and do not have side-effects. Verification proceeds by symbolic execution, where the heap is represented as a separation logic formula. Since neither VeriFast itself nor the underlying SMT solver do any significant search, verification time is predictable and low. The VeriFast IDE allows users to step through failed symbolic execution paths, and to inspect the symbolic state at each step. This yields a relatively comfortable interactive annotation authoring experience. We are currently using VeriFast to verify fine-grained concurrent data structures, unloadable kernel modules, and JavaCard programs.
3:Making Sense of Relaxed-Memory Concurrency
 Peter Sewell
 Abstract: I will introduce some of the issues of relaxed-memory concurrency, as they appear in mainstream processors (x86, Power, ARM) and programming languages (C, C++, Java), discussing what has to be done, first to establish usable semantic models, and then for reasoning above them.

For Accepted Papers

4:Verification of Dependable Software using Spark and Isabelle
 Stefan Berghofer
 Paper: PDF
 Abstract: We present a link between the interactive proof assistant Isabelle/HOL and the Spark/Ada tool suite for the verification of high-integrity software. Using this link, we can tackle verification problems that are beyond reach of the proof tools currently available for Spark. To demonstrate that our methodology is suitable for real-world applications, we show how it can be used to verify an efficient library for big numbers. This library is then used as a basis for an implementation of the RSA public-key encryption algorithm in Spark/Ada.
5:A Tool for the Certification of Sequential Function Charts based System Specifications
 Jan Olaf Blech
 Paper: PDF
 Abstract: We describe a tool framework for certifying properties of sequential function chart (SFC) based system specifications: CertPLC. CertPLC handles programmable logic controller (PLC) descriptions provided in the SFC language of the IEC 61131-3 standard. It provides routines to certify properties of systems by delivering an independently checkable formal system description and proof (called certificate) for the desired properties. We focus on properties that can be described as inductive invariants. System descriptions and certificates are generated and handled using the COQ proof assistant. Our tool framework is used to provide supporting evidence for the safety of embedded systems in the industrial automation domain to third-party authorities.
6:Adaptable Value-Set Analysis for Low-Level Code
 Paper: PDF
 Jörg Brauer, Rene Rydhof Hansen, Stefan Kowalewski, Kim Guldstrand Larsen, Mads Chr. Olesen
 Abstract: This paper presents a framework for binary code analysis based on SAT solving. Within our tool, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, which connects the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties about medium-sized programs for different microcontroller platforms.
7:Structuring Interactive Correctness Proofs by Formalizing Coding Idioms
 Holger Gast
 Paper: PDF
 Abstract: This paper examines a novel strategy for developing correctness proofs in interactive software verification for C programs. Rather than proceeding backwards from the generated verification conditions, we start by developing a library of the employed data structures, coding patterns, and idioms. The application of that library then leads to a straightforward correctness proof, in the sense that the proof follows informal arguments. We apply this strategy to the low-level memory allocator of the L4 microkernel, a case study discussed previously in the literature.
8:Automatic Derivation of Abstract Semantics From Instruction Set Descriptions
 Dominique Gückel and Stefan Kowalewski
 Paper: PDF
 Abstract: Abstracted semantics of instructions of processor-based architectures are an invaluable asset for several formal verification techniques, such as software model checking and static analysis. In the field of model checking, abstract versions of instructions can help counter the state explosion problem, for instance by replacing explicit values by symbolic representations of sets of values. Similar to this, static analyses often operate on an abstract domain in order to reduce complexity, guarantee termination, or both. Hence, for a given microcontroller, the task at hand is to find such abstractions. Due to the large number of available microcontrollers, some of which are even created for specific applications, it is impracticable to rely on human developers to perform this step. Therefore, we propose a technique that starts from imperative descriptions of instructions, which allows to automate most of the process.
9:Verification of Safety-Critical Systems: A Case Study Report on Using Modern Model Checking Toolss
 Paper: PDF
 Antti Jääkeläinen, Mika Katara, Shmuel Katz and Heikki Virtanen
 Abstract: Formal methods are making their way into the development of safety-critical systems. In this paper, we describe a case study where a simple 2oo3 voting scheme for a shutdown system was verified using two bounded model checking tools, CBMC and EBMC. The system represents Systematic Capability level 3 according to IEC 61508 ed2.0. The verification process was based on requirements and pseudo code, and involved verifying C and Verilog code implementing the pseudo code. The results suggest that the tools were suitable for the task, but require considerable training to reach productive use for code embedded in industrial equipment. We also identified some issues in the development process that could be streamlined with the use of more formal verification methods. Towards the end of the paper, we discuss the issues we found and how to address them in a practical setting.
Sponsored by:
NICTA
Supported by:
FBK RWTH-AACHEN Technische Universitat Dresden RWTH-AACHEN
Published by:
[to be announced]
Valid XHTML 1.0 Transitional Valid CSS! [Valid RSS]
Inspired by the FMICS 2010 web pages by Marco Roveri