GCC编译器安全验证方法研究
| 摘要 | 第1-5页 |
| Abstract | 第5-10页 |
| 第1章 绪论 | 第10-17页 |
| ·研究背景 | 第10-15页 |
| ·可信软件与软件验证 | 第11-12页 |
| ·静态分析与形式化方法 | 第12-13页 |
| ·动态分析与软件测试 | 第13-15页 |
| ·研究内容 | 第15页 |
| ·研究目标 | 第15页 |
| ·本文结构组织 | 第15-16页 |
| ·本章小结 | 第16-17页 |
| 第2章 编译器验证研究综述 | 第17-22页 |
| ·编译器安全验证 | 第17-19页 |
| ·编译优化验证 | 第19页 |
| ·编译结果运行时保证 | 第19-21页 |
| ·本章小结 | 第21-22页 |
| 第3章 编译器代码分析及保障对比验证 | 第22-37页 |
| ·引言 | 第22页 |
| ·总体方案描述 | 第22-28页 |
| ·基本思路 | 第23-24页 |
| ·实施步骤 | 第24-26页 |
| ·参与人员角色与约束 | 第26-27页 |
| ·其他注意事项 | 第27-28页 |
| ·实施实例 | 第28-34页 |
| ·循环代码外提优化的安全性验证 | 第28-34页 |
| ·工作量估计 | 第34-36页 |
| ·本章小结 | 第36-37页 |
| 第4章 控制流逻辑结构对比验证 | 第37-65页 |
| ·引言 | 第37-38页 |
| ·控制流图 | 第38-42页 |
| ·控制流图结构 | 第38-41页 |
| ·同构图问题 | 第41-42页 |
| ·C语言源代码控制流图生产 | 第42-51页 |
| ·Lex& Yacc | 第43-44页 |
| ·条件判断语句 | 第44-46页 |
| ·循环语句 | 第46-50页 |
| ·函数调用 | 第50-51页 |
| ·目标码控制流图生产 | 第51-54页 |
| ·控制流图简化与图同构 | 第54-57页 |
| ·控制流图简化 | 第54-55页 |
| ·控制流图同构 | 第55-57页 |
| ·实验评估测试 | 第57-64页 |
| ·控制流图实验用例 | 第57-60页 |
| ·恶意代码嵌入 | 第60页 |
| ·恶意代码嵌入实验 | 第60-63页 |
| ·真实程序测试用例 | 第63-64页 |
| ·本章小结 | 第64-65页 |
| 第5章 总结与展望 | 第65-67页 |
| ·本文完成的主要研究工作 | 第65页 |
| ·本文的主要贡献以及创新点 | 第65-66页 |
| ·进一步的研究工作 | 第66-67页 |
| 附录 | 第67-81页 |
| C语言词法规则 | 第67-71页 |
| C语言语法规则 | 第71-81页 |
| 参考文献 | 第81-86页 |
| 致谢 | 第86页 |
