Polyvios Pratikakis, Post-doctoral Researcher, Verimag
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.
Time and place:
2:00pm Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Pedro R. D'Argenio, Lecturer, Universidad Nacional de Cordoba (UNC), Argentina
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.
Time and place:
3:00pm Sala de Grados
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Francesco Zappa Nardelli, Researcher, INRIA Paris-Rocquencourt
Time and place:
11:00am Amphitheatre H-1005
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Gogul Balakrishnan, Researcher, NCE Labs, Princeton, NJ
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.).
Time and place:
11:00am Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Chris Gill, Associate Professor, Washington University in St. Louis
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.
Time and place:
4:15pm Amphitheatre H-1005
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Gerardo Schneider, Researcher, University of Oslo
Time and place:
11:00am Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Xavier Leroy, Senior Computer Scientist, INRIA, Paris-Rocquencourt
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.
Time and place:
2:00pm Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Jose Meseguer, Professor, University of Illinois at Urbana-Champaign
Time and place:
11:00am Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain
Anindya Banerjee, Professor, Kansas State University
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.
Time and place:
11:00am Amphitheatre H-1002
Facultad de Informática
Universidad Politécnica de Madrid
28660-Boadilla del Monte, Madrid, Spain