Agenda
Attendees are welcome from 9:30 onwards and are encouraged to use this opportunity to meet other researchers.
Session 1: 10:30 - 12:05
(Keynote presentation)
Matthias Felleisen, Northeastern University:
Next Generation Software Systems and Programming
Language Research
Dominic Duggan, Stevens Institute of Technology:
Cryptographic Types
Session 2: 1:30 - 3:15
Darko Marinov, MIT:
An Analyzable Annotation Language
Perry Cheng, IBM Research:
A Defragmenting, Mostly Non-moving Garbage
Collector
Scott
Stoller, SUNY Stonybrook:
Domain Partitioning for Open Reactive Systems
Session 3: 3:45 - 5:00
Dan Grossman, Cornell University:
Cyclone: A Safe Language at the C Level of Abstraction
Nadeem Abdul Hamid, Yale University:
A Syntactic Approach to Foundation Proof-Carrying
Code
Abstracts:
Next
Generation Software Systems and Programming Language Research
Matthias Felleisen, Northeastern University:
Future software systems will consist of reusable components. They will also provide interfaces for third-party programmers to extend the systems statically as well as dynamically. A Web browser, for example, allows users to add plug-ins and applets. Similarly, mail clients can execute attached "macro" programs, and users can specify mime-type specific application tools.
Programming language research must support this emergent form of system design because it poses new problems for programmers and systems architects. Researchers will have to study a wide range of problems, including the design of constructs for the implementation and composition of components; the development of mechanism for monitoring and enforcing invariants across components; the development of run-time systems in support of dynamic extensibility; and the evolution of new programming paradigms. Programming environments that assist with the analysis and synthesis of componential and extensible software will be an additional focus of programming language research.
In my talk, I will first present the basic problems with a concrete example: the design and implementation of a Web server for fast and convenient dynamic content generation. Based on this example, I will provide an overview of my team's recent and future research efforts on programming language support for building such extensible systems: language support for reusable components; the design and implementation of extensible abstract data types; the administration of resources; and the specification and enforcement of behavioral contracts for components.
Cryptographic
Types
Dominic Duggan Stevens Institute of Technology
Networks
secured by cryptographic techniques can be likened to programming
languages where all type-checking is performed at run-time: cryptographic
operations such as signature checking and decryption are analogous
to run-time dynamic type-checking. Languages such as Java allow
a combination of static and dynamic type-checking in distributed
programming. Cryptographic types are a way to express cryptographic
guarantees (of secrecy and integrity) in a type system for a network
programming language. This allows some of these guarantees to be
checked statically, before a network program executes. Where dynamic
checks are required, these are represented at the source language
level as dynamic checking, and are translated by the compiler to
lower level cryptographic operations for encryption/decryption and
signing/authentication. Static checking avoids the unnecessary overhead
of run-time cryptographic operations where communication is through
a trusted medium (e.g. the OS kernel, or a trusted subnet), and
also provides static guarantees of the reliability of a network
application. Cryptographic types can also be used to build application-specific
security protocols, where
type-checking in the lower layers of the protocol stack verifies
security properties for upper layers. Cryptographic types are described
formally using a process calculus, the ec-calculus, allowing the
correctness to be verified for a scheme for compiling type operations
to cryptographic operations.
An
Analyzable Annotation Language
Sarfraz Khurshid, Darko Marinov, and Daniel Jackson
LCS, MIT
The Alloy
Annotation Language (AAL) is a language for annotating Java code
based on the Alloy modeling language. It offers a syntax similar
to the Java Modeling Language (JML), and the same opportunities
for generation of run-time assertions. In addition, however, AAL
offers the possibility of fully automatic compile-time analysis.
Several
kinds of analyses are supported, including: checking the code of
a method against its specification; checking that the specification
of a method in a subclass is compatible with the specification in
the superclass; and checking properties relating method calls on
different objects, such as that the equals methods of a class (and
its overridings) induce an equivalence. Using partial models in
place of code, it is also possible to analyze object-oriented designs
in the
abstract: investigating, for example, a view relationship amongst
objects.
The paper
gives examples of annotations and such analyses. It presents (informally)
a systematic translation of annotations into Alloy, a simple first-order
logic with relational operators. By doing so, it makes Alloy's automatic
analysis, which is based on state-of-the-art SAT solvers, applicable
to the analysis of object-oriented programs, and demonstrates the
power of a simple logic as the basis for an annotation language.
A
Defragmenting, Mostly Non-moving Garbage Collector
David Bacon, Perry Cheng
IBM Research
Our goal is to design a real-time garbage collector for Java targeted for uniprocessor embedded systems. The most basic choice in designing a collector is choosing whether it will be copying or non-copying. While previous work has demonstrated the feasibility of developing real-time copying collectors, the factor of two in space overhead inherent in copying collectors makes this choice unattractive for embedded systems. On the other hand, mark-sweep collectors do not have to pay the doubled space cost. Instead, they are subject to fragmentation which effectively increases memory consumption.
To achieve the goal of real-time collection with good bounded memory usage, we designed our collector to be a mostly non-moving collector with on-demand incremental defragmentation. We present initial results for a stop-the-world prototype to show the feasibility of the design. Our experiments show that a Brooks-style read barrier can be implemented in an optimizing compiler with under 5% overhead on the SPECjvm98 benchmarks.
We implemented our defragmenting collector in a segregated free-list allocator and showed that the SPECjvm98 benchmarks can be run with no more than 10% over the theoretical minimum heap size. For the SPECjvm98 benchmarks, we found the conventional wisdom that programs only allocate objects from a small set of sizes is false. We explore the implications of this property on both segregated free-list and defragmenting systems.
Domain
Partitioning for Open Reactive Systems
Scott Stoller, SUNY Stonybrook
Testing or model-checking an open reactive system often requires generating a model of the environment. We describe a static analysis for Java that computes a partition of a system's inputs: inputs in the same equivalence class lead to identical behavior. The partition provides a basis for generation of code for a most general environment of the system, i.e., one that exercises all possible behaviors of the system. The partition also helps the generated environment avoid exercising the same behavior multiple times. Many distributed systems with security requirements can be regarded as open reactive systems whose environment is an adversary-controlled network. We illustrate our approach by applying it to a fault-tolerant and intrusion-tolerant distributed voting system and model-checking the system together with the generated environment.
Cyclone:
A Safe Language at the C Level of Abstraction
Dan Grossman, Cornell University
Memory safety and type safety are invaluable features for constructing reliable software and enforcing abstractions such as abstract data types and access controls. However, most safe safe languages are at a high level of abstraction; programmers cede almost all control over data representation and memory management. For this (and other) reasons, C remains the de facto standard for writing systems software or extending legacy systems already written in C.
The Cyclone project aims to bring safety to C-style programming without sacrificing the programmer control necessary for low-level software. Of course, this task involves difficult trade-offs among performance, language expressiveness, and programmer convenience. This talk will highlight Cyclone's design principles with an emphasis on how its advanced type system captures important C idioms while remaining usable by C programmers. Examples will give the flavor of Cyclone programming and give a sense of how the language "all fits together".
Cyclone is joint work with Trevor Jim (AT&T Research), Greg Morrisett, Michael Hicks, James Cheney, and Yanling Wang (Cornell University)
A
Syntactic Approach to Foundation Proof-Carrying Code
Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier,
and Zhaozhong Ni
Yale University
Proof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. Foundational Proof-Carrying Code (FPCC), on the other hand, constructs and verifies its proofs using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base.
Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and higher-order polymorphism.
In this talk, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker while the latter is known to be much easier to construct than the semantic soundness proofs. We present a comprehensive translation from a typed assembly language into FPCC, demonstrate the advantages of our new system, and describe an implementation in the Coq proof assistant.
More information is available. Ganesan Ramalingam will be making the local arrangments and overseeing the program selection process. Because of the larger number of participants, there will be a slightly more involved procedure for volunteering to talk.