Nowadays, software-intensive systems can be found in a large number of human-made products. On the one hand, this increases comfort and allows for a huge number of new applications. On the other hand, it imposes a responsibility to ensure that the applications work as intended and the used data is secure. This responsibility must be taken very seriously. Especially for mission- or safety-critical applications. Increasing the reliability of those applications represents an essential and challenging research topic, particularly in computer science.

Scientific foundations provide models that allow for the capture of application domains and their requirements, but also for understanding the structure and behaviour of programs. These foundations cover a broad spectrum of issues and work with formal models and description techniques, their semantics, and methods in order to support a deep and precise understanding of system properties and interplay. Only on the basis of such formal fundamentals, it is possible to prove and ensure the correctness of both software and hardware. Tools and methods to support or automate proofs have been developed in the last few decades and remarkable advances have been achieved for the complexity of systems that can be proved as correct, either mechanically or by human agents, assisted by means of mathematically rigorous proofs. Formal methods to support such reasoning mainly follow two different approaches: the so called language-based and the logic-based approaches. The objective of the 2009 Summer School on Formal Logical Methods for System Security and Correctness was to present the state-of-the-art of both approaches to an audience which consisted of students from all over the world.

PATRICK COUSOT lectured on Program Analysis and Verification by Abstract Interpretation. He introduced the basic concepts in abstract interpretation of exact and approximate abstraction. He applied them to design of program semantics and proof methods by exact abstractions, and to automatic and sound static analyzers and verifiers by approximate abstractions to cope with undecidability.

Static program analysis is the process of obtaining information about the behavior of a program without actually executing its code. From a mathematical point of view, static program analysis reduces to solving equations. In his course on Newtonian Program Analysis JAVIER ESPARZA presented generic methods for solving such equations, i.e., methods that are well defined for any interpretation. After reviewing the classical worklist algorithm derived from the Knaster-Tarski and Kleene theorems, he showed that Newton's method - a well-known technique for numerically solving equations with the real numbers as domain - can be extended to arbitrary interpretations. He taught consequences and applications for other domains like languages or semilinear sets.

A refinement type is a type qualified by a logical constraint; an example is the type of even numbers, that is, the type of integers qualified by the is-an-even-number constraint. Although this idea has been known in the research community for some time, it has been assumed impractical because of the difficulties of constraint solving. But recent advances in automated reasoning have overturned this conventional wisdom, and transformed the idea into a practical design principle. In his lectures on Principles and Applications of Refinement Types ANDREW GORDON presented a primer on the design, implementation, and application of refinement types. These implementation techniques include the use of external SML solvers in conjunction with conventional typing algorithms, and the applications include avoiding security errors in enterprise datacenters and proving security properties of cryptographic protocol implementations.

ORNA GRUMBERG lectured on 3-Valued Abstraction and its Applications in Model Checking. She expounded two frameworks of abstraction-refinement: one for the 2-valued semantics and another for the 3-valued semantics. She showed two applications for the 3-valued framework: a compositional model checking and a high-capacity (Un)Bounded 3-valued model checking for hardware.

The lectures of GERHARD JÄGER on Modal Fixed Point Logics concentrated on multi-modal logics extended by the possibility to introduce least and greatest fixed points. After discussing a range of traditional results the course turned to more recent approaches dealing with finite and infinite derivations and explicit representations of proofs. The focus has been on foundational questions and a proof-theoretic perspective rather than practical applications.

In his lectures on Effective Analysis of Infinite-state Stochastic Processes and Games ANTONÍN KU ČERA considered the classes of Markov chains, Markov decision processes, and stochastic games definable by pushdown automata with probabilistic and non-deterministic choice. He gave an overview of the existing results and presented selected concepts and techniques that have been used to establish these results.

ORNA KUPFERMAN lectured on Multi-valued Automata and their Applications. Standard automata accept or reject input words. Accordingly, an automation induces a mapping from Σ* to the binary set {true, false}. The course introduced “multi-valued automata”, which induce mappings from Σ* to richer sets of values. She focused on lattice automata, which map input words to values from a lattice, and “weighted automata”, which map input words to R (the set of real numbers). She described applications of lattice automata in abstraction and model checking of multi-valued logics, and described applications of weighted automata in the competitive analysis of online algorithms.

The goal of XAVIER LEROY's lecture on Mechanized Semantics with Applications to Program Proof and Compiler Verification was to show how modern theorem provers - he used the Coq proof assistant - can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs as well as over generic program transformations as typically found in compilers.

With his lectures on Using Security Policies to Write Secure Software ANDREW MYERS explored the idea of integrating security policies into the programming environment and the run-time system. A programming language that incorporates security policies can help programmers reason about the security of the software they are building, and to show that it does not violate information security policies. He examined how this approach works in the context of the security-typed programming language Jif. Once security policies are exposed to the compiler and run-time system, these layers can automatically synthesize security enforcement mechanisms. We saw an instance of this idea in the Swift web application framework, in which information security policies automatically drive the secure partitioning of web applications between the browser and the server. His lecture was based on A. Sabelfeld's lecture series.

LUKE ONG lectured on A Type System Equivalent to the Modal μ-Calculus Model Checking of Higher-Order Recursion Schemes. In his course he gave a survey about the algorithmic model theory of recursion schemes, and explained the novel application to the model checking of functional programs. Infinite structures are robust and have strong algorithmic properties, which are directly relevant to the verification of higher-order computation. Kobayashi shows that verification problems of higher-order functional programs can easily be reduced to model checking problems of recursion schemes. He used a kind of refined intersection types to construct type-theoretic characterisations of highly complex theories, so that the model checking problem of recursion schemes against the modal μ-calculus (and hence all standard temporal logics) is reducible to a problem of typability of recursion schemes, showed as decidable.

Language-based Control for Information Flow and Release was the lecture of ANDREI SABELFELD. Current standard security practices do not provide substantial assurance that the end-to-end behaviour of a computing system satisfies important security policies such as confidentiality. An end-to-end confidentiality policy might assert that secret input data cannot be inferred by an attacker through the attacker's observations of system output; this policy regulates information flow. Conventional security mechanisms such as access control and encryption do not directly address the enforcement of information-flow policies. Recently, a promising new approach has been developed: the use of programming-language techniques for specifying and enforcing information-flow policies. These lectures gave an overview about the state-of-the-art in language-based information-flow security, particularly focusing on information release, or declassification, policies and on trade-offs between static and dynamic techniques to enforce information-flow policies.

The contributions in this volume have evolved from the lectures of the 30th International Summer School at Marktoberdorf, held from August 4th to August 16th, 2009. About 110 participants from 30 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 go to Dr. Katharina Spies, Silke Müller, and Katjana Stark for their great 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), Microsoft Research and the town and county of Marktoberdorf. We thank all authorities involved.

THE EDITORS