Using high-level security policies to transform unsafe programs into safe programs

Andrew Brown and Mark Ryan
School of Computer Science
University of Birmingham

Users often execute programs that they do not trust: such programs offer 
useful functions but can also contain malicious behaviour. The user must 
decide to trust the program and risk it causing damage to their system, 
or not to trust it and to use some additional technology to attest it, 
or to harness its execution. Digitally signed code, proof-carrying code 
and firewalls can prevent program execution from causing damage, but have 
deficiencies themselves. Digitally signed code, for example, may enhance 
user confidence that an executable has not been altered, but still requires 
the user to trust the code signee.

Program transformation can assist the problem of running untrusted code; 
it allows the user to transform it into safe code that complies with a 
security policy. Our work builds on Polymer: a system for policy enforcement 
through the transformation of Java programs. A policy specifies action 
sequences that should not be invoked by a program, before detailing the 
actions (and their parameters) that should be inserted into the program 
when a policy violation is detected.

If program transformation is to be used to prevent malware, the techniques 
it offers must be operable by the end-user (constructing an effective policy 
that is guaranteed to meet a set of security-critical requirements is difficult 
for any non-programmer). Our work aims to develop an end-user operable anti-malware 
system with a high-level policy specification language (which may be driven 
by a user interface) and a compiler into Polymer.

In this talk we consider examples of malicious applications and demonstrate their 
transformation into variants that comply with a security policy. Current logics 
that policy specification uses are too weak to represent some properties of the 
programs that we may wish to monitor. We discuss the theoretical foundations that 
our work builds upon and detail our investigations into suitably expressive logics 
for policy specification. We conclude by stating our ideas about the format of 
a high-level language to achieve end-user policy specification at the highest 
feasible level.