Principles and Practice of Declarative Programming

Published Language Support for Processing Distributed Ad Hoc Data with Kenny Zhu, Kathleen Fisher, Limin Jia, Yitzhak Mandelbaum, Vivek Pai & David Walker at ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming

This paper presents the design, theory and implementation of GLOVES, a domain-specific language that allows users to specify the provenance (the derivation history starting from the origins), syntax and semantic properties of collections of distributed data sources. In particular, GLOVES specifications indicate where to locate desired data, how to obtain it, when to get it or to give up trying, and what format it will be in on arrival. The GLOVES system compiles such specification into a suite of data-processing tools including an archiver, a provenance tracking system, a database loading tool, an alert system, an RSS feed generator and a debugging tool. In addition, the system generates description-specific libraries so that developers can create their own applications.

In re Katz Interactive Call Processing Patent Litigation

General Electric Company and Ronald A. Katz Technology Licensing, L.P. Settle Patent Lawsuit and Enter into License Agreement

General Electric Company (GE), a diversified technology, media and financial services company (NYSE:GE), and Ronald A. Katz Technology Licensing, L.P., announced today the settlement of patent litigation between the parties. As part of the settlement, GE has agreed to pay an undisclosed sum for a nonexclusive license under a comprehensive portfolio of patents that Katz owns relating to interactive voice applications.

Transactions on Programming Languages & Systems

Published AspectML: A Polymorphic Aspect-oriented Functional Programming Language with David Walker, Geoffrey Washburn & Stephanie Weirich at ACM Transactions on Programming Languages & Systems

This paper defines AspectML, a typed functional, aspect-oriented programming language. The main contribution of AspectML is the seamless integration of polymorphism, run-time type analysis and aspect-oriented programming language features. In particular, AspectML allows programmers to define type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points.

Additional Resources: Language Interpreter Security Case Study

Formal Methods in Security Engineering

Published A Simple and Expressive Semantic Framework for Policy Composition in Access Control with Glenn Bruns & Michael Huth at the ACM workshop on Formal Methods in Security Engineering: From Specifications to Code

In defining large, complex access control policies, one would like to compose sub-policies, perhaps authored by different organizations, into a single global policy. Existing policy composition approaches tend to be ad-hoc, and do not explain whether too many or too few policy combinators have been defined. We define an access control policy as a four-valued predicate that maps accesses to either grant, deny, conflict, or unspecified. These correspond to the four elements of the Belnap bilattice. Functions on this bilattice are then extended to policies to serve as policy combinators.

Princeton University Ph.D in Computer Science

Presented Ph.D Thesis Analyzing Security Advice in Functional Aspect-oriented Programming Languages to David Walker, Andrew Appel, Stephanie Weirich, Ed Felten & David August

This thesis extends functional programming languages with aspect-oriented features, primarily to explore aspect-oriented enforcement of security policies.
First, this thesis examines an aspect-oriented implementation of the Java security mechanism, which requires the security advice to be triggered by functions with diverse types. I present a new language, AspectML, that allows type-safe polymorphic advice using pointcuts constructed from a collection of polymorphic join points. I then compare my AspectML implementation of the Java security mechanism against the existing Java implementation.
Second, in ordinary aspect-oriented programming, security and other advice added after-the-fact to an existing codebase can disrupt important data invariants and prevent local reasoning. Instead, this thesis shows that many common aspects, including security advice, can be implemented as harmless advice. Harmless advice uses a novel type and effect system related to information-flow type systems to ensure that harmless advice cannot modify the behavior of mainline code. To demonstrate the usefulness of harmless advice for security, I implement many of the security examples used by the Naccio execution monitoring system as harmless advice.
Finally, this thesis expands the harmless advice specification to allow programmers to create interference policies to define how system libraries can be used by aspects. These policies use a combination of compile-time type checking and runtime monitoring to enforce the desired degree of harmlessness on the aspect-oriented program. My thesis formalizes an idealized file I/O library and proves that an interference policy specified by our policy language can continue to enforce our original view of harmlessness for advice that uses file I/O.

Principles of Programming Languages

Published Harmless Advice with David Walker at ACM symposium on Principles of Programming Languages

This paper defines an object-oriented language with harmless aspect-oriented advice. A piece of harmless advice is a computation that, like ordinary aspect-oriented advice, executes when control reaches a designated control-flow point. However, unlike ordinary advice, harmless advice is designed to obey a weak noninterference property. Harmless advice may change the termination behavior of computations and use I/O, but it does not otherwise influence the final result of the mainline code. The benefit of harmless advice is that it facilitates local reasoning about program behavior. More specifically, programmers may ignore harmless advice when reasoning about the partial correctness properties of their programs. In addition, programmers may add new pieces of harmless advice to pre-existing programs in typical “after-the-fact” aspect-oriented style without fear they will break important data invariants used by the mainline code.
The paper also presents an implementation of the language and a case study using harmless advice to implement security policies.

Additional Resources: Conference Slides Language Interpreter Security Case Study

International Conference on Functional Programming

Published PolyAML: A Polymorphic Aspect-oriented Functional Programmming Language with David Walker, Geoffrey Washburn & Stephanie Weirich at the ACM International Conference on Functional Programming

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

Additional Resources: Conference Slides Language Interpreter

Foundations of Object-Oriented Languages

Published Harmless Advice with David Walker at the ACM workshop on Foundations of Object-oriented Languages

This paper develops a simple object calculus with harmless aspect-oriented advice. A piece of harmless advice is a computation that, like ordinary aspect-oriented advice, executes when control reaches a designated control-flow point. However, unlike ordinary advice, harmless advice is designed to obey a weak non-interference property. Harmless advice may change the termination behavior of computations and use I/O, but it does not otherwise influence the final result of computations that trigger it. A simple type and effect system related to information-flow type systems helps enforce harmlessness. We have proven that harmless advice does not interfere with the mainline computation.

Additional resources: Workshop Presentation

Air Force NDSEG Fellow

Named a Air Force National Defense Science & Engineering Graduate (NDSEG) Fellow at Princeton University

The National Defense Science and Engineering Graduate (NDSEG) Fellowship is a highly competitive, portable fellowship that is awarded to U.S. citizens and nationals who intend to pursue a doctoral degree in one of fifteen supported disciplines. NDSEG confers high honors upon its recipients, and allows them to attend whichever U.S. institution they choose.