Abstracts

In contrast to testing, mathematical reasoning and formal verification can show the absence of whole classes of security vulnerabilities. We present the, to our knowledge, first complete, formal, machine-checked verification of information flow security for the implementation of a general-purpose mi- crokernel; namely seL4. Unlike previous proofs of information flow security for operating system kernels, ours applies to the actual 9,600 lines of C code that implement seL4, and so rules out the possibility of invalidation by implementation errors in this code. We assume correctness of compiler, assembly code, hardware, and boot code. We prove everything else. This proof is strong evidence of seL4’s utility as a separation kernel, and describes precisely how the general purpose kernel should be configured to enforce isolation and mandatory information flow control. We describe the information flow security statement we proved (a variant of intransitive noninterference), including the assumptions on which it rests, as well as the modifications that had to be made to seL4 to ensure it was enforced. We discuss the practical limitations and implications of this result, including covert channels not covered by the formal proof.

Zélus is a new programming language for modeling systems that mix discrete logical time and continuous time behaviors. From a user's perspective, its main originality is to extend an existing Lustre-like synchronous language with Ordinary Differential Equations (ODEs). The extension is conservative: any synchronous program expressed as data-flow equations and hierarchical automata can be composed arbitrarily with ODEs in the same source code.

A dedicated type system and causality analysis ensure that all discrete changes are aligned with zero-crossing events so that no side effects or discontinuities occur during integration. Programs are statically scheduled and translated into sequential code which, by construction, runs in bounded time and space. Compilation is effected by source-to-source translation into a small synchronous subset which is processed by a standard synchronous compiler architecture. The resulting code is paired with an off-the-shelf numeric solver.

We show that it is possible to build a modeler for explicit hybrid systems à la Simulink/Stateflow on top of an existing synchronous language, using it both as a semantic basis and as a target for code generation.

An infrared sensor is modeled and analyzed in Uppaal. The sensor typifies the sort of component that engineers regularly integrate into larger systems by writing interface hardware and software.

In all, three main models are developed. For the first, the timing diagram of the sensor is interpreted and modeled as a timed safety automaton. This model serves as a specification for the complete system. A second model that emphasizes the separate roles of driver and sensor is then developed. It is validated against the timing diagram model using an existing construction that permits the verification of timed trace inclusion, for certain models, by reachability analysis (i.e., model checking). A transmission correctness property is also stated by means of an auxiliary automaton and shown to be satisfied by the model.

A third model is created from an assembly language driver program, using a direct translation from the instruction set of a processor with simple timing behavior. This model is validated against the driver component of the second timing diagram model using the timed trace inclusion validation technique. The approach and its limitations offer insight into the nature and challenges of programming in real time.

Large-scale verification projects pose particular challenges. Issues include proof exploration, efficiency of the edit-check cycle, and proof refactoring for documentation and maintainability. We draw on insights from two large-scale verification projects, L4.verified and Verisoft, that both used the Isabelle/HOL prover. We identify the main challenges in large-scale proofs, propose possible solutions, and discuss the Levity tool, which we developed to automatically move lemmas to appropriate theories, as an example of the kind of tool required by such proofs.

Hybrid modeling tools like Simulink have evolved from simulation platforms into development platforms on which testing, verification and code generation are also performed. It is critical to ensure that the results of simulation, compilation and verification are consistent. Synchronous languages have addressed these issues but only for discrete systems.

Reprising earlier work, we present a hybrid modeler built from a synchronous language and an off-the-shelf numerical solver. The main novelty is a language with hierarchical automata that can be arbitrarily mixed with data-flow and ordinary differential equations (ODEs). A type system statically ensures that discrete state changes are aligned with zero-crossing events and that the function passed to the numerical solver has no side-effects during integration. Well-typed programs are compiled by source-to-source translation into synchronous code which is then translated into sequential code using an existing synchronous language compiler.

Hybrid system modelers have become a corner stone of complex embedded system development. Embedded systems include not only control components and software, but also physical devices. In this area, Simulink is a de facto standard design framework, and Modelica a new player. However, such tools raise several issues related to the lack of reproducibility of simulations (sensitivity to simulation parameters and to the choice of a simulation engine).

In this paper we propose using techniques from non-standard analysis to define a semantic domain for hybrid systems. Non-standard analysis is an extension of classical analysis in which infinitesimal (the ε and η in the celebrated generic sentence ∀ε ∃η ... of college maths) can be manipulated as first class citizens. This approach allows us to define both a denotational semantics, a constructive semantics, and a Kahn Process Network semantics for hybrid systems, thus establishing simulation engines on a sound but flexible mathematical foundation. These semantics offer a clear distinction between the concerns of the numerical analyst (solving differential equations) and those of the computer scientist (generating execution schemes).

We also discuss a number of practical and fundamental issues in hybrid system modelers that give rise to non reproducibility of results, nondeterminism, and undesirable side effects. Of particular importance are cascaded mode changes (also called zero-crossings in the context of hybrid systems modelers).

Hybrid modelers such as Simulink have become corner stones of embedded systems development. They allow both discrete controllers and their continuous environments to be expressed in a single language. Despite the availability of such tools, there remain a number of issues related to the lack of reproducibility of simulations and to the separation of the continuous part, which has to be exercised by a numerical solver, from the discrete part, which must be guaranteed not to evolve during a step.

Starting from a minimal, yet full-featured, Lustre-like synchronous language, this paper presents a conservative extension where data-flow equations can be mixed with ordinary differential equations (ODEs) with possible reset. A type system is proposed to statically distinguish discrete computations from continuous ones and to ensure that signals are used in their proper domains. We propose a semantics based on non-standard analysis which gives a synchronous interpretation to the whole language, clarifies the discrete/continuous interaction and the treatment of zero-crossings, and also allows the correctness of the type system to be established.

The extended data-flow language is realized through a source-to-source transformation into a synchronous subset, which can then be compiled using existing tools into routines that are both efficient and bounded in their use of memory. These routines are orchestrated with a single off-the-shelf numerical solver using a simple but precise algorithm which treats causally-related cascades of zero-crossings. We have validated the viability of the approach through experiments with the Sundials library.

Recently, we have proposed a new design theory for timed systems. This theory, building on Timed I/O Automata with game semantics, includes classical operators like satisfaction, consistency, logical composition and structural composition. This paper presents a new efficient algorithm for checking Büchi objectives of timed games. This new algorithm can be used to enforce liveness in an interface, or to guarantee that the interface can indeed be implemented. We illustrate the framework with an infrared sensor case study.

Embedded controllers coordinate the behaviours of specialised hardware components to satisfy broader application requirements. They are difficult to model and to program. One of the greatest challenges is to express intricate timing behaviours—which arise from the physical characteristics of components—while not precluding efficient implementations on resource-constrained platforms. Aspects of this challenge are addressed by this thesis through four distinct applications of timed automata and the synchronous languages Argos and Esterel.

A novel framework for simulating controllers written in an imperative synchronous language is described. It includes a transformation of synchronous models into timed automata that accounts for timing properties which are important in constrained implementations but ignored by the usual assumption of synchrony. The transformation provides an interface between the discrete time of synchronous programs and a continuous model of time. This interface is extended to provide a way for simulating Argos programs within the widely-used Simulink software.

Timed automata are well-suited for semantic descriptions, like the aforementioned transformation, and for modelling abstract algorithms and protocols. This thesis also includes a different type of case study. The timing diagram of a small-scale embedded component is modelled in more detail than usual with the aim of studying timing properties in this type of system. Multiple models are constructed, including one of an assembly language controller. Their interrelations are verified in Uppaal using a construction for timed trace inclusion testing.

Existing constructions for testing timed trace inclusion do not directly address recent features of the Uppaal modelling language. Novel solutions for the problems presented by selection bindings, quantifiers, and channel arrays in Uppaal are presented in this thesis. The first known implementation of a tool for automatically generating a timed trace inclusion construction is described.

The timed automata case study demonstrates one way of implementing application timing behaviours while respecting implementation constraints. A more challenging, but less detailed, example is proposed to evaluate the adequacy of Esterel for such tasks. Since none of the standard techniques are completely adequate, a novel alternative for expressing delays in physical time is proposed. Programs in standard Esterel are recovered through syntactic transformations that account for platform constraints.

The timing details in many embedded applications are inseparable from other behavioural aspects. Time is also a resource; a physical constraint on system design that introduces limitations and costs. Design and implementation choices are often explored and decided simultaneously, complicating both tasks and encouraging platform specific programs where the meaning of a specification is mixed with the mechanisms of implementation.

The Esterel programming language is ideal for describing complex reactive behaviours. But, perhaps surprisingly, timing details cannot be expressed without making significant implementation choices at early stages of design. We illustrate this point with an example application where reactive behaviour and physical time are intertwined.

A simple solution is proposed: add a statement for expressing delays in physical time. While there are similar statements or library calls in many programming languages, the novelty of our proposal is that the delay statements are later replaced with standard Esterel statements when platform details become available. Delays are thus expressed directly in terms of physical time, but later implemented as a discrete controller using existing techniques. This approach is familiar in control system design where analytical models are constructed in continuous time and then later discretized to produce implementations.

We present some ideas for performing the translation and outline some of the remaining challenges and uncertainties.

Relations between models are important for effective automatic validation, for comparing implementations with specifications, and for increased understanding of embedded systems designs. Timed automata may be used to model a system at multiple levels of abstraction, and timed trace inclusion is one way to relate the models.

It is known that a deterministic and tau-free timed automaton can be transformed such that reachability analysis can decide timed trace inclusion with another timed automaton. Performing the transformation manually is tedious and error-prone. We have developed a tool that does it automatically for a large subset of Uppaal models.

Certain features of the Uppaal modeling language, namely selection bindings and channel arrays, complicate the transformation. We formalize these features and extend the validation technique to incorporate them. We find it impracticable to manipulate some forms of channel array subscripts, and some combinations of selection bindings and universal quantifiers; doing so either requires premature parameter instantiation or produces models that Uppaal rejects.

Current operating systems lack well-defined protocols for interaction with device drivers. We argue that this hinders the development of reliable drivers and thereby undermines overall system stability. We present an approach to specify driver protocols using a formalism based on state machines. We show that it can simplify device programming, facilitate static analysis of drivers against protocol specifications, and enable detection of incorrect behaviours at runtime.

We describe a simple scheme for mapping synchronous language models, in the form of Boolean Mealy Machines, into timed automata. The mapping captures certain idealised implementation details that are ignored, or assumed away, by the synchronous paradigm. In this regard, the scheme may be compared with other approaches such as the AASAP semantics. However, our model addresses input latching and reaction triggering differently. Additionally, the focus is not on model-checking but rather on creating a semantic model for simulating synchronous controllers within Simulink.

The model considers both sample-driven and event-driven execution paradigms, and clarifies their similarities and differences. It provides a means of analysing the timing behaviour of small-scale embedded controllers. The integration of the timed automata models into Simulink is described and related work is discussed.

Simulink is widely used within industry for simulation and model-driven development, and reactive behaviours are often modelled using an add-on called Stateflow. Argos is one of the synchronous languages that have been proposed for the specification, validation and implementation of reactive systems. It is a rigorously defined graphical notation which, although not as powerful as Stateflow, is much less complicated. This paper describes the implementation of an Argos block for Simulink.