Ebook: Engineering Methods and Tools for Software Safety and Security

As a consequence of the wide distribution of software and software infrastructure, information security and safety depend on the quality and excellent understanding of its functioning. Only if this functionality is guaranteed as safe, customer and information are protected against adversarial attacks and malfunction. A vast proportion of information exchange is dominated by computer systems. Due to the fact that technical systems are more or less interfaced with software systems most information exchange is closely related to software and computer systems. Information safety and security of software systems depend on the quality and excellent understanding of its functioning.

The last few years have shown a renewed interest in formally specifying and verifying software and its role in engineering methods. Within the last decade, interactive program verifiers have been applied to control software and other critical applications, software model checking has made strides into industrial applications, and a number of research tools for bug detection have been built using automatic program-verification technology. Such solutions are high level programming methods and provide strategies to ensure information security in complex software systems by automatically verified correctness.

Based on the specific needs in applications of software technology, models and formal methods must serve the needs and the quality of advanced software engineering methods. The objective of our Summer School 2008 Engineering Methods and Tools for Software Safety and Security was an in-depth presentation of state-of-the-art topics on how to meet such challenges covering both theoretical foundations and industrial practice.

With Methods and Tools for System and Software Construction JEAN-RAYMOND ABRIAL's contribution gives an introduction to the construction of complex systems using a formalism called Event-B and a tool called the Rodin Platform. The intent of his contribution is to explain all this in great details by means of various practical examples and tool demonstrations. The contribution is not made of examples and demonstrations only: the theory behind Event-B and the tool are also exposed in details.

GERARD BERRY presents with Synchronous Techniques for Software and Hardware Embedded Systems the synchronous programming approach to embedded systems design, based on specific languages and programming and verification environments. The synchronous approach is based on zero-delay deterministic information transmission between concurrent processes. It is now widely used for the design and verification of embedded systems in two main application areas: safety-critical embedded software (avionics, railways, heavy industry, and automotive applications), and high-level synthesis of Systems-on-Chips components. The synchronous tools are fully integrated in industrial development flows, ranging from specification-level design to formal verification.

For digital interactive distributed systems the timing of their events and the causality between their events are key issues. With his contribution on Relating Time and Causality in Interactive Distributed Systems MANFRED BROY demonstrates the relationship between causality and the timing of input and output events, as well as its relationship to the granularity of time. He deals, in particular, with the problem of time abstraction and the precise timing of events. How causality and time forms the basis of inductive reasoning, specially in the case of dependencies in communication cycles (“feedback”), is also presented as well as how it is able to work with time in models of distributed systems with a flexible choice of local clocks and local timing.

Following the results of Jean-Raymond's topic, MICHAEL BUTLER shows in his contribution on Incremental Design of Distributed Systems how Event-B can be used to model and reason about distributed systems from a high-level global view down to a detailed distributed architectural view. It is shown how refinement and decomposition could be used to introduce distribution of state and control and to introduce message passing between components. Performing refinement in incremental steps means that the abstraction gap between refinement levels is not too great. This means that the proof effort can be factored out into many relatively simple steps. Simple proof steps allow for a high degree of automation in proof.

Proving Program Termination and Liveness is the contribution of BYRON COOK. Byron introduces available automatic methods for proving that programs eventually do something good (e.g. that programs don't hang, that programs don't forget to release locks, etc.). Introduced topics include rank-function synthesis, variance analysis and refinement, fair termination, concurrency, and the support for programs with dynamically allocated data structures.

TONY HOARE's contribution on Separation Logic and Trace Semantics is concerned with developing a family of simple models of the separating conjunction of separation logic. He illustrates their utility in formalisation of many modern programming language features, including concurrency, sharing of memory, communication, dynamic allocation and disposal of resources, and the transfer of their ownership. He avoids the particularities of any existing or proposed new programming language, but instead attempts to clarify general principles of programming, those that govern the execution of programs expressed in any procedural programming language that includes given feature. The principles are expressed as sanity conditions on timed traces of program execution, and on the predicates describing them.

The contribution of KIM G. LARSEN on Verification, Performance Analysis and Controller Synthesis for Real-Time Systems provides a thorough tutorial of the tool UPPAAL and its application to modelling, verification, optimal scheduling and synthesis of real-time and embedded systems. The theory underlying UPPAAL is focussed, including: timed automata, priced automata and game automata together. Efficient algorithms and data structures for the analysis of these models were thoroughly covered as well as applications of the tool.

In his contribution on Specification and Verification of Object-Oriented Software RUSTAN LEINO presents an object-based language, Dafny, whose specifications use the style of dynamic frames. He shows how to write and specify programs in Dafny, and demonstrates how to build a first-order automatic program verifier for Dafny programs, generating the verification conditions as input to an automatic satisfiability-modulo-theories solver.

J. STROTHER MOORE presents Mechanized Operational Semantics. He explains how to formalize an “operational” or semantics of a von Neumann programming language in a functional programming language. Such semantics permit both simulation and code proofs. Moore formalizes a simple programming language related to the Java Virtual Machine and shows how it could be elaborated. He focuses on how to prove properties of programs and concluded with a proof of the correctness of the Boyer-Moore fast string searching algorithm.

JOHN REYNOLDS explains in his contribution on Separation Logic – A Logic for Shared Data and Local Reasoning that separation logic is an extension of Hoare logic originally intended for reasoning about programs that use shared mutable data structures. It is based on the concept of separating conjunction, which permits the concise expression of aliasing constraints. He shows that the logic also includes a “frame rule”, which enables local reasoning that is the key to the scalability of proofs. Examples of nontrivial proofs include the Schorr-Waite marking algorithm and the Cheney relocating garbage collector. John Reynolds describes that more recently the logic has been extended to encompass information hiding, shared-variable concurrency, and numerical permissions.

JIM WOODCOCK demonstrated The Verified Software Repository. His contribution describes experiments in mechanically verifying several different kinds of systems as part of building a Verified Software Repository. He starts by proposing a series of open challenges and finishes by drawing some conclusions about the current state of the art in modelling and verification, and the need for inter-operability of notations and tools.

The contributions in this volume have emerged from the lectures of the 29th International Summer School helt at Marktoberdorf from August 5 to August 17, 2008. 109 participants from 34 countries attended—including students, lecturers and staff. The Summer School provided two weeks of learning, discussion and development of new ideas, and was a fruitful event, at both the professional and social level.

We would like to thank all lecturers, staff, and hosts in Marktoberdorf. In particular special thanks goes to Dr. Katharina Spies, Silke Müller, and Katjana Stark for their great and gentle support.

The Marktoberdorf Summer School was arranged as an Advanced Study Institute of the NATO Science for Peace and Security Programme with support from the Deutscher Akademischer Austausch Dienst (DAAD), the Microsoft Research Ltd. under the Inspire Programme and the town and county of Marktoberdorf. We thank all authorities involved.

The Editors

In this text, we present a complete development with Event-B [1] [2] [3]: a mechanical press. The intention is to show how this can be done in a systematic fashion in order to obtain correct final code. In section 1, we present an informal description of this system. In section 2, we develop two general patterns [4] that we shall subsequently use. The development of these patterns will be made by using the proofs as a mean of discovering the invariants and the guards of the events. In section 3, we define the requirement document in a more precise fashion by using the terminology developed in the definition of the patterns. The main development of the mechanical press will take place in further sections where more design patterns will be presented.

We survey the synchronous approach to embedded hardware and software systems, its scientific content, and its use in industry. We discuss the concurrency and determinism constraints of embedded applications, and the way in which they are reconciled by the synchronous concurrency model. We present the main synchronous languages, their semantics, and the industrial tools and flows that support them.

For digital interactive distributed systems the timing of their events and the causality between their events are key issues. In real time applications of embedded software systems timing properties are essential such as response times of reactions depending on the precise timing of the input events.

In a highly abstract view, a digital system can be represented by a set of events annotated by their timing. Sets of timed events labeled by actions represent the observations about systems. An essential property that helps to understand distributed interactive systems and a way to reason about their event flow is causality. Causality addresses the questions under which conditions certain events must, may or must not happen. Causality addresses the logical dependencies between the events in systems. Strictly speaking, causality reflects the logical essence in the event and action flow of systems.

Causality is closely related to time. In particular, we study in the following the relationship between causality and the timing of input and output events, as well as its relationship to the granularity of time. We deal, in particular, with the problem of time abstraction and the precise timing of events. We show how causality and time form the basis of inductive reasoning, in particular, in the case of dependencies in communication cycles (“feedback”) and how we can work with time in models of distributed systems with a flexible choice of local clocks and local timing.

It is shown how Event-B can be use to model and reason about distributed systems from a high-level global view down to a detailed distributed architectural view. It is shown how refinement and decomposition can be used to introduce distribution of state and control and to introduce message passing between components. Distribution is treated as a special case of concurrency. Techniques are presented for decomposing abstract atomic events into smaller atomic steps in refinement and for decomposing models into sub-models.

In this paper we introduce the basic concepts behind the problem of proving program termination, including well-founded relations, well-ordered sets, and ranking functions. We also connect the notion of termination of computer programs with that of well-founded relations. This paper introduces no original concepts, nor does it propose solutions towards the the problem of automating termination proofs. It does, however, provide a foundation from which the reader can peruse the more advanced literature on the topic.

Labelled graphs are used to model control and data flow among events occurring in the execution of a (possibly concurrent) program. Data flow is a unifying concept that covers both access to memory and communication along channels; it covers many variations including weakly consistent memory, re-ordered execution, and communication channels that are multiplexed, buffered, or otherwise unreliable. Nevertheless, the laws of Hoare and Jones correctness reasoning remain valid when interpreted in this general model. The key is use of the same language and logic for the specification of programs as for description of the behavior of programs. We make no attempt to lift the level of abstraction above that of the atomic events involved in program execution.

This note aims at providing a concise and precise Travellers Guide, Phrase Book or Reference Manual to the timed automata modeling formalism introduced by Alur and Dill [7,8]. The note gives comprehensive definitions of timed automata, priced (or weighted) timed automata, and timed games and highlights a number of results on associated decision problems related to model checking, equivalence checking, optimal scheduling, and winning strategies.

The specification of object-oriented and other pointer-based programs must be able to describe the structure of the program's dynamically allocated data as well as some abstract view of what the code implements. The verification of such programs can be done by generating logical verification conditions from the program and its specifications and then analyzing the verification conditions by a mechanical theorem prover.

In these lecture notes, I present an object-based language, Dafny, whose specifications use the style of dynamic frames. I show how to write and specify programs in Dafny. Most of the material is devoted to how to build a first-order automatic program verifier for Dafny programs, generating the verification conditions as input to an automatic satisfiability-modulo-theories solver.

We describe a mechanically checked proof that the Boyer-Moore fast string searching algorithm is correct. This is done by expressing both the fast algorithm and the naïve (obviously correct) algorithm as functions in applicative Common Lisp and proving them equivalent with the ACL2 theorem prover. The algorithm verified differs from the original Boyer-Moore algorithm in one key way: the original algorithm preprocessed the pattern into two arrays and skipped forward by the maximum of the skip distances recorded in those arrays; the algorithm verified uses one array that combines the two original arrays (and awhose size is the product of that of the original arrays). The algorithm here skips at least as far as the original Boyer-Moore algorithm and often skips further, though we do not prove that mechanically. A key fact about the original algorithm is that preprocessing can be done in time linear in the length of the pattern, |pat|, and the size of the alphabet, |α|. Our implementation of the preprocessing here is unconcerned with efficiency and has complexity |α|×|pat|². Our mechanically checked proof includes a proof that our preprocessing is correct. We briefly describe a proof (shown in detail elsewhere) that an imperatively coded version of the fast algorithm implements the algorithm verified here.

Separation logic, originally developed by O'Hearn and Reynolds, is an extension of Hoare logic originally intended for reasoning about programs that use shared mutable data structures. It was based on the concept of separating conjuction, which permits the concise expression of aliasing constraints.

The logic also includes a “frame rule”, which enables local reasoning that is the key to the scalability of proofs. Examples of nontrivial proofs include the Schorr-Waite marking algorithm and the Cheney relocating garbage collector.

More recently, by generalizing the concept of storage access to ownership and permissions, the logic has been extended to encompass information hiding, shared-variable concurrency, and numerical permissions.

We propose a unifying theory of undefined expressions in logics used for formally specifying software systems. We show how to use classical logic to prove facts in a monotonic partial logic with guards, and we exhibit guards for several different semantical systems. We show how classical logic can be used to prove semi-classical facts. The mechanical theorem prover Z/Eves is used to prove facts about semi-classical Z specifications, although it uses classical logic; it does this with guards from McCarthy logic. It can also be used to prove facts about VDM specifications. The use of left-to-right guards guarantees, for example, that every theorem proved in Z/Eves is valid in VDM and in Z.