基于机器语言的移动代码安全研究

摘要

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

目录

文摘

英文文摘

第1章绪言

1.1安全策略

1.2信任关系

1.3传统方法

1.3.1 身份认证

1.3.2 内核监督

1.3.3 代码检测

1.3.4 基于硬件的地址空间

1.3.5 加解密方法

1.4基于语言的安全

1.4.1 Java

1.4.2 Proof-Carrying Code

1.4.3 Typed Assemble Language

1.5主机资源的安全

1.5.1Janus

1.5.2 Generic Software Wrapper

1.6论文的纽织

1.7本文的创新和贡献

参考文献

第2章代码检查的体系结构

2.1安全检查

2.2三层体系结构

2.3低级代码安全策略

2.3.1 安全策略

2.3.2 携带注解的代码和提示

2.3.3 接收方的代码验证

2.4中级代码安全策略

2.4.1 策略描述语言

2.4.2 一个例子

2.4.3 策略的实现过程

2.5高级代码安全策略

2.5.1 系统组成

2.5.2 策略描述语言

2.5.3 API的替换策略

2.6 小结

参考文献

第3章认证编译器的设计与实现

3.1概述

3.2认证编译器的结构

3.3 MINI-C

3.4安全策略系统中的类型

3.4.1 C语言安全子集中的类型

3.4.2安全策略系统中的类型抽象

3.4.3类型和变量声明的转换函数

3.5注解自动生成

3.5.1 扩展的CFG(ECFG)

3.5.2 变量的类型注解

3.5.3 函数前后条件

3.5.4 循环不变式

3.5.5 一个含注解代码的例子

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

3.6.1 PCC内存安全检查

3.6.2 数组边界检查

3.6.3 数组边界检查的例子

3.7 小结

参考文献

第4章 机器语言的类型化及代码的安全检查

4.1 引言

4.2类型系统

4.2.1 类型化语言和非类型化语言

4.2.2 执行错误和安全语言

4.2.3 描述类型系统的语言

4.3 TML0语言

4.4 TML0指令操作语义

4.5 TML0定型规则

4.5.1 等价类型与子类型

4.5.2 指令的定型规则

4.6原型系统

4.6.1 原型系统的组成

4.6.2 符号变量

4.6.3 前端处理

4.6.4 类型检查算法

4.6.5 一个例子

4.7符号值范围的静态分析

4.7.1 符号表达式比较

4.7.2 值范围简化

4.7.3 值范围替换次序

4.7.4 值范围传播

4.7.5 时间复杂度分析

4.8小结

参考文献

第5章主机系统资源的安全策略

5.1 引言

5.2资源和策略描述

5.3策略支持库

5.4策略执行库

5.5 小结

参考文献

第6章总结和进一步工作

6.1本文工作的总结

6.2进一步工作

致谢

读博期间发表的论文

作者简历