PCC中数组边界检查的优化和生成

Optimization and Creation for Array Bound Check in Proof Carrying Code

PCC的数组边界检查存在着由于无法确定数组下标表达式符号值的范围 ,而造成拒绝执行一些安全的移动代码等问题 .本文给出的一种数组边界检查的优化及生成算法 ,不仅能够比较好地解决了这一问题 ,同时还生成了循环不变式注解中的条件谓词 .我们设计的编译器———认证编译器———已经实现了这些算法 ,并完成了从用C编程语言的类型安全子集编写的源程序到携带注解的Intelx86 /linux汇编语言程序的编译过程 .由于基于语言安全策略系统的证明是建立在携带注解的代码基础之上的 ,因此该认证编译器中实现的算法在移动代码安全检查中非常有用 .

Some of the safe mobile codes may be rejected to execute, since there is no way to verify statically that the symbol range value of an array subscript expression in PCC. Compiler optimization and creation algorithms for array bound checks we disigned can not only overcome the above problem, but also form conditional predicates of the loop-invariant annotation. We have implemented a certifying compiler that translates programs written in a type safe subset of the C programming language into highly annotated Intel x86/linux assembly language programs. Since the language-based proof system of the safety policy is founded on the annotated target code, algorithms implemented in the certifying compiler thus may be useful in a system for safe mobile code.