Arrival and Coffee: 9:30 - 10:00
Session 1: 10:00 - 10:45
David August (Princeton)
Liberating threads from sequential programs
Break: 10:45 - 11:15
Session 2: 11:15 - 12:00
Dimitrios Vytiniotis
An open and shut typecase
Lunch: 12:00 - 1:50
Business meeting: 1:50 - 2:00
Session 3: 2:00 - 3:30
Michale Furr (Maryland)
Checking type safety of foreign functions calls
Peng Li (University of Pennsylvania)
Downgrading policies for information-flow control
Abstract: A fundamental change is happening in computer architecture. For years, a variety of techniques to increase clock speed could be relied upon to consistently deliver increased performance. Recently, however, these techniques have failed. Last year, for example, Intel delayed its planned release of a 4GHz Pentium 4 before ultimately canceling the project. Now, at a time when even relatively recent projections had us at 10GHz, still no plan for a 4GHz part exists. Meanwhile, investments in architectural techniques to dynamically extract parallelism, once promising, are now also exhibiting flat returns.
On the bright side, the exponential growth in transistor count remains strong (for now). As a result, all major microprocessor companies are beginning to produce designs incorporating multiple processors on a chip. Unfortunately, designers have no means to reliably provide these multiple processor resources with independent threads. To address this problem, we present a new pipelined approach to extracting concurrent threads from general purpose programs, called decoupled software pipelining (DSWP). DSWP is made effective by several important technologies including a new interprocessor communication mechanism to reduce synchronization overhead, a low-level alias and shape analysis to better resolve memory dependences during the thread extraction process, and a whole program representation to enhance the scope of thread partitioning.
Abstract: Ad-hoc polymorphism is a compelling addition to typed programming languages. It may be used to implement generic operations over complex data structures. The central question we address is related to user-defined types: Once our language supports generativity, how should the behaviour of ad-hoc polymorphic operations change for new types?
We outline existing approaches to ad-hoc polymorphism such as intensional type analysis and Haskell type classes and present our developments: A calculus with a type analysis operator that supports first class extensions to polytypic operations. We discuss examples and fragments of the type system.
This is joint work with Geoff Washburn and Stephanie Weirich.
Abstract: We present a multi-lingual type inference system for checking type safety across a foreign function interface. The goal of our system is to prevent foreign function calls from introducing type and memory safety violations into an otherwise safe language. Our system targets OCaml's FFI to C, which is relatively lightweight and illustrates some interesting challenges in multi-lingual type inference. The type language in our system embeds OCaml types in C types and vice-versa, which allows us to track type information accurately even through the foreign language, where the original types are lost. Our system uses a representational type that can model multiple OCaml types, because C programs can observe that many OCaml types have the same physical representation. Furthermore, because C has a low-level view of OCaml data, our inference system includes a dataflow analysis to track memory offsets and tag information. Finally, our type system includes garbage collection information to ensure that pointers from the FFI to the OCaml heap are tracked properly. We have implemented our inference system and applied it to a small set of benchmarks. Our results show that programmers do misuse these interfaces, and our implementation has found several bugs and questionable coding practices in our benchmarks.
Abstract: In traditional information-flow type systems, the security policy is often formalized as noninterference properties. However, noninterference alone is too strong to express security properties useful in practice. If we allow downgrading in such systems, it is challenging to formalize the security policy as an extensional property of the system.
This talk presents a generalized framework of downgrading policies. Such policies can be specified in a simple and tractable language and can be statically enforced by mechanisms such as type systems. The security guarantee is then formalized as a concise extensional property using program equivalences. This relaxed noninterference implies traditional pure noninterference and precisely characterizes the information released due to downgrading.
Based on the above framework, this talk also discusses a practical application of language-based information-flow control, namely, a domain-specific web scripting language designed for interfacing with databases. The primary goal is to provide strong enforcement of confidentiality and integrity policies: Confidential data can be released only in permitted ways, and trustworthy data must result from expected computations or conform to expected patterns. Such security policies are specified in the database layer and statically enforced for the rest of the system in an end-to-end fashion.
[1] Peng Li and Steve Zdancewic. Downgrading Policies and Relaxed Noninterference. In Proc. of The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Jan. 2005.
[2] Peng Li and Steve Zdancewic. Practical Information-flow Control in Web-based Information Systems. Submitted, Nov. 2004.