[talks] D Dantas preFPO

[Melissa M Lawson]

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.