Certified In-lined Reference Monitoring on .Net
MOBILE is an extension of the .NET Common Intermediate Language that permits certified In-Lined Reference Monitoring on Microsoft .NET architectures. MOBILE programs have the useful property that if they are well-typed with respect to a declared security policy, then they are guaranteed not to violate that security policy when executed. Thus, when an In-Lined Reference Monitor (IRM) is expressed in MOBILE, it can be certified by a simple type-checker to eliminate the need to trust the producer of the IRM. MOBILE thereby permits development of arbitrarily complex IRM producers without contributing that added complexity to the trusted computing base of the system. Security policies in MOBILE are declarative, can involve potentially unbounded collections of objects allocated at runtime, and can regard finite- or infinite-length histories of security events exhibited by those objects. Our prototype implementation of MOBILE enforces properties expressed by finite-state security automata -- one automaton for each security-relevant object, and can type-check MOBILE programs in the presence of exceptions, finalizers, concurrency, and non-termination. Executing MOBILE programs requires no change to existing .NET virtual machine implementations, since MOBILE programs consist of normal managed CIL code with extra typing annotations stored in .NET attributes.