TACL Seminar Fall '05
|Sep 22||Daniel S Dantas]||PolyAML: A Polymorphic Aspect-oriented Functional Programmming Language||Abstract|
|Oct 6||Frances Spalding||SpacerX: Detecting Deadlocks Using Sequential Analysis||Abstract|
|Oct 13||David Walker]||PADS/ML|
|Oct 27||Jay Ligatti||Policy Enforcement via Program Monitoring||Abstract|
|Nov 3||Guilherme Ottoni||Automatic Thread Extraction with Decoupled Software Pipelining||Abstract|
|Nov 15||Anupam Datta - Stanford||Security Analysis of Network Protocols|
|Nov 22||Matthew Bridges||Predicate Instruction Fusion||Abstract|
|Dec 15||Yitzhak Mandelbaum||The Next 700 Data Description Languages||Abstract|
Daniel S Dantas
This talk defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, PolyAML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. PolyAML also comes equipped with a type inference algorithm that conservatively extends Hindley-Milner type inference. To support first-class polymorphic point-cut designators, a crucial feature for developing aspect-oriented profiling or logging libraries, the algorithm blends the conventional Hindley-Milner type inference algorithm with a simple form of local type inference.
We give our language operational meaning via a type-directed translation into an expressive type-safe intermediate language. Many complexities of the source language are eliminated in this translation, leading to a modular specification of its semantics. One of the novelties of the intermediate language is the definition of polymorphic labels for marking control-flow points. These labels are organized in a tree structure such that a parent in the tree serves as a representative for all of its children. Type safety requires that the type of each child is less polymorphic than its parent type. Similarly, when a set of labels is assembled as a pointcut, the type of each label is an instance of the type of the pointcut.
This is work I did this summer as an intern at Microsoft in the Program Analysis Group.
Deadlocks are a very common problem in concurrent code and are notoriously hard to debug. SpacerX is a prototype tool that detects potential deadlocks using sequential analysis.
This is accomplished in two phases. In phase one, we compute the sequence of locks held at each program point using a dataflow analysis. This analysis is built to leverage existing tools from the Program Ananlysis Group, such as a value alias analysis, a path feasibility simulator, and a graphical interface for viewing traces through the code. In phase two, we compute the ordering constraints between locks and look for cycles in these ordering constraints.
After running SpacerX on a very small subset of the Windows code base, we have already found three confirmed deadlocks. These deadlocks could not have been found by hand (the reasoning is too complicated), by model checking (the code involved is too large), or by testing (one deadlock only occurs under specific conditions at precisely midnight).
Program monitors intercept security-relevant actions of a target application at run time and take remedial steps whenever the target attempts to execute a potentially dangerous action. Although it is well known that monitors with simple remedial options can enforce only safety properties, we will describe more sophisticated monitors that can enforce any of what we call the 'infinite renewal' properties. We will compare the set of infinite renewal properties with the standard sets of safety and liveness properties and find that infinite renewal properties include all safety properties, some liveness properties, and some properties that are neither safety nor liveness.
In practice, the security policies enforced by program monitors grow more complex both as the monitored software is given new capabilities and as policies are refined in response to attacks and user feedback. We propose dealing with policy complexity by organizing policies so that they are composeable. Security architects can then specify complex policies more simply as compositions of smaller 'subpolicies'. We will describe a language and system called Polymer that implements and supports composeable policies for Java applications.
This is joint work with Lujo Bauer (Carnegie Mellon University) and David Walker (Princeton University).