WORKSHOP PROGRAM ABSTRACTS

Typed Assembly Language for Implementing OS Kernels in SMP/Multi-Core Environments with Interrupts
Back to Program
Although many people still think that it is difficult or even impossible to implement OS kernels in a strictly typed programming language, we dispelled the myth in our previous works by designing and implementing a typed assembly language which is flexible enough to implement essential functionalities of OS kernels (e.g., memory and multi-thread management facilities). Taking a step further, in this paper, we show an extended typed assembly language which supports SMP/multi-core environments with CPU hardware interrupts and illustrate how to implement synchronization primitives, which are essential for implementing OS kernels in the environments.

Counterexample-Guided Abstraction Refinement for PLCs
Back to Program
This paper presents a method for model checking programs for programmable logic controllers (PLCs) using the counterexample-guided abstraction refinement (CEGAR) approach. The technique is tailored to this specific hardware platform by accounting for the cyclic scanning mode that is symptomatic to PLCs. In particular, the hardware model poses the need for on-the-fly abstraction refinement in order to guarantee a deterministic control flow. It also allows to treat refinement phases triggered by input and global variables differently, leading to a more effective implementation. The effectiveness of this approach is shown in a case study, which highlights the verification process for function blocks that implement a specification provided by the industrial consortium PLCopen.

dBug: Systematic Evaluation of Distributed Systems
Back to Program
This paper presents the design, implementation and evaluation of "dBug" — a tool that leverages manual instrumentation for systematic evaluation of distributed and concurrent systems. Specifically, for a given distributed concurrent system, its initial state and a workload, the dBug tool systematically explores possible orders in which concurrent events triggered by the workload can happen. Further, dBug optionally uses the partial order reduction mechanism to avoid exploration of equivalent orders. Provided with a correctness check, the dBug tool is able to verify that all possible serializations of a given concurrent workload execute correctly. Upon encountering an error, the tool produces a trace that can be replayed to investigate the error. We applied the dBug tool to two distributed systems — the Parallel Virtual File System (PVFS) implemented in C and the FAWN-based key-value storage (FAWN-KV) implemented in C++. In particular, we integrated both systems with dBug to expose the non-determinism due to concurrency. This mechanism was used to verify that the result of concurrent execution of a number of basic operations from a fixed initial state meets the high-level specification of PVFS and FAWN-KV. The experimental evidence shows that the dBug tool is capable of systematically exploring behaviors of a distributed system in a modular, practical, and effective manner.

Model-based Testing Without a Model: Assessing Portability in the Seattle Testbed
Back to Program
Despite widespread OS, network, and hardware heterogeneity, there has been a lack of research into quantifying and improving portability of a programming environment. We have constructed a distributed testbed called Seattle built on a platform-independent programming API that is implemented on different operating systems and architectures. Our goal is to show that applications written to our API will be portable. In this work, we use an instrumented version of the programming environment for testing purposes. The instrumentation allows us to gather traces of actual program behavior from a running implementation. These traces can be used across different versions of the implementation exactly as if they were test cases generated offline from a model program, so we can commence testing using model based testing tools, without constructing a model program. Such offline testing is only effective in scenarios where traces are expected to be reproducible (deterministic). Where reproducibility is not expected, for instance due to nondeterminism in the network environment, we must resort to on-the-fly testing, which does require a model program. To validate this model program, we can use the recorded traces of actual behavior. Validating with captured traces should provide greater coverage than we could achieve by validating only with traces constructed a priori.

Correctness Proofs for Device Drivers in Embedded Systems
Back to Program
Computer systems do not exist in isolation: they must interact with the world through I/O devices. Our work, which focuses on constrained embedded systems, provides a framework for verifying device driver software at the machine code level. We created an abstract device model that can be plugged into an existing formal semantics for an instruction set architecture. We have instantiated the abstract model with a model for the serial port for a real embedded processor, and we have verified the full functional correctness of the transmit and receive functions from an open-source driver for this device.

Lyrebird—Assigning Meanings to Machines
Back to Program
This paper presents work in progress on the Lyrebird framework, consisting of a language for specifying the programmer-visible behaviour of a processor and its associated devices, a tool for automatically producing a fast simulator, and a formal semantic interpretation providing a machine model for use in an interactive theorem prover. Machine specifications are modular, providing abstract interfaces and structural parameterization (MMU-less processors, for example). Also presented is a specific example: An instantiation for the ARM1136jf-s core.

A Precise Memory Model for Low-Level Bounded Model Checking
Back to Program
Formalizing the semantics of programming languages like C or C++ for bounded model checking can be cumbersome if complete coverage of all language features is to be achieved. On the other hand, low-level languages that occur during translation (compilation) have a much simpler semantics since they are closer to the machine level. It thus makes sense to use these low-level languages for bounded model checking. In this paper we present a highly precise memory model suitable for bounded model checking of such low-level languages. Our method also takes memory protection (malloc/free) into account.

Verification of Stack Manipulation in the SCIP Processor
Back to Program
This paper presents a case study in the formal verification of the hardware description level specification of a general purpose computer processor. The major contributions of this paper are a framework for modelling VHDL hardware designs in the ACL2 language, a discipline for managing the layering of abstractions when verifying a hierarchical design, and a description of the significant theorems proved.

Towards Proving Security in the Presence of Large Untrusted Components
Back to Program
This paper proposes a generalized framework to build large, complex systems where security guarantees can be given for the overall system's implementation. The work builds on the formally proven correct seL4 microkernel and on its fine-grained access control. This access control mechanism allows large untrusted components to be isolated in a way that prevents them from violating a defined security property, leaving only the trusted components to be formally verified. The first steps of the approach are illustrated by the formalisation of a multi-level secure access device and a proof in Isabelle/HOL that information cannot flow from one back-end network to another.

Loop Refinement Using Octagons and Satisfiability
Back to Program
This paper presents a technique for refining the control structure of loops in programs operating over finite bit-vectors. This technique is based on abstract interpretation using octagons and affine equalities in order to identify infeasible sequences of loop iterations. Our approach naturally integrates wrap-around arithmetic during the generation of abstractions. Abstract interpreters operating on a refined control structure then typically derive strengthened program invariants without having to rely on complicated domain constructions such as disjunctive completions.

Comparing Model Checking and Static Program Analysis: A Case Study in Error Detection Approaches
Back to Program
Static program analysis and model checking are two different techniques in bug detection that perform error checking statically, without running the program. In general, static program analysis determines run-time properties of programs by examining the code structure while model checking needs to explore the relevant states of the computation. This paper reports on a comparison of such approaches via an empirical evaluation of tools that implement these techniques: CBMC — a bounded model checker and Parfait — a static program analysis tool. These tools are run over code repositories with known, marked in the code bugs. We indicate the performance of these tools and report on statistics of found and missed bugs. Our results illustrate the relative strengths of each approach.