一种Java字节码中内联引用验证的代码携带框架
A Proof Carrying Code Framework for Inlined Reference Monitors in Java Bytecode
摘要：
我们提出了一个轻量级的方法来证明监视器内联顺序Java字节码使用证明携带代码。其目标是在开发时使用质量保证监控，同时最大限度地减少交付后代码重写以及对终端主机TCB的更改的需要。标准的基于自动机的安全策略表达了对允许的API调用/返回序列的约束。证明被表示为XML风格的程序注释。这在我们的情况下是足够的，因为在我们的框架中生成的所有证明都是在程序大小的时间多项式中识别的。通过将内联监视器的转换与使用XML样式的注释表示的可信“幽灵”监视器的转换进行比较，可以证明策略遵守。在接收到具有证明注释的程序时，接收器插件插入其自己的可信幽灵监视器并检查所得到的验证条件，以验证正确策略的内联已被正确执行就足够了。我们已经在Java字节码级别证明了该方法的正确性，并在Coq中形式化了可靠性证明。一个实现，包括一个应用程序加载器上运行的移动终端，是可用的，我们的结论是两个示例应用程序的基准。
英文摘要：
We propose a light-weight approach for certification of monitor inlining for sequential Java bytecode using proof-carrying code. The goal is to enable the use of monitoring for quality assurance at development time, while minimizing the need for post-shipping code rewrites as well as changes to the end-host TCB. Standard automaton-based security policies express constraints on allowed API call/return sequences. Proofs are represented as JML-style program annotations. This is adequate in our case as all proofs generated in our framework are recognized in time polynomial in the size of the program. Policy adherence is proved by comparing the transitions of an inlined monitor with those of a trusted "ghost" monitor represented using JML-style annotations. At time of receiving a program with proof annotations, it is sufficient for the receiver to plug in its own trusted ghost monitor and check the resulting verification conditions, to verify that inlining has been performed correctly, of the correct policy. We have proved correctness of the approach at the Java bytecode level and formalized the proof of soundness in Coq. An implementation, including an application loader running on a mobile device, is available, and we conclude by giving benchmarks for two sample applications.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
