认证编译器是实现三层体系结构中基于逻辑证明的低级代码安全策略的基石.该文设计和实现的认证编译器是安全策略体系中代码发送方的核心组件,它完成了编程语言 C—种子集(Mini—C)到汇编语言(Intel x86/Linux)转换的编译过程,同时还生成了低级代码安全策略证明系统中所需的注解信息.三层体系结构中的高级代码安全策略是用于保护主机系统资源的.我们描述了一种通过限制程序行为的方案来保护主机系统资源,该方案是由平台无关的策略描述语言和执行这些策略的组件构成.策略描述语言定义的安全策略经策略编译器编译生成策略支持库,采用库插入技术生成了原系统共享库的包装(即策略执行库).在策略支持库和策略执行库的支撑下,通过对动态连接器进行重新定向,使应用程序中的所有对共享库的函数调用被截获,并对其进行给定的安全策略验证.通过对文件系统和存储访问函数调用的截获测试表明,系统设计变得相当简单,而且还可以获得较高的性能.基于逻辑证明的低级安全策略对源语言具有很强的依赖性,并且对编译器的正确性也有一定的要求,因此该文从另外一种角度对代码的基本安全属性进行静态分析(这种方法实际上也是一种低级代码安全策略).