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