[logo suggestions welcome]


These abstracts are for talks at this event.

NEPLS is a venue for ongoing research, so the abstract and supplemental material associated with each talk is necessarily temporal. The work presented here may be in a state of flux. In all cases, please consult the authors' Web pages for up-to-date information. Please don't refer to these pages as a definitive source.

Compiling Cryptographic Protocols for Deployment on the Web

Jay McCarthy (Brown), Joshua Guttman (MITRE), John Ramsdell (MITRE), Shriram Krishnamurthi (Brown)

Cryptographic protocols are useful for trust engineering in Web
transactions.  The Cryptographic Protocol Programming Language (CPPL)
provides a model wherein trust management annotations are attached to
protocol actions, and are used to constrain the behavior of a protocol
participant to be compatible with its own trust policy.

The first implementation of CPPL generated stand-alone, single-session
servers, making it unsuitable for deploying protocols on the Web. We
describe a new compiler that uses a constraint-based analysis to
produce multi-session server programs.  The resulting programs run
without persistent TCP connections for deployment on traditional Web
servers.  Most importantly, the compiler preserves existing proofs
about the protocols.  We present an enhanced version of the CPPL
language, discuss the generation and use of constraints, show their
use in the compiler, formalize the preservation of properties, present
subtleties, and outline implementation details.

This paper will appear at WWW 2007 and is available at http://www2007.org/paper140.php.

Verification of Network Flows Using a Type System with Constrained Polymorphism

LiKai Liu, Azer Bestavros, Assaf Kfoury, Abraham Matta (Boston University)

We propose a typed domain-specific language TRAFFIC(X) for the
specification and analysis of end-to-end network flow
configurations. TRAFFIC(X) is inspired by HM(X), a framework that
augments the familiar Hindley-Milner polymorphic type system for
ML-like functional languages with a constraint system X. In
TRAFFIC(X), the constraint system X can be instantiated to different
constraint-rewriting rules, corresponding to the verification of
different properties of network flows. To illustrate our methodology,
we examine two examples: (1) proper nesting of tunneled streams by
means of lossy or lossless compression and encryption; and (2)
computing round-trip time using linear-programming constraints.

This talk presents work done in collaboration with Azer Bestavros, Abraham Matta, and Assaf Kfoury at Boston University. For more information on this project, see csr.bu.edu/traffic.

Jeannie: making the Java Native Interface Pretty and Light-Weight

Martin Hirzel (IBM), Robert Grimm (NYU)

Many programs are written in more than one language. Reasons for this
include reuse of legacy libraries, access to platform functionality,
and efficiency. Jeannie is a language design for integrating Java with
C, aiming at programmer productivity, static and dynamic error
checking, portability, and efficiency.  Both Java code and C code are
nested in each other in the same file, and compile down to traditional
JNI. Jeannie performs static semantic checks and facilitates dynamic
resource management and exception handling, two concerns that
otherwise make JNI applications ugly and heavy-weight. This talk
reports on our experiences from a prototype Jeannie compiler, and
highlights areas for future work on language interoperability.

LADDIE: The Language for Automated Device Drivers

Lea Wittie, Derrin Pierret (Bucknell University)

Device drivers are known to be a main source of OS bugs.
Several research groups have created driver specification languages
that dynamically check pre- and postconditions on the IO operations 
of a device driver. Low level type safe languages exist that can 
statically check function pre- and postconditions. However, these 
low level languages are too general to make the specific task of 
driver writing simple. This research presents Clay, a low level type 
safe language that has the facilities to statically check the safety
of a device driver, and Laddie, a device driver specification language
which compiles to Clay thus leveraging its static safety checking
while remaining simple to use.

Clay, developed at Dartmouth, is a C-like language which dependent 
types, like those of DML, to track program values statically. It
builds on the linear logic of Girard to produce linear capabilities 
which guard access to memory and to logical system state and prevent 
aliasing errors. Clay also incorporates the arithmetic constraints of 
Xi and Pfenning into function pre- and postconditions to produce Hoare 
Triples, {P} f {Q} where P and Q are pre- and postconditions on function f.
Clay statically enforces linear access to memory and statically checks all
pre- and post conditions on function calls. When successfully type
checked, a Clay program then compiles to C++.

There are several existing specification languages for device drivers
including Devil, NDL, and Hail. All of these perform dynamic safety 
checks. To move the safety checks to compile time, we created Laddie, 
a language for specifying the IO communication between a driver and
its device. Devices are typically accessed via a set of locations
called registers. Each register has rules governing how and when it
can be accessed. These rules may depend on the logical state of the
device, which is not usually stored in driver memory. (This state
might include the status of device interrupts). Laddie uses syntax
similar to that of Hail to allow a simple encoding of the complex
rules and logical device state into pre- and postconditions on access
to registers. Laddie compiles to Clay which checks the pre- and
postconditions statically. 

This talk presents work done in collaboration with Chris Hawblitzel (Microsoft Research) and Derrin Pierret (undergraduate at Bucknell University). For more information on Laddie and Clay, see http://www.eg.bucknell.edu/~lwittie/research.html.

Building an Efficient Generational Garbage Collector for Java Application Servers

Feng Xian, Witawas Srisa-an, ChengHuan Jia, Hong Jiang (University of Nebraska, Lincoln)

Recent studies have found that generational collection strategies
employing only one nursery do not not perform well in application
servers due to their inability to efficiently manage objects with
diverse lifespans. In this presentation, we introduce a generational
collector that takes advantage of an intrinsic behavior of many
application servers; that is remotable objects are commonly used as
gateways for client requests, and objects instantiated as part of
these requests (remote objects) tend to live longer than objects not
created to serve remote requests (local objects). This insight is used
to segregate remote and local objects in two separate nurseries; each
is properly sized to allow sufficient time for objects to die. We have
implemented the proposed collector in the HotSpot virtual machine and
evaluated its performance in a real-world application server
setting. Given the same heap size, the proposed scheme can improve the
maximum throughput by as much as 14% over the default generational
collector. In addition, the proposed scheme allows the application
server to handle a 10% higher workload before memory is exhausted.
Our collector can achieve such performance benefits because it can
reduce the frequency of full collection invocations, paging effort,
average pause time, and overall garbage collection time.

This is a joint work with Feng Xian, ChengHuan Jia, and Hong Jiang. More information about this work can be found here.

Exterminator: Automatically Correcting Memory Errors with High Probability

Gene Novark (UMass Amherst)

Programs written in C and C++ are susceptible to memory errors,
including buffer overflows and dangling pointers. These errors, which
can lead to crashes, erroneous execution, and security
vulnerabilities, are notoriously costly to repair. Tracking down their
location in the source code is difficult, even when the full memory
state of the program is available. Once the errors are finally found,
fixing them remains challenging: even for critical security-sensitive
bugs, the average time between initial reports and the issuance of a
patch is nearly one month.

We present Exterminator, a system that automatically corrects
heap-based memory errors without programmer intervention. Exterminator
exploits randomization to pinpoint errors with high precision. From
this information, Exterminator derives runtime patches that fix these
errors both in current and subsequent executions. In addition,
Exterminator enables collaborative bug correction by merging patches
generated by multiple users. We present analytical and empirical
results that demonstrate Exterminator's effectiveness at detecting and
correcting both injected and real faults.

This talk presents joint work with Emery Berger (UMass Amherst) and Ben Zorn (Microsoft Research). Our paper can be found at http://www.cs.umass.edu/~emery/pubs/pldi028-novark.pdf

Space-Efficient Gradual Typing

David Herman (Northeastern University), Aaron Tomb, Cormac Flanagan (UC Santa Cruz)

Gradual type systems offer a smooth continuum between static and
dynamic typing by permitting the free mixture of typed and untyped
code. The runtime systems for these languages---and other languages
with hybrid type checking---typically enforce function types by
dynamically generating function proxies. This approach can result in
unbounded growth in the number of proxies, however, which drastically
impacts space efficiency and destroys tail recursion.

We present an implementation strategy for gradual typing that is based
on coercions instead of function proxies, and which combines adjacent
coercions to limit their space consumption. We prove bounds on the
space consumed by coercions as well as soundness of the type system,
demonstrating that programmers can safely mix typing disciplines
without incurring unreasonable overheads. Our approach also detects
certain errors earlier than prior work.

This talk presents joint work done with Aaron Tomb and Cormac Flanagan (University of California, Santa Cruz). Our paper can be found at http://www.ccs.neu.edu/home/dherman/research/publications/tfp07-gradual-typing.pdf.

Spatial Computing with Proto

Jonathan Bachrach, Jacob Beal (MIT)

Spatial computing is an increasingly prevalent mode of computing, in
which a program runs on a collection of devices spread through space
whose ability to interact is strongly dependent on their geometry.
Spatial computing arises in many domains: sensor networks, smart
materials, swarm robotics, biofilms, and modular robotics, to name a
few.  Programmability has been a major barrier to the deployment of
spatial computing systems.  Applications become entangled with the
details of coordination and robustness, and as a result we see a
plethora of niche solutions which often do not scale or compose well,
let alone translate to other application domains.  We offer an
alternate approach, in which the application programmer expresses
programs in terms of the global behavior of an {\em amorphous
medium}---a continuous computational material filling the space of
interest.  We accomplish this with two components: a programming
language, called Proto, for a spatial computer which implements the
{\em amorphous medium} abstraction and a distributed operating system
which marshalls a collection of devices into a virtual spatial
computer implementing Proto semantics approximately.  Proto has been
demonstrated on platforms in three spatial computing domains: sensor
networks, swarm robotics, and modular robotics.

Last modified Saturday, April 7th, 2007 6:51:59amPowered by PLT