软件漏洞分析技术第8章定理证明读书笔记。

  • 定理证明
    • 基本原理
      • 技术框架
      • 特点
    • 方法实现
      • 程序转换
      • 属性描述
      • 定理证明
    • 实例分析
    • 典型工具
      • Saturn
      • ESC/Java

基本原理

定理证明的基本步骤：

  1. 用逻辑的方法将系统规范的功能和性质形式化为逻辑形式的模型
  2. 将系统设计实现也形式化为逻辑形式的模型
  3. 用数学定理进行推导证明实现的模型等价于或者蕴含规范的模型

定理证明的优点：

  1. 误报率很低
  2. 可以处理无限状态空间问题
  3. 只要程序表达为规范形式，就可以进行推理验证安全属性

定理证明的缺点：

  1. 需要程序员输入额外注释
  2. 交互式定理证明系统需要与用户交互
  3. 形式化程序转化为定理表达式存在困难，并且证明推理过程过于抽象，缺乏运行过程信息
  4. 漏洞产生过程的能力较差

典型工具

Saturn：该工具的实现主要基于函数abstract，同时基于条件约束进行分析。
ESC/Java：该工具用来检测 Java 漏洞。