软件安全性测试方法研究
3.6 基于属性的测试 文献[7]描 述 了基 于 属 性的 测 试 方 法 , 采 用 TASPEC 语 言 对 软件的安全属性进行描述生成安全属性规格说明, 利用程序切 片技术抽取与这个安全属性相关的代码, 测试这部分代码是否 违 反 安 全 属 性 规 格 说 明 。基 于 属 性 的 测 试 有 针 对 性 的 测 试 目 标
安全性测试(Security Testing)的主要方法和技术。
2 安全性测试的特点和分类
软件安全性测试是确定软件的安全特性实现是否与预期 设计一致的过程, 包括安全功能测试、渗透测试与验证过程。软 件安全性测试有其不同于其它测试类型的特殊性, 安全性相关 缺 陷 不 同 于 一 般 的 软 件 缺 陷 。一 个 很 难 发 现 的 软 件 安 全 漏 洞 可 能导致大量用户受到影响, 而一个很难发现的软件缺陷可能只 影 响 很 少 一 部 分 用 户 。安 全 性 测 试 不 同 于 传 统 测 试 类 型 最 大 的 区别是它强调软件不应当做什么, 而不是软件要做什么。非安 全性缺陷常常是违反规约, 即软件应当做 A, 它却做了 B。安全 性 缺 陷 常 常 由 软 件 的 副 作 用(Side- Effect )引 起 , 即 软 件 应 当 做 A, 它做了 A 的同时, 又做了 B。传统 测试 类 型 强调 软 件 的肯 定 需 求 (Positive Requirements), 例 如 用 户 账 户 3 次 登 陆 失 败 则 关 闭 此 账 户 。 安 全 性 测 试 更 强 调 软 件 的 否 定 需 求 (Negative Re- quirements), 例如未授权用户不能访问数据。技1Fra bibliotek引言术
安 全 性 是 软 件 质 量 的 一 个 重 要 属 性 。传 统 上 国 内 学 者 较 多
创 关 注 软 件 的 失 效 安 全 性(Safety),即 软 件 运 行 不 引 起 系 统 事 故 的 能力, 强调的是一类安全关键软件的安全性失效可能造成重大
新 人员伤亡、财产损失、环境污染等危险事故。对失效安全性的度 量 主 要 有 建 立 在 可 靠 性 理 论 基 础 上 的 安 全 度 、失 效 度 、平 均 事
施寅生: 硕士研究生 基 金 资 助 : 总 装 “十 一 五 ”预 研 项 目 (编 号 不 公 开 )
软 件 安 全 性 测 试 可 分 为 安 全 功 能 测 试 (Security Functional Testing)和 安 全 漏 洞 测 试 (Security Vulnerability Testing)两 个 方 面。安全功能测试基于软件的安全功能需求说明, 测试软件的 安全功能实现是否与安全需求一致, 需求实现是否正确完备。 软 件 安 全功 能 需 求主 要 包 括数 据 机 密性 、完 整 性、可 用 性 、不 可 否 认 性、身 份 认 证、授 权 、访 问控 制 、审 计跟 踪 、委 托、隐 私 保 护 、 安全管理等。安全漏洞测试从攻击者的角度, 以发现软件的安 全 漏 洞为 目 的 。安全 漏 洞 是指 系 统 在设 计 、实 现、操 作 、管 理 上 存 在 的 可 被 利 用 的 缺 陷 或 弱 点 。漏 洞 被 利 用 可 能 造 成 软 件 受 到 攻击, 使软件进入不安全的状态, 安全漏洞测试就是识别软件 的安全漏洞。
注人函数能够强制性地使程序进入到某些特定的状态, 而这些 状态在采用常规的标准测试技术的情况下一般是无法到达的。
3.5 模糊测试 模糊 测 试(Fuzz Testing)是一 种 发 现安 全 漏 洞 的 有 效 的 测 试 方法, 在安全性测试中越来越受到重视。模糊测试将随机的坏 数据插入程序, 观察程序是否能容忍杂乱输入。模糊测试是不 合逻辑的, 只是产生杂乱数据攻击程序。采用模糊测试攻击应 用程序可发现其他采用逻辑思维来测试很难发现的安全缺陷。
冲区溢出等。
创
新
图 1 自动化安全功能测试处理流程图 3.3 语法测试 语法测试是根据被测软件的功能接口的语法生成测试输 入, 检测被测软件对各类输入的响应。接口可以有多种类型, 命 令 行 、文 件 、环 境 变 量 、套 接 字 等 。语 法 测 试 基 于 这 样 一 种 思 想 , 软 件 的 接 口 明 确 或 隐 含 规 定 了 输 入 的 语 法 。语 法 定 义 了 软 件 接 受的输入数据的类型、格式。语法定义可采用 BNF 或正则表达 式。语法测试的步骤是识别被测软件接口的语言, 定义语言的 语法, 根据语法生成测试用例并执行测试。生成的测试输入应 当包含各类语法错误,符合语法的正确输入, 不符合语法的畸形 输入等。通过查看被测软件对各类输入的处理情况, 确定被测 软 件 是 否 存 在 安 全 缺 陷 。语 法 测 试 适 用 于 被 测 软 件 有 较 明 确 的 接口语法, 易于表达语法并生成测试输入的情况。语法测试结 合故障注入技术可得到更好的测试效果。 3.4 基于故障注入的安全性测试 Wenliang Du 将故 障 注入 技 术 用 于 软 件 安 全 性 测 试 , 建 立 软件与环境交互(Environment- Application Interaction , EAI)的 故 障模型。故障注入针对应用与环境的交互点, 主要包括用户输 入 、文 件 系统 、网 络 接口 、环 境 变量 等 引 起的 故 障 。相关 项 目 有 OUSPG (University of Oulu, Secure Programming Group)的 项 目 PROTOS Security Testing of Protocol Implementations, 该 项 目 的 目 标 是 测 试 协 议 实 现 的 安 全 性 。主 要 思 路 是 通 过 构 造 各 类 协 议 数 据 包 测 试 目 标 软 件 是 否 能 正 确 处 理 。实 质 是 在 各 类 协 议 数 据 包中植入故障, 如修改某些协议字段的值等, 以发现被测软件 是否存在安全漏洞, 支 持 的协 议 有 HTTP、SIP、WAP、SNMP 等。 故障注入可以有效地模拟各种各样的异常程序行为, 通过故障
3 安全性测试主要方法
随着软件安全性受到人们的重视, 安全性测试方法相关研 究取得了一定进展。
3.1 形式化安全测试 形式化方法的基本思想是建立软件的数学模型, 并在形式 规 格 说 明 语 言 的 支 持 下 ,提 供 软 件 的 形 式 规 格 说 明 。常 用 的 形 式 规格 说 明语 言 有 基于 模 型 的语 言,如 Z、VDM 和 B 等 ; 基 于 有 限 状 态 的 语 言,如 有 限 状 态 机 、SDL 和 状 态 图 等;基 于 行 为 的 语 言, 如 CSP、CCS、LOTOS 和 Petri 网等。形式化安全测试方法可分为 两类, 即定理证明和模型检测。定理证明方法将程序转换为逻 辑 公 式,然 后 使 用 公 理 和 规 则 证 明 程 序 是 一 个 合 法 的 定 理 。模 型 检测用状态迁移系统 S 描述软件的行为,用逻辑公式 F 表示软 件执行必须满足的性质, 通过自动搜索 S 中不满足公式 F 的状 态 来 发 现 软 件 中 的 漏 洞 。 National Aeronautics and Space Ad- ministration (NASA)的 一个 实 验 室 Jet Propulsion Laboratory (JPL) 开 展 过 形 式 化 安 全 测 试 方 面 的 项 目 。主 要 思 路 是 建 立 安 全 需 求 的形式化模型, 例如状态机模型。安全测试即搜索状态空间, 看 是否能从起始状态找到一条路径到达违反规约的不安全的状 态。形式化安全测试方法有一定的局限性。对于定理证明方法 , 由于定理证明过程难以完全自动化, 需要高素质分析人员的大 量参与,证明过程非常耗时费力,一般只用于验证设计阶段的程
(北京系统工程研究所)施 寅 生 邓 世 伟 谷 天 阳
S HI YINS HENG DENG S HIWEI GU TIANYANG
摘要:软 件 安 全 性 测 试 是 保 证 软 件 安 全 性 的 重 要 手 段 。本 文 论 述 了 软 件 安 全 性 测 试 的 特 点 和 主 要 内 容 , 重 点 研 究 了 国 内 外 软
技 Lori Pollock 提 出 一 种 基 于 动 态 编 译 技 术 的 安 全 测 试 框 架 , 可
在 程 序 运 行 时 插 入 攻 击 代 码 , 测 试 安 全 机 制 是 否 可 用 完 备 。主
术 要用 来 测试 基 于 程 序 的 攻 击(Program- Based Attacks),如 堆 栈 缓
属 性 。软 件 安 全 性 是 软 件 在 受 到 恶 意 攻 击 时 仍 提 供 所 需 功 能 的
能力。对于保密安全性测试(Security testing), 目前主要有静态分
析、形 式 化方 法 、故 障注 入 、基 于模 型 的 测试 、基 于 属性 的 测 试、
语法测试、模糊测试(Fuzz Testing)等测试方法。本文将重点关注
- 56 - 360元 / 年 邮局订阅号: 82-946
《现场总线技术应用 200 例》
您的论文得到两院院士关注
信息安全
序规范而非实际代码。对于模型检测方法, 由于需要穷尽程序 的所有实际执行状态,所以模型检测的效率较低,并且很难检验 无穷状态系统。
3.2 基于模型的安全功能测试 基于模型的测试方法是对软件的行为和结构进行建模, 生 成测试模型, 由测试模型生成测试用例, 驱动软件测试。常用的 软件测试模型有有限状态机、UML 模型、马尔可夫 链 等 。Mark Blackburn、Robert Busser 研 究 了 基 于 模 型 的 安 全 功 能 测 试 。 主 要项目支 撑 是 NIST Computer Security Division (CSD)部 门 的 项 目 Automated Security Functional Testing。 主 要 思 路 是 利 用 SCRModeling 工 具 对 软 件 的 安 全 功 能 需 求 进 行 建 模 , 使 用 表 单方式设计软件的安全功能行为模型, 将表单模型转换成测 试 规 格 说 明 模 型 , 利 用 T- VEC 工 具 生 成 测 试 向 量 (由 一 组 输 入 变 量 , 期 望 输 出 变 量 组 成 ), 将 测 试 向 量 输 入 测 试 驱 动 执 行 测 试(如 图 1)。 这 种 方 法 是 一 种 一 般 的 安 全 功 能 测 试 方 法 , 它 的适用范围取决于安全功能的建模能力, 特别适用于建模用 与 或 子 句 表 达 逻 辑 关 系 的 安 全 需 求 , 对 授 权 、访 问 控 制 等 安 全功能测试比较适用。