
Daniel Dantas will present his preFPO at 10AM on Tuesday, February 6 in Room 402. The members of his committee are David Walker, advisor; Andrew Appel, Stephanie Weirich, readers; Ed Felten, and David August, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ------------------------------ My thesis extends functional programming languages with aspect-oriented features, primarily to explore aspect-oriented enforcement of security policies. First, my thesis examines an aspect-oriented implementation of the Java security mechanism, which requires the security advice to be triggered by functions with diverse argument and return types. My thesis presents a new language, AspectML, that allows a programmer to define 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, my 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 implemented many of the security examples used by the Naccio execution monitoring system by Evans and Twyman as harmless advice. Finally, my thesis expands the harmless advice specification to allow programmers to create interference policies for system libraries to define how those libraries can be used by aspects. These policies use a selection of compile-time type checking and run-time monitoring to enforce the desired definition of harmlessness on the aspect-oriented program. My thesis formalizes an idealized file IO system 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 IO.