Lecture Notes in Computer Science vol:5051/2008 pages:240-258
Formal Methods for Open Object-based Distributed Systems edition:10 location:Oslo, Norway date:4-6 June 2008
Runtime security policy enforcement systems are crucial to limit the risks associated with running untrustworthy (malicious or buggy) code. The inlined reference monitor approach to policy enforcement, pioneered by Erlingsson and Schneider, implements runtime enforcement through program rewriting: security checks are inserted inside untrusted programs.
Ensuring complete mediation – the guarantee that every security-relevant event is actually intercepted by the monitor – is non-trivial when the program rewriter operates on an object-oriented intermediate language with state-of-the-art features such as virtual methods and delegates.
This paper proposes a caller-side rewriting algorithm for MSIL – the bytecode of the .NET virtual machine – where security checks are inserted around calls to security-relevant methods. We prove that this algorithm achieves sound and complete mediation and transparency for a simplified model of MSIL, and we report on our experiences with the implementation of the algorithm for full MSIL.
The original publication is available at http://www.springerlink.com/content/8l30r27122322k11/