While most branches of engineering consist of methodologies for building complex systems from simple components, formulating incremental and compositional methods for security engineering has been a daunting task: in general, security properties are not preserved under refinement or composition. The reason is that nondestructive composition operations require guarantees that components' static assumptions about the environment are maintained; whereas security engineering is concerned with dynamic, adversarial environments, and what happens when the assumptions fail.

The goal of our long-term effort towards Protocol Derivation System has been to capture the sound rules and methods for incremental protocol development, that have evolved in practice, to study their semantic foundations, and to provide tool support. In this talk, I shall summarize results of this effort so far, and present a case study of GDOI, the standard protocol for group communication and multicast over IPSec. Although carefully designed and thoroughly analyzed prior to standardization, this protocol turned out to have vulnerabilities invalidating the basic stated requirements: an attempt to derive it incrementally, together with the desired security properties, led to a derivation of an attack, which in turn allowed evaluation of the repair options. The derivations were built using the Protocol Derivation Assistant, a development environment that will be demonstrated during the talk.

GDOI was analyzed in joint work with Catherine Meadows.

We give an informal introduction to the picalculus, showing that it can be viewed as an expressive language for expressing the behaviour of mobile agents. By means of examples we will demonstrate the usefulness of so-called behavioural equivalences for expressng the correctness of agents, and will briefly touch on proof methodologies for actually demonstrating their correctness.

If time permits we will also discuss

• extensions of the picalculus which take into account the distributed world inhabited by these mobile agents,
• the use of static type systems to constrain the permitted behaviour of these agents

In the past decades a large portion of formal language theory has been generalized from strings to more complex structures like trees and graphs. I want to show how some of the obtained results can be used to specify and efficienty verify graph properties for certain classes of graphs. In particular, sentences in Monadic Second-Order logic (MSO) interpreted in finite graph models naturally capture the notion of "finite-state graph languages", and MSO transductions naturally capture the notion of "finite-state graph transductions". On graphs of bounded tree-width (which can be generated by context-free graph grammars) such MSO sentences and transductions can efficiently be evaluated, using tree automata and tree transducers, respectively.

Electronic communications devices safeguard classified information in government and military computer networks. Before they can be deployed, however, such devices must be carefully evaluated to ensure that they preserve data confidentiality. Our research is devising ways of making information security evaluations more rigorous and efficient. We have shown how graph theory can be applied to logical circuit diagrams and processor board designs to evaluate the flow of classified information through a device in different operating modes. We have also adapted risk analysis concepts to assess the effects of component failures within the device on information security. These techniques have been incorporated into a prototype security evaluation tool capable of analysing circuit diagrams produced by the popular design tool Protel.

Highly secure computing platforms generally require formal proofs of correctness as part of their evaluation (e.g., Common Criteria EAL7). We have developed practical techniques for creating executable formal models of computing platforms that can both be proved correct, as well as function as high-speed simulators, thus achieving both verification (we built the thing right) and validation (we built the right thing). In this talk, we will review these theorem-prover-based technologies, discuss their application to both hardware and software, and summarize their use as evidence in an actual EAL7 evaluation. The talk will emphasize the importance of expressing the right high-level theorem; crafting a low-level model that can be shown to correspond to the actual design; using levels of abstraction to connect the low-level model to the high-level theorem; as well as the theorem proving tools and techniques that make this work truly practical in an industrial setting.

One of the challenges in verifying systems level code is the low-level, untyped view of the machine state that operating systems have. We describe a way to faithfully formalise this view while at the same time providing an easy-to-use, abstract and typed view of memory where possible. We have used this formal memory model to verify parts of the virtual memory subsystem of the L4 high-performance microkernel. All formalisations and proofs have been carried out in the theorem prover Isabelle and the verified code has been integrated into the current implementation of L4.

We consider the algorithmic analysis of information flow in multi-agent systems from the perspective of the logic of knowledge, showing that certain questions about the existence of covert channels can be viewed as special cases of model checking and synthesis problems for the logic of knowledge. We describe some recent results concerning the decidability of these general problems and discuss algorithms for some special cases.

Orion is a static analyzer aimed at detecting programming errors in C, C++, and Java code. It differs from tools like lint and its successors in that it puts more effort in suppressing spurious error reports. The large number of such false alarms that is typical for similar tools prevents a more widespread use among developers. Orion uses techniques from model checking and theorem proving to improve this signal-to-noise ratio. The current prototype shows a significant improvement over lint-like tools on several test cases, with acceptable running times. This talk will cover the underlying algorithms and their relation to model checking, the design decisions and tool architecture behind Orion, and some recent developments

Dennis Dams is member of the Bell Labs Computing Sciences Center. His background is in formal verification, in particular model checking and abstract interpretation. One of his main current interests is to harness the power of these techniques into easy-to-use tools for the software developer. Previously, Dennis has worked as an assistant professor at the Electrical Engineering department of Eindhoven University of Technology in The Netherlands. He holds a PhD in Computer Science from Eindhoven University.

We extend assertion-based sequential-program logic by separating the state into visible and hidden parts, allowing a specialisation of knowledge-based reasoning about the (hidden) values that cannot be observed directly. It is done by adding an extra shadow state-component to represent the values the hidden variables might have acquired as a result of nondeterminism in the program.

Our intended application is a simple form of security where we provably limit the conclusions an observer can draw, from the visible part, about the hidden part of the state; we allow increase of ignorance as a form of program refinement; and we avoid the refinement paradox where apparently secure programs are refinable into insecure ones.

Program-algebraic refinement laws are illustrated and justified; they can be used to derive ignorance-preserving implementations from suitable specifications. As a case study we treat the Dining Cryptographers protocol.

This talk reviews syntactic criteria on transition system specifications that ensure compositionality of semantic equivalences and implementation relations: if a transition system is obtained as a composition of other transition systems, and one of these components is replaced by a transition system that constitutes a correct implementation according to some semantic equivalence or preorder, then the resulting composition is a correct implementation of the original one. Such compositionality results are derived from the syntactic shape of the operational rules specifying the composition operator in question. Typically the proofs involve a decomposition of the formulas in the modal logic that characterises the implementation relation under investigation.

Abstract: This talk is an introduction to the area of control of real- time systems, which are specified by Timed Game Automata. This model is a (minor) variant of Timed Automata which are Finite Automata equipped with clocks, taking their value in a dense time domain. We first present the model of Timed Game Automata and the basic results established in the last decade for the control problems on this model. We also review some of the issues raised by the use of dense time to model real-time systems.

System software has been under scrutiny by the software verification community from various angles in the recent past. There are two major algorithmic approaches to ensure the correctness and/or the elimination of bugs of such systems: Software model checking and static analysis. Both approaches are typically complementary. In this talk we present a framework that transforms static analysis problems into model checking problems. The advantage being that highly optimized model checkers can be used in the exploration of relevant properties while at the same time avoiding the scalability and abstraction issues typically existing with pure model checking approaches.

Presented by Simon Winwood.

A standard method for securing untrusted code is code rewriting, whereby operations that might compromise a safety policy are secured by run-time program monitors. In this talk, I describe a novel approach to sandboxing that is based on a combination of code rewriting and hardware-based memory protection. In contrast to previous work, this rewriting is on raw binary code. I also describe a machine-checkable proof of safety that includes the interaction of the untrusted binary with the operating system. This proof constitutes a crucial step towards the use of rewritten binaries with proof-carrying code.

I will also talk about on-going work into the synthesis of suitable proof-carrying code monitors.

The mechanisation of proofs for probabilistic systems is particularly challenging due to the verification of real-valued properties that probability entails: experience indicates that there are many difficulties in automating real-number arithmetic in the context of other program features.

In this paper we propose a framework for verification of probabilistic distributed systems based on the generalisation of Kleene algebra with tests that has been used as a basis for development of concurrency control in standard programming. We show that verification of real-valued properties in these systems can be considerably simplified, and moreover that there is an interpretation which is susceptible to counterexample search via state exploration, despite the underlying real-number domain.

Classic texts on Artificial Intelligence recommend various strategies for combinatorial search, without really explaining where they come from, and without showing how programs that make combinatorial choices can be composed. I will show how the well-known "lists of successes" approach in functional programming (which implements depth-first search) can be extended to implement breadth-first search and depth-bounded search also, and how all three search methods can be viewed as implementations of a single algebraic specification.