Program
New: Program schedule
Software Architecture for Dependable Systems
Abstract: One of the most important engineering tools for achieving dependability is the use of high-level models for reasoning about the structure and behavior of a system. In this lecture I show how formal software architectural models can be used to improve dependability, including analysis of critical quality attributes (e.g., performance, security, etc.) and soundness (e.g., absence of deadlock, and component compatibility). I also provide an overview of techniques for ensuring that an implementation conforms to its architecture, and ways to use architectures at run-time to provide self-healing capabilities.
The Evolution of Software Composition Mechanisms
Abstract: Software has been evolving from pre-defined, monolithic architectures to increasingly decentralized, distributed, dynamically composed federations of components. Binding mechanisms have been evolving from static to highly dynamic schemes based on discovery, negotiation, and optimization. The talk surveys the evolution of software composition mechanisms, from in-the-small embedded environments to in-the-large environments, like web services.
Certified Code
Abstract: Proof-carrying code, more simply referred to as PCC, was developed in 1996 and relatively quickly a substantial amount of work by several researchers led to nearly practical demonstrations and some interesting variants such as typed assembly language (TAL), foundational FPCC, and temporal-logic PCC. Collectively, PCC and its variants can be referred to as "certified code" schemes, as they all seek to provide what amount to digital certificates that permit automatic verification of important properties of software. Because the certificates allow independent parties to do the verification, many have seen certified code as one of the key technologies for future mobile code systems, particularly for applications where security and fast performance are critical. In this session, we will begin with a basic introduction to some of the basic technical concepts underlying PCC and explore some of the reasons for the development of its variants. Many of these reasons can be traced to basic engineering concerns, such as the soundness of the system, size of the certificates, or the time required to verify them. Indeed, in a sense the entire development of certified code can be viewed as the emergence of a discipline of "proof engineering". We will then explore the current and future limitations of certified code, with an eye towards understanding the practical impact on computing systems.
Abstractions for Building Reliable Distributed Systems
Abstract: Reliable distributed systems composed of many interacting parts are notoriously difficult to design and reason about. In order to cope with this complexity and reduce design and implementation errors, practitioners and theoreticians have often employed modular approaches. The idea is to decompose the system into smaller parts also known as abstractions or building blocks. The first part of this seminar will introduce group communication abstractions that can be used to build reliable distributed systems. The second part of the seminar will discuss how these abstractions can be efficiently implemented, while still tolerating component failures.
Software Security and Verification
Abstract: Security of computer systems has multiple aspects ranging from cryptography to securing low level implementations. Most practical exploits are based on implementation flaws rather than on flaws of the cryptographic principles or protocols. This session will present an approach that encompasses information security, integrity, and availability problems in software by assuring security of the actual implementation given in a language such as ANSI-C. The existing techniques for ensuring security properties are mostly ad hoc and informal. In contrast, this session will present an approach based on model checking techniques that are exhaustive and formally guarantee the correctness of security properties.
This session will start from introducing basic concepts of model checking and then show how advanced techniques of automated abstraction and satisfiability testing (SAT solving) can be used for practical verification of ANSI-C programs. We will also present a solution to a problem of secure substitutability in the context of evolving systems. The substitutability problem is solved as verification of the following two criteria: (i) any updated portion of a software system must continue to provide all services offered by its earlier counterpart, and (ii) previously established system correctness properties must remain valid for the new version of the software system.
The Value Proposition for Everyday Dependability
Evaluating the dependability of a system for a specific application entails not only determining technical characteristics of the system such as reliability, soundness, performance, security, and usability. It also entails understanding the level of dependability required for that specific application and acceptable costs of achieving that dependability - so the evaluation must reflect clients' expectations as well as the specifications of the system and its components. Further, decisions that may substantially affect dependability must often be made early in design, long before code can actually be evaluated.
I will discuss the setting of everyday dependability, in which cost-effectiveness is the dominant criterion for evaluation. Based on this I will discuss the value proposition for dependability, which reflects a given client's needs and the tradeoffs between cost and dependability. Finally I will discuss an approach to predicting the value of a system early in design, when critical commitments must be made.