可信编译构造理论与关键技术PDF电子书下载

第1章 绪论 1

1.1 研究背景及意义 1

1.2 相关研究现状 2

1.2.1 编译器自身的安全性问题研究 3

1.2.2 编译所生成程序代码的安全性问题研究 3

1.2.3 安全程序设计语言及其相应编译系统构造方法研究 5

1.3 目标及内容 7

1.3.1 编译器自身的可信性研究 8

1.3.2 编译所得可执行代码的可信性研究 9

1.4 本书组织结构 11

1.5 本章小结 12

参考文献 13

第2章 编译器自身可信性 15

2.1 引言 15

2.2 可信编译概念 16

2.3 编译正确性证明 17

2.3.1 编译器正确性 18

2.3.2 形式语义与语义保持 21

2.3.3 保证编译器自身可信性方法 22

2.4 可信编译器构造 26

2.4.1 基于编译器正确性的构造方法 27

2.4.2 基于携带证明代码的构造方法 29

2.4.3 基于转换检验的构造方法 31

2.4.4 基于可证明微型编译器的构造方法 33

2.4.5 可信编译器构造方法对比分析 38

2.5 基于形式语义的编译器正确性证明 39

2.5.1 源语言 39

2.5.2 目标语言 42

2.5.3 编译转换及正确性证明 43

2.6 编译优化正确性证明 49

2.6.1 中间语言语法和迁移系统 50

2.6.2 模拟关系及语义一致性验证 52

2.6.3 编译优化实现正确性验证过程 52

2.6.4 应用示例 55

2.6.5 结论 56

2.7 本章小结 57

参考文献 57

第3章 编译对象的可信性 63

3.1 引言 63

3.2 代码可信性验证机制 63

3.2.1 基于分离逻辑的程序验证 64

3.2.2 基于模型检测的程序验证方法 67

3.3 代码安全性加强机制 80

3.3.1 基于有色Petri网的缓冲区溢出检测 80

3.3.2 基于SMT求解器的程序验证方法 86

3.4 可执行代码安全保护机制 93

3.4.1 基于压缩的低开销代码保护策略 93

3.4.2 基于程序流敏感的自修改代码混淆方法 101

3.4.3 程序动态完整性保护 109

3.5 本章小结 118

参考文献 119

第4章 基于编译嵌入式软件优化 121

4.1 引言 121

4.2 基于编译的优化框架 122

4.2.1 基于编译的嵌入式系统优化框架结构设计 122

4.2.2 面向嵌入式平台编译优化的中间语言设计 123

4.2.3 目标机器特征描述语言研究 124

4.3 传统的编译器优化技术概述 124

4.3.1 机器无关的编译器优化技术 124

4.3.2 机器相关的编译器优化技术 128

4.4 内存优化 128

4.4.1 背景 129

4.4.2 分析 131

4.4.3 方法 132

4.4.4 一个例子 136

4.4.5 实验结果 136

4.5 功耗优化 138

4.5.1 功耗模型 139

4.5.2 基于编译的功耗优化方法 141

4.5.3 基于总线的功耗优化实例 143

4.5.4 基于片上缓存的功耗优化 154

4.6 本章小结 165

参考文献 166

第5章 绿色编译优化 168

5.1 引言 168

5.2 绿色编译器概念及优化框架 169

5.2.1 绿色编译器的概念 169

5.2.2 绿色编译优化框架 170

5.3 面向移动嵌入式系统的绿色编译优化方法研究 172

5.3.1 基于计算博弈论的混合存储系统绿色编译优化 174

5.3.2 基于总线翻转编码和多维度集成学习的指令选择和调度方法研究 176

5.3.3 基于编译的多核环境下的并行程序绿色优化 177

5.4 绿色评估模型 181

5.5 本章小结 183

参考文献 183

第6章 基于编译的软件测试 185

6.1 引言 185

6.2 基于编译的测试框架 186

6.3 测试需求描述语言 188

6.4 基于编译的错误可跟踪的自动测试方法 190

6.4.1 用于测试用例生成的扩展语法及对应语义 192

6.4.2 应用举例 194

6.5 本章小结 197

参考文献 197

第7章 基于编译的可信软件构造及关键技术 200

7.1 引言 200

7.2 基于编译的可信软件开发过程模型 201

7.2.1 可信软件开发过程模型 201

7.2.2 可信软件开发过程可信保障机制 202

7.3 可信软件需求建模与验证 205

7.3.1 基于软件行为的需求建模方法 205

7.3.2 面向可信软件需求模型的验证方法 206

7.4 可信软件的设计与实现 208

7.4.1 可信软件体系结构设计 208

7.4.2 体系结构驱动的构件化可信软件组装 210

7.4.3 基于可信编译的代码生成与分析 212

7.5 可信软件的测试与评估 220

7.5.1 可信软件的测试 220

7.5.2 可信软件的评估 221

7.6 本章小结 222

参考文献 223

第8章 总结及展望 226

8.1 总结 226

8.2 展望 227