TACL Seminar Fall '03
Fall '03 Schedule
|Sep 3||Limin Jia||Modal Proofs as Distributed Programs||Abstract / Paper|
|Sep 4||New Jersey Programming Languages and Systems Day (NJPLS)|
|Sep 12||Dominic Duggan (Stevens)||Type-Based Distributed Access Control||Abstract / Paper|
|Sep 26||Spyros Triantafyllis||LIL: A portable low-level language for expressing runtime support code||Abstract|
|Oct 3||Dinghao Wu||Precise Race Detection Using Sequential Program Analysis and Model Checking||Abstract|
|Oct 17||Iliano Cervesato||MSR 3.0: the Logical Meeting Point of Multiset Rewriting and Process Algebra||Abstract|
|Nov 14||Sotiris Ioannidis (Penn)||Abstraction, Specification and Enforcement of Security Policies for Decentralized Systems||Abstract|
|Nov 21||New Jersey Programming Languages and Systems Seminar (NJPLS)|
|Dec 5||Ge Wang||A Survey of Programming Languages and Systems for Computer Music||Abstract|
|Dec 12||Gang Tan||Construction of a Semantic Model for a Typed Assembly Language||Abstract / Paper|
|Jan 9||David Walker||Stacks, Heaps and Regions: One Logic to Bind Them||Abstract|
Modal Proofs as Distributed Programs
We develop a new foundation for distributed programming languages by defining an intuitionistic, modal logic and then interpreting the modal proofs as distributed programs. More specifically, the proof terms for the various modalities have computational interpretations as remote procedure calls, commands to broadcast computations to all nodes in the network, commands to use portable code, and finally, commands to invoke computational agents that can find their own way to safe places in the network where they can execute. We prove some simple meta-theoretic results about our logic as well as a safety theorem that demonstrates that the deductive rules act as a sound type system for a distributed programming language.
Type-Based Distributed Access Control
The term 'distributed access control' is used here to refer to a weak form of information flow control, one that ensures that access control restrictions on data are propagated to all the places where it is accessed in a distributed system. The motivation for DAC is accountability: building an audit trail based on accesses to data. The key to making this practical is performing the access checks statically, at compile-time.
Various forms of type-based access control and information flow control require that network security be maintained by the runtime rather than the application. This is because the guarantees of the information flow might otherwise be violated by unsafe communication. This talk presents the 'Key-based Decentralized Label Model (KDLM)', an approach to extending a type system for distributed access control to a typed API for cryptographic operations, that ensures that the access control restrictions are preserved by the application's use of cryptography to secure communications. The notion of 'declassification certificates' is introduced to support the declassification of encrypted data.
This is joint work with Tom Chothia (Stevens) and Jan Vitek (Purdue University).
LIL: A portable low-level language for expressing runtime support code
The ORP managed runtime environment consists of a core virtual machine (VM), several just-in-time compilers (JITs), and a garbage collector (GC). In order to avoid exposing the VM, the JITs, and the GC to each other's implementation specifics, ORP employs a call-based runtime-support interface. Whenever the user's code requires runtime support, an ORP JIT generates calls to VM generated code stubs, which may in turn call the GC. LIL is a low-level, architecture-independent language for expressing such code stubs. The first part of the talk describes LIL and its implementation, with emphasis on the LIL code generator for IPF. It demonstrates that LIL makes the development of runtime support stubs much easier, less error-prone, and more portable than the direct generation of such code stubs in machine language. Moreover, these gains in flexibility and maintainability come at negligible performance loss. The second part of the talk describes how LIL can be used in order to implant VM-dependent or GC-dependent code directly into JITed code. This implanting avoids the performance losses associated with a call-based interface yet retains the modularity of ORP's components.
Precise Race Detection Using Sequential Program Analysis and Model Checking
Based on static program analysis and model checking techniques, a precise static race detector, Zen, has been developed for Windows device drivers. However, the technique is applicable to software verification in general. Zen is precise and static. Comparing to other existing race detectors, Zen is not sound (it may miss potential races, but we believe it will catch a large class of races) but complete (or precise; it won't report false alarms). It checks race conditions automatically and requires no annotations from the users.
The novelty of Zen is that it uses sequential program analysis and model checking techniques. The idea of constructing a sequential program to simulate some interleavings for the input multithreaded program is very useful since many existing sequential program analysis techniques such as alias analysis can be used. The biggest challenge we have encountered is scalability. Currently we have made Zen scalable to thousands of lines of driver code (written in C), and found several serious race conditions in some Windows device drivers, such as kbfilter and fakemodem drivers.
(Joint work with Shaz Qadeer, Microsoft Research)
MSR 3.0: the Logical Meeting Point of Multiset Rewriting and Process Algebra
Multiset rewriting, as embodied in MSR versions 1 and 2, and in the operation of numerous tools for security protocol verification (e.g. CIS/CAPL and the NRL protocol analyzer), is based on local transitions between explicit states. This paradigm has a simple interpretation in terms of both Petri nets and linear logic.
Languages derived from process algebras (e.g. the spi-calculus) and strand spaces are instead based on self-transforming processes, with little emphasis on a notion of state. The translations between languages in these two families (e.g. between MSR and strand spaces, or between MSR and the spi-calculus) have proved cumbersome and somewhat ad-hoc.
MSR 3 is a conservative extension of MSR 1 and 2 that pushes to new heights the links between multiset rewriting and linear logic. This also allows immediate translations to and from process algebraic languages. The tension between state-transition and process-transformation witnessed earlier is internally resolved on logical grounds through a technique reminiscent of Skolemization. This transformation itself is interesting as it allows reasoning on certain aspects of denial-of-service.
Abstraction, Specification and Enforcement of Security Policies for Decentralized Systems'
Security requirements for a system may be represented symbolically as a policy specification. This enables mechanical translation of the policy into a set of enforcement actions, eliminating many steps at which human error can creep in. As the 'semantic gap' between high-level (and global) policies and low-level (and highly localized) enforcement actions seems particularly large, we believe that a good choice of abstraction coupled to a set of translation tools can have significant operational impact on system security. This impact is particularly strong for complex systems such as those constructed from decentralized components.
Our approach is a policy enforcement programming language (PEPL) allowing general purpose programming of policies at a high level of abstraction, or perhaps more interestingly, the use of abstract PEPL objects to erect domain-specific policy specification infrastructures.
In this talk I will give an overview of our proposed security architecture. I will describe the policy language, that enables high-level security policy specification, the adaptation layer supporting the policy-to-enforcement mapping, and the runtime support for policy coordination in a decentralized computing environment.
A Survey of Programming Languages and Systems for Computer Music
The domain of digital audio programming presents unique and interesting challenges to the programmer and thus to the computer music programming language designer. Managing the flow of time, supporting parallelism, accurately representing sound/musical concepts, and (often) providing real-time control are among the key issue that must be addressed.
In this talk, we will (1) identify the motivations and challenges of programming languages for computer music synthesis, composition, and performance, and (2) examine and assess existing computer music programming languages. We begin with an overview of digital audio synthesis and audio programming concepts. We then examine and "listen to" several computer music programming languages and systems that have been influential in the evolution of computer music. For each language or system, we look at its approach in meeting the challenges of audio programming (in a practical way: by showing and running demo programs) and evaluate its design in terms of expressive power, representation of audio/musical concepts, and efficiency.
This presentation is aimed to provide insight into the domain of audio programming and programming languages for computer music. All are welcome!
Construction of a Semantic Model for a Typed Assembly Language
Typed Assembly Languages (TALs) can be used to validate the safety of assembly-language programs. However, typing rules are usually trusted as axioms. In this paper, we show how to build semantic models for typing judgments in TALs based on an induction technique, so that both the type-safety theorem and the typing rules can be proved as lemmas in a simple logic. We demonstrate this technique by giving a complete model to a sample TAL. This model allows a typing derivation to be interpreted as a machine-checkable safety proof at the machine level.
This is a joint work with Andrew Appel, Kedar Swadi and Dinghao Wu.
Stacks, Heaps and Regions: One Logic to Bind Them
Systems of proof-carrying code and typed assembly language guarantee a variety of important safety properties for low-level programs. However, implementers often spend the most time and effort creating mechanisms related to checking aliasing properties, data layout and memory management. One of the main causes of this phenomenon is simply the sheer number and complexity of different memory invariants aliasing relationships that are possible in a certifying compiler. In the face of this complexity, ad hoc techniques for ensuring memory safety will break down.
A promising new way to manage the complexity of memory management invariants in safe low-level systems is to use substructural logics. The expressive connectives of some substructural logics are able to capture the spatial orientation of a data structure in a concise fashion without having to rely upon the ad hoc auxiliary predicates needed by conventional logics. In this talk, we will explain how to develop a substructural logic with connectives capable of expressing a variety of spatial properties of data including:
- Juxtaposition of one piece of storage next to another
- Separation (disjointedness) of one piece of storage with respect to another
- Containment of one piece of storage within another
Great care has been taken to define each connective in our logic orthogonally to the others, so a particular proof-carrying code system can employ the exact fragment of logic that suits its needs. The connectives also compose nicely and allow us to express rich invariants involving data structures allocated on the stack, in the heap, or in user-managed memory regions. We have defined the syntactic proof rules for our logic, given a storage semantics to the connectives, and defined a typed assembly language that uses the logic to ensure safe stack, heap and region allocation and deallocation of data.
This is joint research with Amal Ahmed and Limin Jia.