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
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.
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.
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.
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.
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