Runtime monitoring for mobile code security
Group
 Ville Leppänen Home page | MSc student Jari-Matti Mäkelä Home page | (Tuohimaa) PhD student Sanna Mäkelä |
Sami Mäkelä | Tomi Karlsted | Lauri Taimila |
Mikael Laine |
Overview
There exists three kinds of approaches for mobile code security: (a) providing a proof of security properties along with the code, (b) establishing an authority for certifying the safety of mobile code, (c) running mobile code under some runtime monitoring system in the target platform. We follow approach (c) and have developed a rule-based language (Modular Policy Language, MPL) for expressing runtime monitors and a compiler for translating descriptions to AspectJ based monitors. We use a weaver to weave the aspects into the mobile code to guarantee its safe runtime execution. If the runtime behavior of the code attempts to violate the applied security policy, the application is halted. We aim at simple and compact policy descriptions. We also focus on representing the meaning of a policy description by an invariant over the saved attribute values, and how such invariants and the rule descriptions can be used to prove that the rules preserve the invariant condition.
Goals
We develop tools and software analysis methods for ensuring secure execution of mobile code. Future emphasis will be in MPL development, especially attaching invariants to MPL monitor descriptions and developing a method to prove that descriptions preserve their invariant. The scope of applicability of MPL descriptions also needs to be studied. We also plan to develop MPL compilers for other languages besides Java.
Outcomes
Compiler for the MPL language
A compiler exists for AspectJ and there is also a preliminary version for Aspect++. See also the examples.