Here are directions to the CS department at UMCP. We will have the meeting in room 3120 of the Computer Science Instructional Center (CSIC). Here is location information on CSIC. Click the "Location" link to see a campus map for each building. Here are floorplans of CSIC.
Location: 3120 CSIC
Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 11:30
Iulian Neamtiu (University of Maryland, College Park)
Contextual Effects for Version-Consistent Dynamic Software Updating
and Safe Concurrent Programming
Frances Perry (Princeton University)
Reasoning about Control Flow in the Presence of Transient
Faults
Lunch: 11:30 - 12:50
Business meeting: 12:50 - 1:00
Session 2: 1:00 - 2:30
Christopher Conway (New York University)
Pointer Analysis, Conditional Soundness, and Proving the Absence of
Errors
David Naumann (Stevens Institute of Technology)
Expressive Declassification Policies and Modular Static
Enforcement
Break: 2:30 - 2:45
Session 3: 2:45 - 3:30
Nate Foster (University of Pennsylvania)
Boomerang: Resourceful Lenses for String Data
A LENS is a bidirectional program. When read from left to right, it denotes an ordinary function that maps inputs to outputs. When read from right to left, it denotes an ``update translator'' that takes an input together with an updated output and produces a new input that reflects the update. Many variants of this idea have been explored, but none deal fully with ORDERED data. If, for example, an update changes the order of a list in the output, the items in the output list and the chunks of the input that generated them from can be misaligned, leading to lost or corrupted data. We attack this problem in the context of bidirectional transformations over strings, the primordial ordered data type.
We first propose a collection of bidirectional STRING LENS COMBINATORS, based on familiar operations on regular transducers (union, concatenation, Kleene-star) and with a type system based on regular expressions. We then design a new semantic space of DICTIONARY LENSES, enriching the lenses of Foster et al. to support two additional combinators for marking ``reorderable chunks'' and their keys. To demonstrate the effectiveness of these primitives as a foundation for programming bidirectional string transformations, we describe the design and implementation of Boomerang, a full-blown BIDIRECTIONAL PROGRAMMING LANGUAGE with dictionary lenses at its core. We have used Boomerang to build transformers for complex real-world data formats including the SwissProt genomic database.
We formalize an essential feature of RESOURCEFULNESS---the correct use of keys to associate chunks in the input and output---by defining a refined space of QUASI-OBLIVIOUS LENSES. Several previously studied properties of lenses turn out to have compact characterizations in this space.
This talk describes a way to specify expressive information policies including when, what, and where policies that include conditions under which downgrading is allowed. An end-to-end semantic property is introduced, based on a model that allows observations of intermediate low states as well as termination. An attacker's knowledge only increases at explicit declassification steps, and within limits set by policy. Practical means of enforcement is provided, by combining type-checking with program verification techniques applied to the small subprograms that carry out declassifications. Verification exploits a novel logic of regions.
This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression $e$. Our system additionally computes the effects of the computational context in which $e$ occurs: both the effect of the computation that has already occurred (prior effects) and the effect of the computation yet to take place (future effects).
Contextual effects can be used in any application in which the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency (TVC), a novel correctness property for dynamic software updates. TVC ensures that programmer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.
Joint work with David Walker
A transient fault is a temporary, one-time event that causes a change in state or erroneous signal transfer in a digital circuit. These faults do not cause permanent damage, but when they strike conventional processors, they may result in incorrect program execution. While detecting and correcting faults in first-order data may be accomplished relatively easily by adding redundancy, protecting against faults during control flow transfers is substantially more difficult. In this talk, we analyze the problem of maintaining the control-flow integrity of a program in the face of transient faults from a formal theoretical perspective. More specifically, we augment the operational semantics of an idealized assembly language with additional rules that model erroneous control-flow transfers. Next, we explain a strategy for detecting control-flow errors in software based on previous work by Oh and Reis. In order to reason about the correctness of the strategy relative to our fault model, we develop a new assembly-level type system designed to guarantee that any control flow transfer to an incorrect block will be caught before control leaves that block. Our key technical result is a rigorous proof of this fundamental control-flow property for well-typed programs.
Joint work with: Dennis Dams (Bell Labs), Kedar S. Namjoshi (Bell Labs), and Clark Barrett (NYU)
It is well known that the use of points-to information can substantially improve the accuracy of a static program analysis. Commonly used algorithms for computing points-to information are known to be sound only for programs that have no memory errors. It thus appears impossible to utilize points-to information in an analysis of memory safety, without giving up soundness. The main result of this paper shows that a sound combination is possible, even if the points-to information is obtained independently. This result is based on a refined statement of the conditions under which a points-to analysis is sound and a general mechanism for combining conditionally sound analyses.