基于类型注解的认证编译器设计与实现

基于类型注解的认证编译器是安全策略系统的核心部件 ,它不仅能够用C语言的类型安全子集编写的程序编译成优化的Intelx86 /linux汇编语言程序 ,而且还可以根据类型安全策略的要求产生带注解的汇编程序 实验结果表明 ,新设计的认证编译器可实现 :①类型安全的C语言子集的编译 ;②许多标准的局部优化 ;③可以对数组运行时越界操作进行检查 由于安全策略系统的证明是建立在含注解的代码基础之上的 ,因此 。

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

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