**Arrival and Coffee: 9:30 - 10:00**

**Session 1: 10:00 - 10:45**

Nate Foster (University of Pennsylvania)

A Logic Your Typechecker Can Count On: Unordered Tree
Types in Practice

**Break: 10:45 - 11:00**

**Session 2: 11:00 - 12:30**

Chung-chieh Shan (Rutgers)

A Substructural Type System for Delimited
Continuations

Xinyi Feng (Yale University)

On the Relationship between Concurrent Separation Logic and
Assume-Guarantee Reasoning

**Lunch: 12:30 - 1:50**

**Business meeting: 1:50 - 2:00**

**Session 3: 2:00 - 3:30**

Octavian Udrea (University of Maryland)

Rule-Based Static Analysis of Network Protocol Implementations

Katia Hristova (SUNY Stonybrook)

Efficient Type Inference for Secure Information Flow

Nate Foster (University of Pennsylvania)

**Abstract:**
Type systems featuring counting constraints are often studied, but
seldom implemented. We describe an efficient implementation of a type
system for unordered, edge-labeled trees based on Presburger
arithmetic constraints. We begin with a type system for unordered
trees and give a compilation into counting automata. We then describe
an optimized implementation that provides the fundamental operations
of membership and emptiness testing. Although each operation has
worst-case exponential complexity, we show how to achieve reasonable
performance in practice using a combination of techniques, including
syntactic translations, lazy automata unfolding, hash-consing,
memoization, and incremental tree processing implemented using partial
evaluation. These techniques avoid constructing and examining large
structures in many cases and amortize the costs of expensive
operations across many computations. To demonstrate the effectiveness
of these optimizations, we present experimental data from executions
on realistically sized examples drawn from the Harmony data
synchronizer.

Chung-chieh Shan (Rutgers)

**Abstract:**
We propose type systems that abstractly interpret small-step rather than
big-step operational semantics. We treat an expression or evaluation
context as a structure in a linear logic with hypothetical reasoning.
Evaluation order is not only regulated by familiar focusing rules in the
operational semantics, but also expressed by structural rules in the
type system, so the types track control flow more closely. Binding and
evaluation contexts are related, but the latter is linear.

We use these ideas to build a type system for delimited continuations. It lets control operators change the answer type or act beyond the nearest dynamically-enclosing delimiter, yet needs no extra fields in judgments and arrow types to record answer types. The typing derivation of a direct-style program desugars it into continuation-passing style.

Xinyi Feng (Yale University)

**Abstract:**
We study the relationship between Concurrent Separation Logic (CSL)
and the assume-guarantee (A-G) method (a.k.a. rely-guarantee
method). We show in three steps that CSL can be treated as a
specialization of the A-G method for well-synchronized concurrent
programs. First, we present an A-G based program logic for a low-level
language with built-in locking primitives. Then we extend the program
logic with explicit separation of ``private data'' and ``shared
data'', which provides better memory modularity. Finally, we show that
CSL (adapted for the low-level language) can be viewed as a
specialization of the extended A-G logic by enforcing the invariant
that "shared resources are well-formed outside of critical
regions". This work can also be viewed as a different approach (from
Brookes') to proving the soundness of CSL: our CSL inference rules are
proved as lemmas in the A-G based logic, whose soundness is
established following the syntactic approach to proving soundness of
type systems.

Joint work with Rodrigo Ferreira and Zhong Shao.

Octavian Udrea (University of Maryland)

**Abstract:**
Today's software systems communicate over the Internet using standard
protocols that have been heavily scrutinized, providing some assurance
of resistance to malicious attacks and general robustness. However,
the software that implements those protocols may still contain
mistakes, and an incorrect implementation could lead to
vulnerabilities even in the most well-understood protocol. The goal
of this work is to close this gap by introducing a new technique for
checking that a C implementation of a protocol matches its description
in an RFC or similar standards document. We present a static
(compile-time) source code analysis tool called Pistachio that checks
C code against a rule-based specification of its behavior. Rules
describe what should happen during each round of communication, and
can be used to enforce constraints on ordering of operations and on
data values. Our analysis is not guaranteed sound due to some
heuristic approximations it makes, but has a low false negative rate
in practice when compared to known bug reports. We have applied
Pistachio to two different implementations of SSH2 and an
implementation of RCP. Pistachio discovered a multitude of bugs,
including security vulnerabilities, that we confirmed by hand and
checked against each project's bug databases.

Joint work with Cristian Lumezanu and Jeff Foster.

Katia Hristova (SUNY Stonybrook)

**Abstract:** We describe the design, analysis, and
implementation of an efficient algorithm for information flow analysis
expressed using a type system. Given a program and an environment of
security classes for information accessed by the program, the
algorithm checks whether the program is well typed, which ensures that
no information of higher security classes flows into locations with
lower security classes, by inferring the highest or lowest security
class, as appropriate, for each program node. We express the analysis
as a set of extended Datalog rules based on the typing and subtyping
rules, and we use a systematic method to generate specialized
algorithms and data structures directly from the extended Datalog
rules. The generated implementation traverses the program multiple
times and uses a combination of linked and indexed data structures to
represent program nodes, environments, and types. The time complexity
of the algorithm is linear in the size of the input program, times the
height of the lattice of security classes, plus an overhead for
preprocessing the lattice. This complexity is confirmed through our
prototype implementation and experimental evaluation on code generated
from high-level specifications for real systems.

A preliminary version of this paper appeared in PLAS'06. Joint work with Tom Rothamel, Yanhong A. Liu, and Scott D. Stoller

Jeff Foster put together the schedule.