软件漏洞分析技术第7章模型检测读书笔记。

  • 模型检测
    • 基本原理
      • 技术框架
      • 技术特点
    • 方法实现
      • 程序建模
      • 安全缺陷属性描述
      • 程序漏洞检测
    • 实例分析
      • 线性时序逻辑检查
      • 分布式软件漏洞检测
    • 典型工具
      • SLAM
      • MOPS

基本原理

模型检测（model checking）基于状态转换系统来判断程序的安全性质，基本分析步骤如下：

  1. 将软件构造为状态机等抽象模型
  2. 使用模态/时序逻辑公式等形式化表达描述安全属性
  3. 对模型进行遍历验证安全属性，判断是否存在漏洞

该方法优点有：

  1. 自动化程度高
  2. 可以检测多种属性
  3. 对有限状态系统而言，算法可终止
  4. 模型检测能够给出诊断信息

该方法的不足有：

  1. 状态空间爆炸
  2. 建模时，对时序、执行路径等安全属性边界的近似处理难度大
  3. 软件中可能存在数据无限性和控制无限性
  4. 检测对象为抽象模型，最终结果准确性取决于模型的准确性

安全缺陷属性描述

安全缺陷属性是指对实际编程开发中发现的不良变成习惯、程序逻辑错误代码等质量缺陷代码进行总结抽象，然后使用形式化语言描述建模形成用于检测的时序模式。

检测算法：模型检测算法比较多，如 labeling算法、fixpoint算法等。

典型工具

SLAM：该工具的应用对象是 windows 设备驱动程序，检测 API 库函数是否遵循文档说明中给出的使用规则。该工具可以对c程序进行自动抽象建模和验证。
MOPS：MOPS 是用于c语言程序漏洞和防御规则的一致性检测的工具。