Abstracts

Galois Connections, Inc. specializes in building high assurance software for security-critical middleware and applications. For example, Galois' Trusted Services Engine (TSE) is a multi-level-secure file server with a Web front end, and illustrates our approach to software design.

The TSE enforces a strict information-flow policy between users of different security classification levels. Galois is using several technologies to ensure the TSE security requirements are met: The TSE software consists of partitioned components running on top of a MILS microkernel; most of the components are written in the functional programming language Haskell; and components that directly mediate cross-security-level communication are formally verified in Isabelle/HOL with respect to their safety and information-flow policies.

This talk will focus on our TSE formal verification efforts. I'll discuss what has worked well for us, as well as Isabelle/HOL improvements we are considering to make our job easier.

One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We present a new approach for statically analyzing data structure implementations and their use in applications. Our approach is based on specifying interfaces of data structures using abstract sets and relations. This enables our system, Jahob, to independently verify that

1. each data structure satisfies internal consistency properties and each data structure operation conforms to its interface;
2. the application uses each data structure interface correctly, and maintains the desired global consistency properties that cut across multiple data structures.

Jahob achieves this goal by combining techniques from static analysis, decision procedures, and theorem proving. To enable such a combination, Jahob uses formulas of the Isabelle interactive theorem prover as an intermediate language throughout all system components. On the one hand, this approach enables a Jahob user to prove the most difficult theorems using interactive theorem proving. This approach also gives a unifying semantic foundation of the specification constructs. On the other hand, Jahob has several validity-preserving approximations of Isabelle formulas into the languages of various automated reasoning procedures, which gives it a higher degree of automation than interactive theorem proving alone. The incorporated reasoning procedures range from decision procedures for specialized logics, such as monadic second-order logic over trees and Boolean algebra with Presburger arithmetic, to Nelson-Oppen-style decision procedures via the SMT-LIB interface, and first-order theorem provers via the TPTP interface.

In the context of the Jahob system, we are developing new algorithms for computing loop invariants, new reasoning techniques, and new approaches for extending the applicability of the existing reasoning techniques. As an example of such a novel technique, we will present Jahob's shape analysis algorithm. This algorithm infers loop invariants of heap manipulating programs by employing the reasoning procedures that Jahob provides. The computed invariants are used to communicate information between independent reasoning procedures. This architecture enabled us to combine precise reasoning about reachability in tree-like data structures with reasoning about first-order properties in general graphs and integer arithmetic properties. We have used Jahob to verify implementations of linked data structures such as (doubly-linked, sorted) lists, trees with and without parent pointers, as well as uses of data structure interfaces and relationships between multiple data structures.

We extend our previous work on a unified memory model for pointers in Isabelle/HOL. Previously, we were able to faithfully formalise the low-level, untyped view of the machine state operating systems and programming languages like C have. At the same time we provided an easy-to-use, abstract and typed view of memory where possible. We now extend this framework by another level: separation logic. This model is more than just an implementation of separation logic in a theorem prover. Its two main additional benefits are that it is a unified model that allows one to break out of abstract separation logic at any point to low-level operations and that it puts separation logic on a provably sound basis. We show the usability of our model by proving the correctness of the memory allocator in the L4 microkernel.

Interactive provers provide expressive formalism and can model complex systems. Therefore, they have been used for large scale verification and specification tasks. However, they require much effort from skilled users to prove theorems. A promising approach to improve their automation is by integrating them with automatic provers. Many problems must be solved to make this integration possible and to make it deliver good results.

In this talk, I will give an overview of the integration between the interactive prover Isabelle and several other automatic provers. I will talk about the problems solved in this project and its current status.

This talk will describe formal probabilistic models of flooding and gossiping protocols, and explores the influence of typical modeling choices and assumptions on the results of performance analysis. We use PRISM, a model checker for probabilistic systems, for the formal analysis of protocols and small network topologies, and use in addition Monte-Carlo simulation, implemented in MatLab, to establish if the results and effects found during formal analysis extend to larger networks.

Full functional verification of software is still out of reach for automatic methods and hence requires the guidance of a user. However, techniques like software model checking and abstract interpretation are often powerful enough to deal with the verification of properties like the absence of common runtime faults (like array bound violations, or Null-pointer dereferencations). In this talk we describe and discuss the integration of those tools into an Hoare-logic based interactive verification environment for imperative programs.

Similarly to the applications managed by an operating system also the operating system itself usually runs in virtual memory. Apart from pointer aliasing the verification of operating systems code has therefore to deal with a second form of aliasing: different virtual addresses might get translated to the same physical address. Consider the prototypical pointer program fragment *p = 0; *q = 1 (where p and q are integer pointers). For the proof that the value *p equals 0 after running the fragment it is not sufficient to assume p <> q. One needs the additional assumption that p and q are mapped to different (non-overlapping) regions of virtual memory.

Operating system code does usually not take advantage of aliasing effects of the address translation (although the same piece of physical memory might be available at several virtual locations). Instead it is written with the traditional assumption that each variable has a unique (virtual) address, which is used for reading and writing it. For the verification of operating system code it makes therefore sense to develop the abstraction of "plain memory" that provides precisely this traditional view.=20

The presentation focusses on the plain memory abstraction and its formalisation in PVS that has been developed in the VFiasco and in the Robin project.

Security-critical applications at the highest Evaluation Assurance Level (EAL) require formal proofs of correctness in order to achieve certification. To support secure application development at the highest EALs, we have developed techniques to largely automate the process of producing proofs of correctness of machine code. As part of the Secure, High-Assurance Development Environment (SHADE) program, we have produced an executable formal model of the Rockwell Collins AAMP7G microprocessor at the instruction set level in ACL2 in order to facilitate proofs of correctness about that processor?s machine code. The AAMP7G, currently in use in Rockwell Collins secure system products, supports strict time and space partitioning in hardware, and has received an NSA MILS certificate based in part of a formal proof of correctness of its separation kernel microcode. Proofs of correctness of AAMP7G machine code are accomplished through the use of the method of "compositional cutpoints", a technique pioneered on the SHADE program that requires neither traditional clock functions nor a Verification Condition Generator (VCG). In this paper, we will summarize the AAMP7G architecture, detail the development of the ACL2 model of the processor, describe our machine code proof framework, and finally summarize a verifying compiler framework for which this machine code proof framework is the final stage.

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 of and to eliminate bugs from such systems: software model checking and static analysis. The approaches are typically complementary. In this talk we present a framework that transforms static analysis problems into model checking problems. We investigate how highly optimised model checkers can be used in the exploration of relevant properties while at the same time avoiding scalability and abstraction issues typically associated with pure software model checking approaches. We present our prototype analysis tool, Goanna, for checking C/C++ programs and demonstrate its applicability to the sources codes of OpenSSL and the GNU coreutils.

Microkernels are very interesting for the construction of reliable operating systems. The kernel only provides very basic abstractions and is therefore relatively small. On top of it, critical system parts like memory management or drivers can be constructed with good isolation and written and tested independently from each other. However, in order to reach a high level of certification for such a system the properties of isolation have to be formally verified.

In a joint project Clearsy, ENST, CEA and STMicroelectronics have been working on methods to formally verify security properties of a system based on the L4 microkernel. The starting point of this research was the development of a formal model of the L4 API in the B language. This proved promising but showed two major shortcomings which we are currently addressing.

First, the L4 kernel itself is not sufficient to prove any of the initially mentioned security properties of isolation because it only provides mechanisms while the security properties require a properly implemented policy in the system on top. Therefore, the current research concentrates on the development of a model that includes not only L4 but also a set of policy applications on top using the refinement possibilities of the B language.

Second, the model of the L4 API cannot prove the correctness of an actual implementation of L4. To solve this problem we are pursuing two different approaches: Clearsy has developed an animator for B models that allows to compare test results produced by the formal model and those of the test suite for L4. With ENST and CEA we are working on automated code checking based on property back-propagation in the implementation code and weakest precondition computation.

This talk will shortly introduce the B model of the L4 API and then focus on the formal model of the system and the B-aided testing of the L4 implementation.

The talk focuses on the VAMOS Microkernel as part of the Academic System of the Verisoft Project. The microkernel layer is divided into two sublayers which are described by formal models. CVM* is our first model on top of the processor layer. It simulates the execution of different DLX Assembler programs as if they were executed on separate machines with own memory and registers. By this, the notion of separate processes is introduced. The CVM* model relies on one distinguished process, the kernel, that performs certain special tasks like process and memory management, device and inter-process communication, rights management as well as scheduling and interrupt delivery. In CVM*, the kernel code itself is a model parameter. The instantiation of CVM* with the concrete kernel VAMOS is denoted by CVM* + VAMOS. Obviously, for higher layers, the actual code of the kernel is no more of any interest. Instead, only its semantic effects should be modeled. This becomes feasible in the abstract model VAMOS*. It models the interaction of separate DLX Assembler processes with the kernel and, thus, gives the specification of the microkernel layer.

The talk presents the different models and their opposite connections. We describe our argumentation on different abstraction layers, to show the functional correctness of the VAMOS implementation. Based on the functional correctness, we proceed by showing properties of the specification.

High performance and high assurance are conflicting goals of microkernel development, especially for embedded systems. We propose to resolve this conflict by a development model of rapid prototyping and iterative refinement of the kernel in a functional programming language, followed by the extraction of a machine-checkable formal specification in higher-order logic and the derivation of a formally verified high-performance implementation in C. To avoid emergent misbehaviour of the kernel API once in real use, we combine the functional kernel prototype with a machine simulator to execute real user-level software, thus providing a platform capable of exposing use issues. We will describe our experience in applying this development methodology to the seL4 high-assurance microkernel.