Analyzing Security Advice in Functional Aspect-oriented Programming Languages (thesis)
Abstract:
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 run-time 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.