Ebook: Software System Reliability and Security

Today almost every complex technical system used in industry, science, commerce and communication is more or less interfaced with software and software systems. This dictates that most information exchange is closely related to software and computer systems. The consequence of this wide distribution of software is a high dependency on its functioning and quality. Because of this dependency and distribution, making information systems safe, reliable, as well as secure and protecting information against all kinds of attack is an essential research topic, particularly in computer science.

Scientific foundations have been developed for programming and building computer systems. These foundations cover a broad spectrum of issues and work with formal models and description techniques in order to support a deep and precise understanding and managing of a system's properties and interplay. In addition, software engineering has many additional applications, ranging from telecommunications to embedded systems. For example software engineering has now become essential in automotive and aircraft industry, and has been intergral in furthering computer networks distributed over wide-area networks. A vast proportion of information exchange is influenced by computer systems and information security is important for reliable and secure software and computer systems.

Information security covers the protection of information against unauthorized disclosure, transfer, modification, and destruction, whether accidentally or intentionally. Attacks against computer systems can cause considerable economic and physical damage. Quality of life in general and of individual citizens, and the effectiveness of the economy critically depends on our ability to build software in a transparent and efficient way. Furthermore, we must be able to enhance the software development process systematically in order to ensure safety, security and reliability. This, in turn, requires very high software reliability, i. e., an extremely high confidence in the ability of the software to perform flawlessly. The foundations of software technology provide models that enable us to capture application domains and their requirements, but also to understand the structure and working of software systems, software architectures and programs. New developments must pay due diligence to the importance of security-related aspects, and align current methods and techniques to information security, integrity, and system reliability. However, 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, especially taking into account security aspects in Information Technology.

As a consequence of the wide distribution of software and software infrastructure, information security depends on the quality and excellent understanding of its functioning. Only when this functionality is guaranteed as safe, customers, and information are protected against adversarial attacks. Thus, to make communication and computation secure against catastrophic failure and malicious interference, it is essential to build secure software systems and methods for their development. Such development is difficult, mainly because of the conflict between development costs and verifiable correctness.

In the summer of 2006, a group of internationally renowned researchers in computer science met and lectured on the topics described above. The articles in this book describe the state-of-the-art ideas on how to meet these challenges in software engineering.

Rajeev Alur describes the foundations of model checking of programs with finite data and stack-based control flow. Manfred Broy introduces an abstract theory for systems, components, composition, architectures, interfaces, and compatibility. In his article he applies this theory to object orientation and elaborates on the application of that theory covering notions for a formal model of objects, classes, components, and architectures as well as those of interfaces of classes and components and their specification. Ernie Cohen explains how to use ordinary program invariants to prove properties of cryptographic protocols.

Networked computer systems face a range of threats from hostile parties on the network leading to violations of design goals such as confidentiality, privacy, authentication, access control, and availability. The purpose of Andrew Gordon's article is to introduce an approach to this problem based on process calculi. Transactions are the essential components of electronic business systems, and their safety and security are of increasing concern. Tony Hoare presents a theoretical model of compensable transactions, showing how long running transactions may be correctly composed out of shorter ones. Orna Kupferman presents on “Applications of Automata-Theory in Formal Verification”. In this automata-theoretic approach to verification, she reduces questions about programs and their specifications to questions about automata.

In a distributed system with no central management such as the Internet, security requires a knowledge about who can be trusted for each step in establishing it, and why. Butler W. Lampson explains the “speaks for” relation between principals describing how authority is delegated. Axel van Lamsweerde contributes model-based requirements engineering. Models for agents, operations, obstacles to goals, and security threats are introduced and a model building with the KAOS method is presented. Wolfgang Paul outlines a correctness proof for a distributed real time system – for the first time in a single place – from the gate level to the computational model of a CASE tool.

Amir Pnueli describes an approach for the synthesis of (hardware and software) designs from LTL specifications. This approach is based on modelling the synthesis problem which is similar to the problem of finding a winning strategy in a two-person game. K. Venkatesh Prasad introduces the notion of a “mobile networked embedded system”, in which a mobile entity is composed of internally and externally networked software components. He discusses the challenges related to designing a mobile networked embedded system with regards to security, privacy, usability, and reliability. Finally, Wolfram Schulte explains the “Spec# Approach”, which provides method contracts in the form of pre- and post-conditions as well as object invariants. He describes the design of Spec#'s state-of-the-art program verifier for object-oriented programs.

The contributions in this volume have emerged from lectures of the 27th International Summer School on Software System Reliability and Security, held at Marktoberdorf from August 1 to August 13, 2006. More than 100 participants from 28 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 our secretaries Dr. Katharina Spies, Silke Müller, and Sonja Werner for their great and gentle support.

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

THE EDITORS

While model-checking of pushdown models is by now an established technique in software verification, temporal logics and automata traditionally used in this area are unattractive on two counts. First, logics and automata traditionally used in model-checking cannot express requirements such as pre/post-conditions that are basic to software analysis. Second, unlike in the finite-state world, where the μ-calculus has a symbolic model-checking algorithm and serves as an “assembly language” of temporal logics, there is no unified formalism to model-check linear and branching requirements on pushdown models. In this survey, we discuss a recently-proposed re-phrasing of the model-checking problem for pushdown models that addresses these issues. The key idea is to view a program as a generator of structures known as nested words and nested trees (respectively in the linear and branching-time cases) as opposed to words and trees. Automata and temporal logics accepting languages of these structures are now defined, and linear and branching time model-checking phrased as language inclusion and membership problems for these languages. We discuss two of these formalisms—automata on nested words and a fixpoint calculus on nested trees—in detail. While these formalisms allow a new frontier of program specifications, their model-checking problem has the same worst-case complexity as their traditional analogs, and can be solved symbolically using a fixpoint computation that generalizes, and includes as a special case, “summary”-based computations traditionally used in interprocedural program analysis.

We introduce an abstract theory for systems, components, composition, architectures, interfaces, and compatibility. We apply this theory to object orientation and work out an instance of that theory that covers these notions in terms of a formal model of objects, classes, components, and architectures as well as of interfaces of classes and components and their specification. We define and analyze, in particular, interfaces for object oriented software systems and their architectures. We deal with “design by contract” as well as “specification by contract” and analyze their limitations. We show how to specify these interfaces by logical formulas in the style of specification by contract, by state machines and also by interaction diagrams. We treat composition given a formal definition of class composition and analyze semantic complications. We discuss, in particular, how we can extend concepts from object orientation towards components and more sophisticated ways to handle interfaces and hierarchical architectures. Our approach is based on the concept of states, state assertions, and state machines. A pragmatic goal is to explore simple and tractable ways to describe interfaces.

This tutorial describes how to reason about cryptographic protocols in perfect cryptography models using ordinary program invariants.

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.

The concept of a compensable transaction has been embodied in modern business workflow languages like BPEL. This article uses the concept of a box-structured Petri net to formalise the definition of a compensable transaction. The standard definitions of structured program connectives are extended to construct longer-running transactions out of shorter fine-grain ones. Floyd-type assertions on the arcs of the net specify the intended properties of the transaction and of its component programs. The correctness of the whole transaction can therefore be proved by simple local reasoning.

In formal verification, we check the correctness of a system with respect to a desired property by checking whether a mathematical model of the system satisfies a specification that formally expresses the property. In the automata-theoretic approach to formal verification, we model both the system and the specification by automata. Questions about systems and their specifications are then reduced to questions about automata. The goal of this course is to teach the basics of automata on infinite words and their applications in formal verification.

Requirements engineering (RE) is concerned with the elicitation of the objectives to be achieved by the system-to-be, the operationalization of such objectives into specifications of requirements and assumptions, the assignment of responsibilities for those specifications to agents such as humans, devices and software, and the evolution of such requirements over time and across system families. Getting high-quality requirements is difficult and critical. Poor requirements were recurrently recognized to be the major cause of system failures. The consequences of such failures may be especially harmful in mission-critical systems.

This paper overviews a systematic, goal-oriented approach to requirements engineering for high-assurance systems. The target of this approach is a complete, consistent, adequate, and structured set of software requirements and environment assumptions. The approach is model-based and partly relies on the use of formal methods when and where needed for RE-specific tasks, notably, goal refinement and operationalization, analysis of hazards and threats, conflict management, and synthesis of behavior models.

In these lecture notes we outline for the first time in a single place a correctness proof for a distributed real-time system from the gate level to the computational model of a CASE tool.

In these notes we present a viable approach to the synthesis of reactive programs from a temporal specification of their desired behavior. When successful, this direct correct-by-construction approach to system development obviates the need for post-facto verification.

In spite of the established double exponential lower bound that applies to the general case, we show that many useful specifications fall into a class of temporal formulas, technically identified as the Reactivity(1) class, for which we present an n³ synthesis algorithm.

The notion of nearly all things being networked almost all the time has been with us for over two decades now. Most networked entities had been fixed until the advent of cellular telephony. With cellular phones the fringes of the information age have begun to expand in pervasive forms. Adding the automobile to this context adds a new dimension to this domain of pervasive networks. In this chapter we introduce the notion of a mobile networked embedded systems (MNES) in which a mobile entity such as an automobile is composed of internally as well as externally networked software components. We further discuss the challenges going forward of designing a MNES-vehicle with regard to security, privacy, usability, and reliability (SPUR).

A verifying compiler automatically verifies the correctness of a source program before compiling it. Founded on the definition of the source language and a set of rules (a methodology) for using the language, the program's correctness criteria and correctness argument are provided in the program text by interface specifications and invariants.

This paper describes the program-verifier component of a verifying compiler for a core multi-threaded object-oriented language. The verifier takes as input a program written in the source language and generates, via a translation into an intermediate verification language, a set of verification conditions. The verification conditions are first-order logical formulas whose validity implies the correctness of the program. The formulas can be analyzed automatically by a satisfiability-modulo-theory (SMT) solver.

The paper defines the source language and intermediate language, the translation from the former into the latter, and the generation of verification conditions from the latter. The paper also builds a methodology for writing and verifying single- and multi-threaded code with object invariants, and encodes the methodology into the intermediate-language program.

The paper is intended as a student's guide to understanding automatic program verification. It includes enough detailed information that students can build their own basic program verifier.