Inline reference monitoring is a powerful technique to enforce security policies on untrusted programs. The security-by-contract paradigm proposed by the EU FP6 S3MS project uses policies, monitoring, and monitor inlining to secure third-party applications running on mobile devices. The focus of this paper is on multi-threaded Java bytecode. An important consideration is that inlining should interfere with the client program only when mandated by the security policy. In a multi-threaded setting, however, this requirement turns out to be problematic. Generally, inliners use locks to control access to shared resources such as an embedded monitor state. This will interfere with application program non-determinism due to Java's relaxed memory consistency model, and rule out the transparency property, that all policy-adherent behaviour of an application program is preserved under inlining. In its place we propose a notion of strong conservativity, to formalise the property that the inliner can terminate the client program only when the policy is about to be violated. An example inlining algorithm is given and proved to be strongly conservative. Finally, benchmarks are given for four example applications studied in the S3MS project.
展开▼
机译:内联引用监视是在不受信任的程序上实施安全策略的强大技术。 EU FP6 S3MS项目提出的“按合同安全”范式使用策略,监视和监视内联来保护在移动设备上运行的第三方应用程序的安全。本文的重点是多线程Java字节码。一个重要的考虑因素是,仅当安全策略要求内联时,内联才应干扰客户端程序。但是,在多线程设置中,此要求却是有问题的。通常,内联器使用锁来控制对共享资源(例如嵌入式监视器状态)的访问。由于Java宽松的内存一致性模型,这将干扰应用程序的不确定性,并排除了透明性,即应用程序的所有策略依从行为都在内联下保留。取而代之的是,我们提出了一种强保守性的概念,以使属性正式化,即只有在即将违反该策略时,内联程序才能终止客户端程序。给出了一个示例内联算法,并证明该算法非常保守。最后,给出了在S3MS项目中研究的四个示例应用程序的基准。
展开▼