NJPLS at Rutgers, December 10, 2010

This instance of NJPLS will take place in the first-floor auditorium of Rutgers's CoRE (Computing Research and Education) building (40.5213,-74.4612). (Lunch will be served in room 301, on the third floor.)

Transportation

By train

Take New Jersey Transit to New Brunswick station (e.g., train 3934 from Trenton arriving at 9:19am or train 3827 from New York arriving at 9:23am), then do one of the following.

Take a cab (about $20; about 15 minutes)

Cabs will be waiting downstairs from the east end of the platform. The driver should take Route 18 north across the river, then take the second exit, labelled "Busch Campus". Go straight through the traffic circle onto Frelinghuysen Rd, then take the next right onto a cul de sac that ends in front of the CoRE building.

Take a campus bus (free; about 20 minutes)

Go to the east end of the platform, walk downstairs, go under the tracks if you came on an eastbound train, then turn left onto Somerset St. Walk a block on Somerset St and make a right onto College Ave at the turnstile intersection. Walk a block on College Ave and cross Hamilton St, then wait at the bus shelter on your left, labelled "Scott Hall". Take the next A or H bus (labelled "Busch").

• If you take the A bus, get off at the Hill Center stop, which is several stops after crossing the river. Hill Center is to your right, behind the bus, up the stairs. The CoRE building is behind Hill Center; walk to the left of Hill Center.
• If you take the H bus, get off at the Werblin gym stop, which is immediately after crossing the river. Werblin gym is across the street. The CoRE building is behind Werblin; walk to the right of Werblin gym, across the parking lot.

Bike (about 15 minutes) or walk (about 45 minutes)

Use Google's bicycling directions to 40.5207,-74.4622 or follow my route ("Calm in the morning").

By car

Please park in Lot 64 (40.5207,-74.4605), unless you are faculty, staff, or a student at Rutgers. After taking the Route 18 exit labelled "Busch Campus", turn right at the traffic circle onto Bartholomew Rd, then take the next left onto Brett Rd. Park in the lot to the left; the CoRE building is at the end of the lot, behind the trees.

Agenda

Abstracts

Making prophecies with decision predicates

We describe a new algorithm for proving linear temporal logic (LTL) properties of infinite-state programs. Our approach takes advantage of the fact that LTL properties can often be proved more efficiently using techniques usually associated with the branching-time logic CTL than they can with native LTL tools. The caveat is that, in certain instances, nondeterminism in the system's transition relation can cause CTL methods to report counterexamples that are spurious with respect to the original LTL formula. To address this problem we describe an algorithm that, as it attempts to apply CTL proof methods, finds and then removes problematic nondeterminism via an analysis on the potentially spurious counterexamples. Problematic nondeterminism is characterized using decision predicates, and removed using a partial and symbolic determinization procedure that introduces new prophecy variables to predict the future outcome of these decisions.

We demonstrate—using examples taken from the PostgreSQL database server, Apache web server, and Windows OS kernel—that our method can yield enormous performance improvements in comparison to known tools, allowing us to automatically prove properties of programs where we could not prove them before.

Transcript: a system for speculative execution of untrusted JavaScript code

Transcript is a system that enhances the JavaScript language with support for speculative execution. It introduces a new 'transaction' construct, which hosting Web applications can use to demarcate regions that contain untrusted guest code. Actions performed within a transaction are logged and considered speculative until they are examined by the host and committed; uncommitted actions simply do not take and cannot affect the host in any way. Transcript therefore provides hosting Web applications with powerful mechanisms to mediate the actions of untrusted guests. It also allows hosts to cleanly recover from the effects of security-violating guest code.

This is joint work with Vinod Ganapathy and Chung-chieh Shan.

Modular analysis via abstract reduction semantics

Modular static analysis requires treating some portion of the program opaquely. To enable such analysis, we introduce a notion of abstract reduction semantics. Opaque components are approximated by their specifications, which in turn are treated as abstract values during reduction. We demonstrate the technique by applying it to two kinds of specifications for higher-order languages: types and first-class contracts, showing that each soundly approximates opaque components. Finally, we derive modular static analyzers from these semantics, soundly predicting evaluation, contract violations, and blame assignment.

Polymorphic contracts

Manifest contracts track precise properties by refining types with predicates—e.g., {x:Int | x > 0} denotes the positive integers. Contracts and polymorphism make a natural combination: programmers can give abstract types strong contracts, precisely stating pre- and post-conditions while hiding implementation details—for example, an abstract type of stacks might specify that the pop operation has input type {x:'a Stack | not(empty x)}. We formalize this combination by defining FH, a polymorphic calculus with manifest contracts, and establishing its fundamental properties, including type soundness and relational parametricity. Our development relies on a significant technical improvement over earlier presentations of contracts: instead of introducing a denotational model to break a problematic circularity between typing, subtyping, and evaluation, we develop the metatheory of contracts in a completely syntactic fashion, omitting subtyping from the core system and recovering it post facto as a derived property.

This is joint work with Joao Belo, Atsushi Igarashi, and Benjamin Pierce.

Yarra: an extension to C for data integrity and partial safety

Modern applications contain libraries and components written by different people at different times in different languages, often including unsafe languages like C or C++. As a result, one bug, such as a buffer overflow, in any component, can compromise the security and reliability of every other component. To help mitigate these problems, we introduce Yarra, a conservative extension to C with mechanisms for enforcing data integrity and partial safety, even when code is linked against unknown C libraries or binaries. Yarra programmers specify their data integrity requirements by declaring critical data types and ascribing these critical types to important data structures. Yarra guarantees that such critical data is only written through pointers with the given static type. Any attempt to write to critical data through a pointer with an invalid type (perhaps because of a buffer overrun) is detected dynamically.

We formalize Yarra’s semantics and prove the soundness of a program logic designed for use with the language. A key contribution is to show that Yarra’s semantics are strong enough to support sound local reasoning and the use of a frame rule, even across calls to unknown, unverified code. We also demonstrate that Yarra’s semantics can be implemented in several different ways, with different performance and pragmatic trade-offs. In one implementation, we perform a source-to-source program transformation to ensure correct execution. In a second implementation, we do not rely upon having access to the entire source code, but instead use conventional hardware permissions to protect critical data. We evaluate our implementations using SPEC benchmarks to understand their performance. Additionally, we apply Yarra to four common applications with known non-control data vulnerabilities. We are able to use Yarra to defend against these attacks while sustaining a negligible impact on their end-to-end performance.

This is joint work with Dave Walker (Princeton University), Karthik Pattabiraman (University of British Columbia), Nikhil Swamy (Microsoft Research) and Ben Zorn (Microsoft Research).

Bridging the functional-imperative divide

In this talk we present an operational/denotational semantics for a higher-order language with both functional and imperative features and an equational axiomatization of state and program equivalence. A key feature is a significantly simplified mathematical definition of closures for mutable bindings that avoids the explicit modeling of memory and captures completely the state of a computation without reference to context. The approach allows us to restrict attention to simple types and to provide an equational axiomatization that captures the notion of value and value in context. We prove full abstraction for an imperative language and for a functional language similar to PCF.

This is joint work with Dexter Kozen.