软件漏洞分析技术:定理证明
软件漏洞分析技术第8章定理证明读书笔记。
- 定理证明
- 基本原理
- 技术框架
- 特点
- 方法实现
- 程序转换
- 属性描述
- 定理证明
- 实例分析
- 典型工具
- Saturn
- ESC/Java
基本原理
定理证明的基本步骤:
- 用逻辑的方法将系统规范的功能和性质形式化为逻辑形式的模型
- 将系统设计实现也形式化为逻辑形式的模型
- 用数学定理进行推导证明实现的模型等价于或者蕴含规范的模型
定理证明的优点:
- 误报率很低
- 可以处理无限状态空间问题
- 只要程序表达为规范形式,就可以进行推理验证安全属性
定理证明的缺点:
- 需要程序员输入额外注释
- 交互式定理证明系统需要与用户交互
- 形式化程序转化为定理表达式存在困难,并且证明推理过程过于抽象,缺乏运行过程信息
- 漏洞产生过程的能力较差
典型工具
Saturn:该工具的实现主要基于函数abstract,同时基于条件约束进行分析。
ESC/Java:该工具用来检测 Java 漏洞。
All articles in this blog are licensed under CC BY-NC-SA 4.0 unless stating additionally.