Security Monitor Inlining in the ABS Modelling Language

M.Sc. Thesis project (Ex-jobb) proposal

Background

One way to enforce a certain behavior of a program, is to rewrite it so that it monitors its own actions and suppresses the actions that would lead to a violation of the intended behavior. The technique is called inlined reference monitoring, and has been successfully applied to Java applications on the level of Java bytecode.

Recently a modelling language called ABS has been developed within the HATS (Highly Adaptable and Trustworthy Software) research project. There is now a need formalize and implement the security monitor inlining process in this modelling language.

Objective

In the project you will read up on the ABS modelling language and the existing inlining techniques in order to implement the technique in ABS. The tasks of the project include but are not limited to
  1. Develop a policy format suitable for ABS monitor inlining.
  2. Implement a compiler for the policy format.
  3. Implement a dynamic code weaver for the ABS language.
  4. Try out the framework on some example cases.
  5. Write a scientific report on the project.

During the project you will be exposed to scientific research in the field of compilers and programming language theory.

Required Competence

Interest in formal methods and theoretical computer science.

Further reading

HATS: http://www.cse.chalmers.se/research/hats/
ABS: http://www.cse.chalmers.se/research/hats/sites/default/files/Deliverable11a_rev2.pdf

Contact

If interested in this project, please contact

Mads Dam: mfd@kth.se / www.csc.kth.se/~mfd, or
Andreas Lundblad: landreas@kth.se / www.csc.kth.se/~landreas



Andreas Lundblad 2010-06-17