Runtime monitoring for mobile code security

Group


Ville Leppänen
Home page
email
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.

Publications (not a complete list)