RV 2010

Invited Speakers

Mike Barnett Principal RSDE, Microsoft Research, Redmond, WA, USA Code Contracts for .NET: Runtime Verification and So Much More Abstract: The Code Contracts project provides a single framework for specifying programs written in any of the .NET languages. On top of the framework, we have built a comprehensive set of tools that offer runtime verification, static checking, documentation generation, and editor extensions, all of which are integrated into Visual Studio. A fundamental design goal has been to fit in with existing development tools, practices, and processes. This talk will describe the history of the project, the design decisions behind it, and its adoption (or lack thereof) in the product groups within Microsoft. And of course we will show off some really cool examples of the tools we have built so far!
Rance Cleaveland Professor, Department of Computer Science, University of Maryland, MD, USA Co-founder of Reactive Systems, Inc.http://www.reactive-systems.com Automatic Requirements Extraction from Test Cases Abstract: This talk describes a method for extracting functional requirements from tests that take the form of vectors of inputs (supplied to the system) and outputs (produced by the system in response to inputs). The approach uses machine-learning/data-mining techniques to infer invariants from the test data, and an automated-verification technology to determine which of these proposed invariants are indeed invariant and may thus be seen as requirements. Experimental results from a pilot study involving an automotive-electronics application show that the method can infer requirements that are missing from existing documentation, and using tests that fully cover the structure of the software yield more complete invariants than structurally-agnostic black box tests.
Matthew Dwyer Professor, Department of Computer Science, University of Nebraska, NE, USA Optimizing Runtime Monitors : Combining Static and Dynamic Techniques Abstract: An optimizing compiler may transform a program, P, by re-ordering, eliminating, or replacing statements as long as the resulting program, P&prime, has equivalent semantics. Runtime monitoring of a property, &phi, generally involves instrumenting the program with additional statements resulting in a new program, P_i, whose execution detects states of P that are relevant to &phi and triggers appropriate monitor processing. While P_i is amenable to optimization by a traditional compiler the degree of performance improvement that can be achieved is limited, since the compiler treats instrumentation like any other statement and preserves it semantics. By analyzing the relationship between the program and property one can transform the monitoring problem to consider a variant of the property, &phi&prime, and program instrumentation, P&prime_i. Such transformations can guarantee lossless monitoring relative to the original property, P_i \|= &phi &hArr P&prime_i \|= &phi&prime, while enabling significant performance improvement. In this talk, we describe recent results along these lines and present challenges and opportunities for future research on optimizing runtime monitoring.
Martin Odersky Professor, Programming Methods Group, EPFL, Lausanne, Switzerland Contracts in Scala (http://www.scala-lang.org) Abstract: Scala is a high-level language that combines functional and object-oriented programming constructs. Its flexible syntax makes it suitable for embeddings of domain-specifc languages. Scala is used as an extension language of the automatic theorem prover Isabelle and there are also a range of projects for the verification and automated testing of Scala programs. A question raised by these projects is in what way and to what degree Scala can support its own specifications as an embedded DSL. In this talk I will give an overview of Scala, and will highlight work being done on verification, automated testing and program synthesis in the Scala context.
Wim De Pauw Researcher, IBM T.J. Watson Research Center, New York, USA Visualizing Complex IT Systems Abstract: Information technology systems have become increasingly complex. As a result, understanding, debugging or profiling these systems with classic text-based tools has become more and more challenging. At the IBM T.J. Watson Research Center we are doing research on visual tools to support the understanding of complex IT systems. The domain of software visualization draws from several other scientific domains, such as information visualization, tracing and debugging techniques, management of complex systems, pattern extraction and human-computer interaction. In this talk, we will illustrate our research on software visualization with demos of tools visualizing the behavior of Java applications, Web Services, Stream Processing systems and mainframe operating systems. Finally, we will also propose new visual debugging techniques for developing streaming applications.
R. Sekar Professor, Department of Computer Science Director, Center for Cybersecurity, Stony Brook University, NY, USA Runtime Analysis and Instrumentation for Securing Software Abstract: The past decade has witnessed an explosive increase in the scale, intensity and sophistication of cyber attacks. While software vendors have significantly increased their efforts on security, they are almost always playing "catch up." As a result, security-conscious organizations and individuals have come to expect their system administrators to deploy an array of tools and techniques to stay a step ahead of the hackers. While developer-oriented security tools rely mainly on static analysis, runtime analysis and policy enforcement are the mechanisms of choice in administrator-oriented tools. The increased automation and precision offered by runtime techniques are more suitable in this context since administrators don't have the time or resources needed to acquire extensive knowledge about the internals of a software system. In this talk, I will begin by summarizing some of the impressive advances that have been achieved in the past few years in the context of software vulnerability mitigation, including buffer overflow defenses, and more recently, the impressive results that have been achieved using dynamic information-flow analysis for blocking the most popular exploits today, including SQL and command injection and cross-site scripting. I will then proceed to describe dynamic analysis and enforcement techniques aimed at another high-profile security problem faced today, namely, malware defense. Our initial target in this regard has been on dynamic analysis techniques for extracting high-level models of program behavior. These models could be used in a variety of applications such as intrusion detection, vulnerability analysis and security policy verification. More recently, interesting advances have been made in the context of security policy development, where a combination of static and dynamic analysis techniques have been developed to synthesize low-level, enforceable policies that achieve a high-level goal such as protecting system integrity from untrusted software. Finally, I will conclude the talk with a discussion of research opportunities and challenges in software security.