Ebook: Software Safety and Security

Over the last decade, we have seen amazing advances in methods and tools for checking the safety and security of software systems. Automatic tools can now detect security flaws not only in programs of the order of a million lines of code, but also in high-level protocol descriptions. Full functional correctness is more difficult, but we have also seen much progress here, for example in the area of operating system verification, where only last year an OS kernel of 10,000 lines was proved correct; something of a breakthrough. The Summer School Marktoberdorf 2011 showed the wide range of computer science, with its foundations, methods and tools, to present the state-of-the-art in research and scientific practice of this challenging, future-oriented and key-topic in computer science. We assembled leading international experts who presented their in-depth knowledge and their experience in the overarching subject matter.

Conceptually, the courses of this NATO ADVANCED STUDY INSTITUTE ON TOOLS FOR ANALYSIS AND VERIFICATION OF SOFTWARE SAFETY AND SECURITY in 2011 were divided into 3 integrated modules:

Foundations of Safety and Security, lectured by Orna Grumberg, Marta Kwiatkowska, Tobias Nipkow, Peter O'Hearn, Helmut Seidl

Applications of Safety Analysis, taught by Gerwin Klein, Rustan Leino, Rupak Majumdar, Sharad Malik

Security Analysis, delivered by Bruno Blanchet, Hubert Comon-Lundh, Andrei Sabelfeld.

In his course, Mechanized Game-Based Proofs of Security Protocols, BRUNO BLANCHET presented techniques for automating proofs of security protocols in the computational model. He focused in particular on the automatic computationally sound prover CryptoVerif. CryptoVerif produces proofs presented as sequences of games, similar to the manual proofs of cryptographers. It provides a generic method for specifying the security properties of many cryptographic primitives, proves secrecy and authentication properties, and produces proofs valid for a number of sessions polynomial in the security parameter. Blanchet illustrated CryptoVerif on two simple examples: the encrypt-then-MAC scheme and the Full Domain Hash (FDH) signature scheme.

HUBERT COMMON-LUNDH lectured on Formal Security Proofs. The goal of his lecture was to present aspects of formal security proofs of protocols. This is a wide area, and there was the lecture (by B. Blanchet) on related topics. The idea was therefore to explain one particular technique, relying on deducibility constraints, in depth. In short: a deducibility constraint is a sequence of proofs in which some parts are unknown (and formalized with variables) and possibly reused in other constraints. An instance of such constraints yields an attacker's strategy. He explained how to solve such constraints in a particular setting of a few cryptographic primitives.

Model Checking was the topic explored by ORNA GRUMBERG. Computerized systems dominate almost every aspect of our lives and their correct behavior is essential. Model checking is an automated verification technique for checking whether a given system satisfies a desired property. In the lectures, different model checking techniques, which can improve model checking applicability in different ways, were surveyed. Grumberg started from the old-fashioned techniques of BDD-based Symbolic Model Checking and SAT based Bounded Model Checking. She then proceeded to using interpolation and interpolation sequence for SAT-based model checking.

The lecture Interactive Proof: Applications to Semantics by GERWIN KLEIN built on the previous introduction to interactive proofs and demonstrated a specific application of interactive proof assistants: the semantics of programming languages. In particular, he showed how to formalize imperative programming languages in the theorem prover Isabelle/HOL, how to define its semantics in different variations, and how to prove properties about the languages in the theorem prover. The emphasis of the lecture was not on formalizing a complex language in depth, but to teach a number of formalization techniques and proof strategies using simple examples. To this purpose, he covered big and small step semantics, typing and type safety, as well as a small machine language with a compiler and compiler correctness proof.

MARTA KWIATKOWSKA delivered a lecture on Advances in Probabilistic Model Checking, which is a formal verification technique for the analysis of systems that exhibit stochastic behavior, such as security and communication protocols. It enables a range of quantitative analyses of probabilistic models against specifications such as the worst-case probability of intrusion within 10 seconds or the minimum expected power consumption over all possible scheduling. In recent years, increasing interest in the topic of probabilistic verification has led to significant advances in the applicability and efficiency of these techniques, as well as the discovery of interesting and anomalous behavior in a wide range of real-life case studies.

With Using and Building an Automatic Program Verifier, RUSTAN LEINO offered a taste of what current technology can do for program correctness. One of the aims in these lectures was to teach the concepts needed to use a program verifier, and to give students some experience with a program verifier (the language and verifier Dafny). The message which the students took home was to remember verification and verification tools the next time a program is not entirely obvious. The second aim of these lectures was to teach the theoretical foundations of this shared infrastructure, described in terms of an intermediate verification language (the language and verification engine Boogie). The message here was: don't build your plumbing from scratch, leverage an intermediate verification language.

Software Model Checking was the topic of RUPAK MAJUMDAR. Software model checking is the algorithmic analysis of programs to prove properties of their executions. One major goal of software model checking research today is to expand the scope of automated techniques for program reasoning, both in the scale of programs handled and in the richness of properties that can be checked, reducing the burden on the expert human programmer. Majumdar presented some algorithmic advances from the last few decades that have made this possible, at least in certain domains.

Boolean Satisfiability Solvers: Techniques and Extensions was delivered by SHARAD MALIK. Boolean Satisfiability (SAT) is the problem of checking whether a propositional logic formula can ever evaluate to true. SAT manifests itself in several important application domains such as the design and verification of hardware and software systems. Several relatively recent research developments have enabled us to tackle instances with millions of variables and constraints – enabling SAT solvers to be effectively deployed in practical applications including in the analysis and verification of software systems. In the first part of this series of lectures, Malik covered the techniques used in modern SAT solvers. In the second part, he considered extensions of these solvers which have proved useful in analysis and verification.

In his course, Interactive Proof: Hands-on Introduction, TOBIAS NIPKOW introduced interactive proving with the Isabelle/HOL system. This involves 3 steps: verified functional programming, predicate logic and structured proofs. The course assumed basic familiarity with some functional programming language of the ML or Haskell family, in particular with recursive data types and pattern matching. No specific background in logic was necessary beyond the ability to read predicate logic formulas.

PETER O'HEARN gave Lectures on Separation Logic. Separation logic is an extension of Hoare's logic for reasoning about programs that mutate data held in computer memory. After a section covering the basics, O'Hearn delivered a lecture on semantic foundations. Using a model theoretic perspective, he attempted to describe the extent to which separation logic's ‘benefits’ do and do not depend on its language of assertions. The later lectures moved on to cover concurrency and mechanized verification, in particular the use of the logic in proof via symbolic execution and static program analysis.

ANDREI SABELFELD lectured on Information-Flow Security. He discussed a principled approach to web application security through tracking information flow. Sabelfeld showed that there are some fundamental challenges and tradeoffs which determine the possibilities and limitations of automatically securing web applications. He addressed challenges related to mutual distrust on the policy side (as in web mashups) and tracking information flow in dynamic web programming languages (such as JavaScript) to provide a foundation for practical web application security.

The first part of HELMUT SEIDL's lecture on Precise Fixpoint Computation through Strategy Iteration and Optimization considered the numerical properties of integer variables. Here he showed how a generalization of the Bellman-Ford algorithm allows the construction of a precise interval analysis. The second part of his lecture considered the numerical properties of variables holding fractional values – Bellman-Ford is no longer applicable. He succeeded in constructing a precise interval analysis by replacing that algorithm with techniques from linear programming.

As was demonstrated in the Summer School Marktoberdorf series, such presentations, as well as working and learning together, are essential for future scientific results in computer science, and consequently for the development of large-scale reliable and secure software systems. Once more it was proved that, over the years, this NATO Advanced Study Institute has facilitated the strengthening of such connections and applications, and influenced the quality of future research as well as the potential to transfer research into practice. The Summer School provided two weeks of learning, discussion and development of new ideas, and was a productive and beneficial event, at both the professional and social level.

We would like to take this opportunity to thank all the lecturers, the staff, and our hosts in Bayrischzell. Special thanks goes to: Dr. Katharina Spies, Silke Müller, and Katjana Stark for their invaluable support.

The Marktoberdorf Summer School was arranged as an Advanced Study Institute of the NATO Science for Peace and Security Programme with support from Deutscher Akademischer Austausch Dienst (DAAD) and Microsoft Research. We would also like to thank all the authorities involved.

THE EDITORS

After a short introduction to the field of security protocol verification, we present the automatic protocol verifier CryptoVerif. In contrast to most previous protocol verifiers, CryptoVerif does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games, like those manually done by cryptographers; these games are formalized in a probabilistic process calculus. CryptoVerif provides a generic method for specifying security properties of the cryptographic primitives. It can prove secrecy and correspondence properties (including authentication). It produces proofs valid for any number of sessions, in the presence of an active adversary. It also provides an explicit formula for the probability of success of an attack against the protocol, as a function of the probability of breaking each primitive and of the number of sessions.

The goal of the lecture is to present some aspects of formal security proofs of protocols. This is a wide area, and there is another lecture (by B. Banchet) on related topics. The idea is therefore to explain in depth one particular technique, that relies on deducibility constraints. We rely mainly on two introductory documents [8,14]. Actually, the current notes are the beginning of [8].

Here is a roadmap:

1. We introduce the problem with examples and touch a little the question of the validity of the security models (section 1).

We describe then a small process algebra, that will serve as a model for the protocols, as well as a few security properties (section 2).

2. The core of the lecture is here: we introduce the attacker model, as a deduction system, and show how to represent any execution in the hostile environment as deducibility constraints. In short, a deducibility constraint is a sequence of proofs, in which some parts are unknown (and formalized with variables) and possibly re-used in other constraints. An instance of such a constraints yields an attacker's strategy.

We explain how to solve such constraints in a particular setting of a few cryptographic primitives. This is more or less what is described in the first part of [12] and is detailed in the section 3.

Though the lecture aims at being self-contained, it assumes some familiarity with inference rules/ formal proofs (or SOS for programming languages) and terms/ substitutions/ unification. Similarly, a knowledge on concurrency is not required, but will make easier the understanding of the model.

In this paper we describe the development of model checking from BDD-based verification, through SAT-based bug finding, to Interpolation-based verification.

Model checking is an automatic approach to formally verifying that a given system satisfies a given specification. BDD-based Symbolic Model Checking (SMC) was the first to enable model checking of real-life designs with a few hundreds of state elements. Currently, SAT-based model checking is the most widely used method for verifying industrial designs. This is due to its ability to handle designs with thousands of state elements and more. Its main drawback, however, is its orientation towards “bug-hunting” rather than full verification.

In this paper we present two SAT-based approaches to full verification. The approaches combine BMC with interpolation or interpolation-sequence in order to compute an over-approximated set of the system's reachable states while checking that the specification is not violated. We compare the two methods both algorithmically and experimentally and conclude that they are incomparable.

Building on a previous lecture in the summer school, the introduction to interactive proof, this lecture demonstrates a specific application of interactive proof assistants: the semantics of programming languages. In particular, I show how to formalise a small imperative programming language in the theorem prover Isabelle/HOL, how to define its semantics in different variations, and how to prove properties about the language in the theorem prover.

The emphasis of the lecture is not on formalising a complex language deeply, but to teach formalisation techniques and proof strategies using simple examples. To this purpose, we cover big- and small step semantics, typing and type safety, as well as a small machine language with compiler and compiler correctness proof.

Probabilistic model checking is an automated verification method that aims to establish the correctness of probabilistic systems. Probability may arise, for example, due to failures of unreliable components, communication across lossy media, or through the use of randomisation in distributed protocols. Probabilistic model checking enables a range of exhaustive, quantitative analyses of properties such as “the probability of a message being delivered within 5ms is at least 0.89”.

In the last ten years, probabilistic model checking has been successfully applied to numerous real-world case studies, and is now a highly active field of research. This tutorial gives an introduction to probabilistic model checking, as well as presenting material on selected recent advances. The first half of the tutorial concerns two classical probabilistic models, discrete-time Markov chains and Markov decision processes, explaining the underlying theory and model checking algorithms for the temporal logic PCTL. The second half discusses two advanced topics: quantitative abstraction refinement and model checking for probabilistic timed automata. We also briefly summarise the functionality of the probabilistic model checker PRISM, the leading tool in the area.

Common program specification and verification build on concepts like method pre- and postconditions and loop invariants. These lectures notes teach those concepts in the context of the language and verifier Dafny.

This article gives an overview of software model checking, with a focus on model checkers using abstraction and refinement. It grew out of notes accompanying my lectures at the Marktoberdorf Summer School in Summer, 2011.

Contemporary satisfiability solvers are the corner-stone of many successful applications in domains such as automated verification and artificial intelligence. The impressive advances of SAT solvers, achieved by clever engineering and sophisticated algorithms, enable us to tackle Boolean Satisfiability (SAT) problem instances with millions of variables – which was previously conceived as a hopeless problem. We provide an introduction to contemporary SAT-solving algorithms, covering the fundamental techniques that made this revolution possible. Further, we present a number of extensions of the SAT problem, such as the enumeration of all satisfying assignments (ALL-SAT) and determining the maximum number of clauses that can be satisfied by an assignment (MAX-SAT). We demonstrate how SAT solvers can be leveraged to solve these problems. We conclude the chapter with an overview of applications of SAT solvers and their extensions in automated verification.

This paper introduces interactive theorem proving with the Isabelle/HOL system [3]. The following topics are covered:

• Verified functional programming: The logic HOL contains an ML-style functional programming language. It is shown how to verify functional programs in this language by induction and simplification.

• Predicate logic: Formulas of predicate logic and set theory are introduced, together with methods for proof automation.

• Inductively defined predicates.

• Structured proofs: We introduce the proof language Isar and show how to write structured proofs that are readable by both the machine and the human.

We assume basic familiarity with some functional programming language of the ML or Haskell family, in particular with recursive data types and pattern matching. No specific background in logic is necessary beyond the ability to read predicate logic formulas.

These are the notes to accompany a course at the Marktoberdorf PhD summer school in 2011. The course consists of an introduction to separation logic, with a slant towards its use in automatic program verification and analysis.

Information-flow control tracks how information propagates through the program during execution to make sure that the program handles the information securely. Secure information flow is comprised of two related aspects: information confidentiality and information integrity — intuitively pertaining to the reading and writing of the information. The prevailing basic semantic notion of secure information flow is noninterference, demanding independence of public (or, in the case of integrity, trusted) output from secret (or, in the case of integrity, untrusted) input. This document gives an account of the state-of-the-art in confidentiality and integrity policies and their enforcement with a systematic formalization of four dominant formulations of noninterference: termination-insensitive, termination-sensitive, progress-insensitive, and progress-sensitive, cast in the setting of two minimal while languages.

We present a practical algorithm for computing least solutions of systems of (fixpoint-)equations over the integers with, besides other monotone operators, addition, multiplication by positive constants, maximum, and minimum. The algorithm is based on max-strategy iteration. Its worst-case running-time (w.r.t. a uniform cost measure) is independent of the sizes of occurring numbers. We apply this algorithm to the problem of computing the abstract semantics of programs over integer intervals as well as over integer zones.