软件漏洞分析技术:模型检测
软件漏洞分析技术第7章模型检测读书笔记。
- 模型检测
- 基本原理
- 技术框架
- 技术特点
- 方法实现
- 程序建模
- 安全缺陷属性描述
- 程序漏洞检测
- 实例分析
- 线性时序逻辑检查
- 分布式软件漏洞检测
- 典型工具
- SLAM
- MOPS
基本原理
模型检测(model checking)基于状态转换系统来判断程序的安全性质,基本分析步骤如下:
- 将软件构造为状态机等抽象模型
- 使用模态/时序逻辑公式等形式化表达描述安全属性
- 对模型进行遍历验证安全属性,判断是否存在漏洞
该方法优点有:
- 自动化程度高
- 可以检测多种属性
- 对有限状态系统而言,算法可终止
- 模型检测能够给出诊断信息
该方法的不足有:
- 状态空间爆炸
- 建模时,对时序、执行路径等安全属性边界的近似处理难度大
- 软件中可能存在数据无限性和控制无限性
- 检测对象为抽象模型,最终结果准确性取决于模型的准确性
安全缺陷属性描述
安全缺陷属性是指对实际编程开发中发现的不良变成习惯、程序逻辑错误代码等质量缺陷代码进行总结抽象,然后使用形式化语言描述建模形成用于检测的时序模式。
检测算法:模型检测算法比较多,如 labeling算法、fixpoint算法等。
典型工具
SLAM:该工具的应用对象是 windows 设备驱动程序,检测 API 库函数是否遵循文档说明中给出的使用规则。该工具可以对c程序进行自动抽象建模和验证。
MOPS:MOPS 是用于c语言程序漏洞和防御规则的一致性检测的工具。
All articles in this blog are licensed under CC BY-NC-SA 4.0 unless stating additionally.