Ebook: Logics and Languages for Reliability and Security

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

We introduce and illustrate basic notions of abstract interpretation theory and its applications by relying on the readers general scientific culture and basic knowledge of computer programming.

We present a novel generic technique for solving dataflow equations in interprocedural dataflow analysis. The technique is obtained by generalizing Newton's method for computing a zero of a differentiable function to ω-continuous semirings. Complete semilattices, the common program analysis framework, are a special class of ω-continuous semirings. We show that our generalized method always converges to the solution, and requires at most as many iterations as current methods based on Kleene's fixed-point theorem. We also show that, contrary to Kleene's method, Newton's method always terminates for arbitrary idempotent and commutative semirings. Furthermore, the number of iterations required to solve a system of n equations is at most n.

A refinement type {x : T | C} is the subset of the type T consisting of the values x to satisfy the formula C. In this tutorial article we explain the principles of refinement types by developing from first principles a concurrent λ-calculus whose type system supports refinement types. Moreover, we describe a series of applications of our refined type theory and of related systems.

This paper presents two frameworks for abstraction-refinement in model checking. The first is the CounterExample-Guided Abstraction-Refinement (CEGAR) which can verify universal fragments of temporal logics and is based on a 2-valued semantics of temporal logics. The other is the Three-valued Abstraction-Refinement (TVAR) and is based on a 3-valued semantics of these logics.

We also present an application of the 3-valued framework for fully automatic compositional model checking. Based on this and other successful applications of the 3-valued framework we conclude that the additional power it provides is worth the extra efforts of having non-standard definitions and algorithms.

The following notes are centered around multi-modal logics extended by the possibility to introduce least and greatest fixed points. We begin with discussing a range of traditional results and turn to more recent approaches dealing with finite and infinite derivations and explicit representations of proofs afterwards. Our focus is on foundational questions and a proof-theoretic perspective rather than practical applications.

We consider the classes of Markov chains, Markov decision processes, and stochastic games definable by pushdown automata with probabilistic and non-deterministic choice. We give an overview of the existing results and present selected concepts and techniques that have been used to establish these results.

Standard automata accept or reject input words. Accordingly, an automaton induces a mapping from Σ* to the binary set {true,false}. The course will introduce multi-valued automata, which induce mappings from Σ* to richer sets of values. We will focus on lattice automata, which map input words to values from a lattice, and weighted automata, which map input words to (the set of real numbers). We describe applications of lattice automata in abstraction and model checking of multi-valued logics, and describe applications of weighted automata in the competitive analysis of online algorithms.

The goal of this lecture is to show how modern theorem provers—in this case, the Coq proof assistant—can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and over generic program transformations, as typically found in compilers. The topics covered include: operational semantics (small-step, big-step, definitional interpreters); a simple form of denotational semantics; axiomatic semantics and Hoare logic; generation of verification conditions, with application to program proof; compilation to virtual machine code and its proof of correctness; an example of an optimizing program transformation (dead code elimination) and its proof of correctness.

We explore 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. We examine how this approach works in the context of the security- typed programming language Jif, which allows programmers to express both information flow policies for confidentiality and integrity, and access control policies. The compiler and run-time system use this added information to enforce strong security properties such as noninterference and robustness.

A variety of language mechanisms make this approach expressive enough to build real software: support for rich language features such as objects and exceptions, automatic inference of security policies, constrained parameterization over security policies, and dependent types that capture security policies determined at run time.

Mechanisms are needed for relaxing confidentiality and integrity policies, but noninterference no longer holds once these mechanisms are used. What can we say about security? We show that a robustness property captures the idea that the adversary cannot cause information to become visible to itself.

Integrating security policies into the program yields an opportunity to raise the level of abstraction at which we build software. Modern applications are difficult to build securely. They are distributed applications, so applications need to be secure even when the adversary partially controls the network and perhaps also some of the host machines running the application. Yet programming these applications also requires attention to a host of low-level details that obscure program logic.

By exposing security policies to the compiler and run-time system, it becomes possible for these layers to automatically synthesize security enforcement mechanisms such as partitioning and replication of code and data, digital signatures and encryption, and network protocols. The result is not only a higher level of abstraction for building secure software, but also stronger assurance that the security mechanisms being used do enforce the security requirements of the application.

We look at how different kinds of policies—for confidentiality and integrity—can be used automatically to drive the compilation of high-level annotated code into target code that employs a variety of security mechanisms. This approach can be used to make web applications easier to build securely and efficiently.

We survey recent developments in a systematic approach to the verification of higher-order computation based on two models: (the respective higher-order hierarchies of) recursion schemes and pushdown automata. Higher-order recursion schemes are in essence the simply-typed lambda calculus with recursion, generated from uninterpreted first-order symbols. Higher-order pushdown automata are a generalisation of pushdown automata to higher-order stacks, which are iterations of stack of stacks. They are highly expressive definitional devices for word languages and such infinite structures as trees and graphs. We study the expressive power of the two models and the algorithmic properties of the infinite structures generated by them. As an algorithmic application of game semantics, we present recent results in the model checking of infinite trees generated by recursion schemes, and a machine characterisation of recursion schemes by a new variant of higher-order pushdown automata called collapsible pushdown automata. We survey recent advances in the solution of parity games over the configuration graphs of collapsible pushdown automata. We conclude with some remarks on an application to the verification of higher-order functional programs. A theme of the work is the fruitful interplay of ideas between the neighbouring fields of semantics and verification.

Information-flow technology is a promising approach for ensuring security by design and construction. When tracking information flow, of particular concern are implicit flows, i.e., flows through control flow when computation branches on secret data and performs publicly observed side effects depending on which branch is taken.

The large body of literature exercises two extreme views on implicit flows: either track them (striving to show that there are no leaks, and often running into the problem of complex enforcement mechanisms and false alarms), or not track them (which reduces false alarms, but provides weak or no security guarantees).

This paper distinguishes between malicious and nonmalicious code. The attacker may exploit implicit flows with malicious code, and so they should be tracked. We show how this can be done by a security type system and by a monitor. For nonmalicious code, we explore a middle ground between the two extremes. We observe that implicit flows are often harmless in nonmalicious code: they cannot be exploited to efficiently leak secrets. To this end, we are able to guarantee strong information-flow properties with a combination of an explicit-flow and a graph-pattern analyses. Initial studies of industrial code (secure logging and data sanitization) suggest that our approach has potential of offering a desired combination of a lightweight analysis, strong security guarantees, and no excessive false alarms.