Certified In-lined Reference Monitoring on .NET
Certified In-lined Reference Monitoring on .NET
复制标题
.NET 上经过认证的内联参考监控
DOI：
10.1145/1134744.1134748
复制
发表时间：
2006
期刊：
影响因子：
--
通讯作者：
F. Schneider
中科院分区：
文献类型：
--
作者：
Kevin W. Hamlen;J. G. Morrisett;F. Schneider
MOBILE 是 .NET 通用中间语言的扩展，支持经过认证的内联引用监控。移动程序具有一个有用的属性，即如果它们的类型符合声明的安全策略，则可以保证它们在执行时不会违反该安全策略。因此，当内联引用监视器 (IRM) 在 Mobile 中表达时，可以通过简单的类型检查器对其进行认证，从而无需信任 IRM 的生成者。 Mobile 中的安全策略是声明性的，可以涉及在运行时分配的无界对象集合，并且可以考虑这些对象所展示的安全事件的无限长历史。原型 Mobile 实现强制执行由有限状态安全自动机（每个安全相关对象一个自动机）表示的属性，并且可以在存在异常、终结器、并发和非终止的情况下对 Mobile 程序进行类型检查。执行 Mobile 程序不需要更改现有的 .NET 虚拟机实现，因为 Mobile 程序由普通的托管 CIL 代码以及存储在 .NET 属性中的额外类型注释组成。
MOBILE is an extension of the .NET Common Intermediate Language that supports certified In-Lined Reference Monitoring. 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.Security policies in Mobile are declarative, can involve unbounded collections of objects allocated at runtime, and can regard infinite-length histories of security events exhibited by those objects. The prototype Mobile implementation 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.