Multi-threaded programming is increasingly relevant due to the growing prevalence of multi-core processors. Unfortunately, the non-determinism in parallel processing makes it easy to make mistakes but difficult to detect them, so that writing concurrent programs is considered very difficult. A data race, which happens when two threads access the same memory location without synchronization is a common concurrency error, with potentially disastrous consequences.

We present Locksmith, a tool for automatically finding data races in multi-threaded C programs by analyzing their source code. Locksmith uses a collection of static analysis techniques to reason about program properties, including a novel effect system to compute memory locations that are shared between threads, a system for inferring "guarded-by" correlations between locks and memory locations, and a novel analysis of data structures using existential types. We present the main analyses in detail and give formal proofs to support their soundness. We discuss the implementation of each analysis in Locksmith, present the problems that arose when extending it to the full C programming language, and discuss some alternative solutions. We provide extensive measurements for the precision and performance of each analysis and compare alternative techniques to find the best combination.

Quantitative model checking computes the probability values of a given property quantifying over all possible schedulers. It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other (and hence arbitrary schedulers may result too powerful). Therefore, we focus on the quantitative model checking problem restricted to distributed schedulers that are obtained only as a combination of local schedulers (i.e. the schedulers of each component) and show that this problem is undecidable. In fact, we show that there is no algorithm that can compute an approximation to the maximum probability of reaching a state within a given bound when restricted to distributed schedulers.

We will also discuss the impact of such result on the analysis of security protocols and ideas to get better overestimatios than those obtained by standard probabilistic model checking.

For performance reasons, multiprocessors may reorder memory accesses in various subtle ways: your shared-memory concurrent program might exhibit behaviours that cannot be obtained as interleaving of its memory accesses. In these lectures I will introduce relaxed memory models for multiprocessors; describe, both informally and formally, a model for Intel 64/IA-32 processors; and compare this with models for other architectures.

What You See Is Not What You eXecute: computers do not execute source-code programs; they execute machine-code programs that are generated from source code. Not only can the WYSINWYX phenomenon create a mismatch between what a programmer intends and what is actually executed by the processor, it can cause analyses that are performed on source code -- which is the approach followed by most security-analysis tools -- to fail to detect bugs and security vulnerabilities. Moreover, source code is not available for a lot of programs such as viruses, worms, Commercial Off the Shelf (COTS) components, etc.

In this talk, I will highlight some of the advantages of analyzing executables directly, and discuss the algorithms we have developed to recover information from stripped executables about the memory-access operations that the program performs. These algorithms are used in the CodeSurfer/x86 tool to construct intermediate representations that are used for browsing, inspecting, and analyzing stripped x86 executables.

Finally, I will talk about our experience with using CodeSurfer/x86 to find problems in Windows device drivers.

Joint work with T. Reps (UW), J. Lim (UW), and T. Teitelbaum (Cornell and GrammaTech, Inc.).

Distributed real-time system software consists of layered stacks of mechanisms, including: operating system level threads, ports, sockets, and timers; low-level middleware abstractions such as reactors and monitor objects; and high-level middleware services such as gateways and request brokers. In these systems, task chains span multiple hosts and may be initiated asynchronously. Furthermore, limited host resources must be shared among competing task chains according to policies that can ensure safety, liveness, and timing properties end-to-end. Our research, which has been supported in part by NSF awards CCF-0448562 (CAREER) and CNS-0716764 (Cybertrust), focuses on system software design, modeling, verification and property enforcement in distributed real-time systems.

This talk summarizes the evolution of our research over the past two years, from a focus on middleware modeling and property enforcement, towards higher level work on real-time component models and verification tool chains, and towards lower level work on scheduling policy design and verification in diverse operating environments. A brief survey of results from our prior research collaborations, on timed automata models for middleware verification and protocols and mechanisms for property enforcement, is given first as background for our current work. The second part of the talk presents our work on a new real-time component model designed specifically for distributed real-time component middleware with different concurrency configurations. The third part of the talk describes our work on scheduling policy design and verification for open soft real-time systems, including methods for designing and verifying scheduling policies under realistic degrees of variability in system timing behavior.

In this talk I will describe CL, a formal language for writing (electronic) contracts, in the context of Service-Oriented Architectures (SOA). The language allows to write (conditional) obligations, permissions and prohibitions, and to represent the so-called contrary-to-duties (CTDs) and contrary-to-prohibitions (CTPs). CTDs and CTPs are useful to establish what happen in case obligations, respectively prohibitions, are not respected. The approach is action-based, meaning that the above normative notions are defined on actions and not on state-of-affairs. I will then sketch some initial ideas on model checking contracts as well as recent work on automatic extraction of contract monitors. Finally, I will present some open problems, and other application domains of CL, besides SOA.

Can you trust your compiler? Can we make sure that the generated machine code behaves as prescribed by the semantics of the source program? This question is particularly acute for critical software that has been certified by applying formal methods to its source code: any bug in the compiler can invalidate the guarantees obtained by formal verification of the source.

Several approaches to this problem have been proposed: proof-carrying code, translation validation, and compiler verification. In the latter approach, mechanized program proof is applied to the compiler itself to prove a semantic preservation result between the source and generated codes.

In the context of the CompCert project (http://compcert.inria.fr/), I am working on such a semantic preservation proof, mechanized using the Coq proof assistant, for a realistic, moderately-optimizing compiler translating a subset of the C language down to PowerPC assembly code. An originality of this work is that most of the compiler is programmed directly in the specification language of Coq (a small pure functional language), then automatically extracted to executable Caml code.

The seminar will give a general overview of the CompCert compiler and its (rather large) proof of correctness, and outline some directions for future work on verification of other tools that participate in the development and verification of critical software.

This talk presents the temporal logic of rewriting TLR*. Syntactically, TLR* is a very simple extension of CTL* which just adds action atoms, in the form of spatial action patterns, to CTL*. Semantically and pragmatically, however, when used together with rewriting logic as a "tandem" of system specification and property specification logics, it has substantially more expressive power than purely state-based logics like CTL*, or purely action-based logics like A-CTL*.Furthermore, it avoids the system/property mismatch problem experienced in state-based or action-based logics, which makes many useful properties inexpressible in those frameworks without unnatural changes to a system's specification.The advantages in expresiveness of TLR* are gained without losing the ability to use existing tools and algorithms to model check its properties: a faithful translation of models and formulas is given that allows verifying TLR* properties with CTL* model checkers.

Information flow policies like confidentiality and integrity are essential to the security of many software systems such as medical information systems, collaborative planning systems and voting systems. Confidentiality policies must ensure that unauthorised clients (attackers) cannot acquire sensitive information. Integrity policies must ensure that untrustworthy data does not flow into trusted sites.

Formal techniques such as program logics, type theory and abstract interpretation facilitate reasoning about information flow policies for application-level software. These techniques help capture policy semantics and permit specification of enforcement mechanisms for verifying complex application software, thus providing end-to-end security guarantees. A key challenge is to provide semantics to declassification policies which involve the deliberate, partial release of confidential information during system execution.