搜索

[13247] 2018-09-30_智能合约自动化审计技术浅析

文档创建者：s7ckTeam
浏览次数：4
最后更新：2025-01-18
2018-09-30_智能合约自动化审计技术浅析 智 能 合 约 自 动 化 审 计 技 术 浅 析 猎 豹 实 验 室   F r e e B u f   2 0 1 8 - 0 9 - 3 0 前 言 前 言 经 过 经 过 T H E   D A O 事 件 、 币 安 被 盗 事 件 ， 智 能 合 约 的 安 全 性 越 来 越 受 到 业 内 关 注 。 本 文 根 据 猎 豹 区 块 链 安 全 专 家 事 件 、 币 安 被 盗 事 件 ， 智 能 合 约 的 安 全 性 越 来 越 受 到 业 内 关 注 。 本 文 根 据 猎 豹 区 块 链 安 全 专 家 杨 文 玉 杨 文 玉 9 月 月 5 日 在 星 球 日 报 日 在 星 球 日 报 P . O . D 大 会 上 的 分 享 录 音 整 理 而 成 ， 浅 析 当 前 智 能 合 约 的 发 展 现 状 ， 以 及 智 能 合 约 自 大 会 上 的 分 享 录 音 整 理 而 成 ， 浅 析 当 前 智 能 合 约 的 发 展 现 状 ， 以 及 智 能 合 约 自 动 化 检 测 的 一 些 方 法 。 动 化 检 测 的 一 些 方 法 。 一 、 智 能 合 约 发 展 现 状 一 、 智 能 合 约 发 展 现 状 首 先 我 们 来 一 起 看 看 现 在 智 能 合 约 发 展 的 一 个 现 状 ： 在 过 去 一 个 月 当 中 ， 智 能 合 约 的 数 量 每 天 还 在 以 1 3 1 7 个 的 平 均 增 长 率 高 速 稳 定 的 增 长 着 ， 这 和 我 们 所 理 解 的 “ 区 块 链 现 在 处 于 寒 冬 的 时 期 ” 不 太 一 样 ， 其 实 智 能 合 约 的 增 长 率 还 是 比 较 稳 定 的 。 现 在 智 能 合 约 比 较 多 的 应 用 在 一 些 基 础 设 施 、 商 业 零 售 、 游 戏 以 及 社 交 媒 体 和 通 讯 领 域 中 。 二 、 智 能 合 约 安 全 现 状 二 、 智 能 合 约 安 全 现 状 从 1 7 年 9 月 到 1 8 年 6 月 ， 智 能 合 约 的 漏 洞 频 繁 爆 发 ， 每 次 漏 洞 爆 发 都 带 来 了 大 量 的 资 金 损 失 。 这 使 得 一 些 区 块 链 开 发 者 、 智 能 合 约 的 开 发 者 或 者 一 些 用 户 对 智 能 合 约 安 全 性 产 生 高 度 的 质 疑 ， 也 阻 碍 了 以 太 坊 之 后 的 一 些 发 展 。 除 了 基 本 的 智 能 合 作 安 全 ， 现 在 D A P P 的 安 全 也 是 受 到 了 极 大 的 关 注 。 比 如 说 F O M O 3 D 在 兴 起 的 时 候 ， 仅 仅 在 第 二 天 就 出 现 了 大 量 的 山 寨 合 约 、 山 寨 的 游 戏 。 在 这 些 游 戏 中 ， 开 发 者 巧 妙 地 更 改 了 资 金 分 配 的 逻 辑 ， 使 得 玩 家 在 玩 F O M O 3 D 游 戏 的 过 程 中 ， 投 入 的 资 金 其 实 大 部 分 都 是 流 向 于 这 种 山 寨 合 约 的 开 发 者 的 ， 这 对 D A P P 的 发 展 有 了 极 大 的 阻 碍 。 现 在 我 们 共 同 面 临 着 一 个 问 题 — — 如 何 保 证 海 量 的 智 能 合 约 的 安 全 。 三 、 智 能 合 约 自 动 化 审 计 方 法 三 、 智 能 合 约 自 动 化 审 计 方 法 我 们 来 回 顾 一 下 现 在 智 能 合 约 的 情 况 。 截 止 到 昨 天 中 午 1 2 点 ， 据 统 计 ， 现 在 共 有 1 9 3 万 个 智 能 合 约 ， 并 且 一 直 保 持 着 稳 定 的 日 增 长 率 。 现 在 的 审 计 方 法 有 人 工 的 攻 防 审 计 以 及 自 动 化 的 审 计 。 在 海 量 的 智 能 合 约 中 ， 最 好 的 一 种 设 想 就 是 要 降 低 人 工 审 计 的 一 些 复 杂 度 ， 从 而 更 多 的 通 过 自 动 化 审 计 来 进 行 。 我 们 把 自 动 化 审 计 分 为 三 个 部 分 ：
第 一 种 就 是 特 征 代 码 的 匹 配 ， 第 二 类 就 是 基 于 形 态 化 验 证 的 自 动 化 审 计 ， 最 后 一 类 是 基 于 符 号 执 行 和 符 号 抽 象 的 自 动 化 审 计 。 1 、 特 征 代 码 匹 配 、 特 征 代 码 匹 配 我 们 首 先 看 这 一 项 ， 特 定 代 码 匹 配 。 大 家 从 名 字 上 来 看 应 该 就 能 理 解 到 ， 其 实 它 就 是 对 恶 意 代 码 进 行 一 些 提 取 抽 象 ， 像 我 们 之 前 做 的 代 码 静 态 检 测 ， 我 们 抽 样 成 一 种 语 义 匹 配 ， 然 后 再 去 匹 配 它 的 静 态 源 代 码 。 这 种 审 计 的 方 法 的 优 点 是 显 而 易 见 的 ， 比 如 说 速 度 很 快 ， 因 为 它 就 是 对 原 码 进 行 一 个 字 符 串 的 匹 配 。 第 二 是 它 能 够 迅 速 的 响 应 新 的 漏 洞 ， 因 为 这 种 审 计 方 法 大 部 分 是 以 插 件 形 式 开 发 ， 比 如 出 现 了 一 个 新 的 漏 洞 ， 我 们 就 可 以 快 速 提 交 一 些 新 的 匹 配 模 式 。 那 么 它 的 缺 点 在 哪 里 呢 ？ 我 们 所 理 解 的 现 在 的 区 块 链 都 应 该 是 公 开 透 明 的 ， 但 实 际 情 况 并 不 是 这 样 ， 我 们 大 概 做 了 一 个 统 计 ， 目 前 代 码 的 开 源 率 仅 仅 只 占 4 8 . 6 2 % ， 也 就 是 在 以 太 坊 上 其 实 有 超 过 一 半 的 智 能 合 约 是 不 开 源 的 ， 只 暴 露 它 的 一 个 O P C O D E 。 对 于 O P C O D E 的 分 析 对 于 安 全 人 员 来 说 其 实 也 是 面 临 着 巨 大 的 挑 战 ， 有 些 人 费 了 十 分 大 的 力 气 ， 去 逆 向 O P C O D E ， 这 就 导 致 了 它 的 适 用 范 围 极 为 有 限 。 其 次 就 是 漏 报 率 高 。 因 为 它 的 一 些 静 态 审 计 方 法 其 实 并 不 和 传 统 的 静 态 代 码 审 计 方 法 一 致 ， 传 统 的 静 态 审 计 方 法 ， 比 如 说 A P P 检 测 ， 我 会 调 用 库 里 面 ， 确 定 稳 定 的 一 些 函 数 ， 来 对 它 进 行 审 计 ， 但 智 能 合 约 里 面 它 的 一 些 函 数 、 它 一 些 特 征 等 等 ， 还 是 变 化 性 比 较 多 的 ， 所 以 说 它 的 漏 报 率 会 比 较 高 。 2 、 基 于 形 式 化 验 证 的 自 动 化 审 计 、 基 于 形 式 化 验 证 的 自 动 化 审 计 第 二 个 方 法 ， 我 们 来 探 讨 一 下 现 在 比 较 火 的 ， 基 于 形 式 化 验 证 的 自 动 化 审 计 。 形 式 化 验 证 来 审 计 智 能 合 约 安 全 ， 最 早 是 在 1 6 年 ， 由 H i r a i 提 供 的 ， 当 时 拿 I s a b e l l e 高 阶 逻 辑 交 互 定 理 证 明 器 ， 然 后 交 E V M 的 一 些 O P C O D E   ， 通 过 它 的 一 个 l e m   l a n g u a g e 转 化 成 了 一 个 形 式 化 的 m o d e l ， 然 后 通 过 形 式 化 m o d e l 的 验 证 来 去 判 断 它 代 码 中 的 逻 辑 是 否 存 在 问 题 。 而 基 于 这 项 工 作 ， 之 后 由 两 个 学 家 把 形 式 化 方 法 进 行 了 进 一 步 的 改 正 ， 也 就 是 说 他 们 放 弃 了 l e m   l a n g u a g e 这 种 比 较 低 效 的 转 换 方 式 ， 采 用 了 F - f r a m e w o r k 和 K - f r a m e w o r k 将 D V M 转 化 为 一 个 f o r m a l   m o d e l ， 而 F - f r a m e w o r k 就 是 N A S A 他 们 经 常 在 航 空 航 天 领 域 当 中 做 一 些 形 式 化 漏 洞 验 证 的 框 架 ， 而 K - f r a m e w o r k 就 是 语 意 的 一 些 整 合 框 架 。 3 、 基 于 符 号 执 行 、 符 号 抽 象 的 自 动 化 审 计 、 基 于 符 号 执 行 、 符 号 抽 象 的 自 动 化 审 计 第 三 点 ， 也 是 我 今 天 想 要 着 重 跟 大 家 交 流 的 ， 以 及 现 在 最 常 用 的 方 法 ， 就 是 基 于 符 号 执 行 和 符 号 抽 象 的 一 些 自 动 化 审 计 。 我 们 在 分 析 一 个 智 能 合 约 的 时 候 ， 我 们 首 先 要 明 确 我 们 的 分 析 对 象 是 什 么 。 也 就 像 我 们 刚 才 在 解 释 的 那 个 特 征 匹 配 代 码 当 中 ， 我 们 知 道 其 实 现 在 E V M 上 合 约 代 码 大 部 分 是 不 公 开 的 。 我 们 就 确 认 应 该 是 一 个 E V M   O P C O D E ， 通 过 一 些 源 码 ， 编 译 ， 可 以 形 成 一 个 O P C O D E ， 然 后 输 入 到 我 们 自 动 化 分 析 引 擎 。 在 这 种 基 于 符 号 执 行 和 符 号 抽 象 化 的 自 动 化 审 计 框 架 里 面 ， 其 实 它 有 些 共 有 的 特 性 ， 就 是 它 在 O P C O D E 或 者 在 输 到 这 个 引 擎 之 后 ， 都 会 转 化 成 一 个 C F G ， 就 是 我 们 的 一 个 C o n t r o l   f l o w   g r a p h ， 即 控 制 流 程 图 。 可 以 简 单 了 解 一 下 这 个 C F G 是 什 么 意 思 。 C F G 就 是 说 他 把 合 约 代 码 里 面 的 逻 辑 包 装 成 每 个 块 ， 然 后 有 逻 辑 有 分 叉 的 时 候 ， 比 如 说 有 I F 等 等 这 种 判 断 的 时 候 ， 就 把 它 分 叉 。 比 如 说 左 边 这 个 a s s e r t i o n 这 个 合 约 ， 我 们 首 先 是 将 i n p u t 与 2 5 6 进 行 一 个 比 较 ， 那 么 在 出 现 一 个 I f 的 判 断 之 后 ， 我 们 需 要
对 这 个 C F G 进 行 一 个 分 叉 。 C F G   B u i l d e r 主 要 是 对 O P C O D E 这 种 智 能 合 约 代 码 ， 把 它 形 成 一 个 十 分 庞 大 完 善 的 一 个 C F G ， 然 后 让 程 序 员 更 好 的 去 了 解 它 里 面 执 行 的 一 些 逻 辑 。 再 有 C F G 生 成 了 之 后 ， 就 是 这 样 两 种 分 析 方 法 。 第 一 类 就 是 基 于 符 号 执 行 的 验 证 ， 这 边 比 较 有 代 表 性 的 ， 可 能 大 家 都 比 较 熟 知 的 像 M y t h r i l 、 O y e n t e 、 M a i a n 。 还 有 一 种 就 是 ， 上 个 月 他 们 刚 刚 公 开 的 一 个 符 号 抽 象 分 析 的 方 法 ， 也 就 是 S e c u r i f y 。 下 面 主 要 分 析 一 下 O y e n t e 以 及 S e c u r i f y 这 两 种 系 统 的 一 个 具 体 的 架 构 以 及 实 现 方 法 。 O y e n t e 符 号 执 行 验 证 符 号 执 行 验 证 O y e n t e 的 逻 辑 是 在 C F G b u i l d 形 成 之 后 ， 首 先 是 一 个 E X P L O R E R ， E X P L O R E R 的 意 思 就 是 说 我 会 把 代 码 当 中 的 每 一 个 流 程 都 去 验 证 一 遍 ， 进 行 一 个 之 外 的 验 证 。 我 们 的 验 证 就 是 是 否 有 一 个 X ， 使 得 X 不 仅 满 足 C 1 、 C 2 、 C 3 三 个 条 件 ， 并 且 Z = X + 2 ， 那 么 这 时 候 我 们 可 以 判 断 他 的 状 态 是 n o 还 是 y e s ， 然 后 以 此 来 验 证 整 个 逻 辑 的 一 个 流 程 。 到 了 第 二 个 c o d e   a n a l y s i s ， 这 一 部 分 其 实 是 这 个 O y e n t e 最 为 核 心 的 一 个 部 分 ， 就 是 它 将 刚 刚 输 出 的 E X P L O R S E 这 种 路
径 把 它 转 化 ， 至 始 至 终 只 包 含 E t h e r 的 一 些 路 径 ， 进 行 一 些 漏 洞 验 证 ， 而 他 目 前 只 提 供 包 括 T O D 、 T i m e s t a m p d e p e n d e n c e 、 M i s h a n d l e d   e x c e p t i o n s 这 三 种 验 证 ， 最 后 系 统 为 了 保 证 误 报 率 和 漏 报 率 ， 采 用 了 微 软 的 Z 3 B i t - V e c t o r S o l v e r   开 源 的 验 证 器 ， 然 后 来 进 行 整 体 架 构 的 一 个 封 装 。 在 刚 刚 我 们 讲 述 的 过 程 当 中 ， 其 实 大 家 也 应 该 了 解 到 ， 在 C F G 转 E X P L O R E R 验 证 的 时 候 ， 我 们 需 要 对 它 的 循 环 的 每 次 都 进 行 一 个 验 证 ， 所 以 说 这 种 分 析 方 法 特 别 耗 时 ， 并 且 也 不 一 定 成 功 。 比 如 说 像 p a r i t y 的 那 个 钱 包 代 码 ， 它 的 O y e n t e 覆 盖 率 仅 仅 达 到 2 0 % ， 剩 下 8 0 % 的 代 码 ， 是 没 有 办 法 去 跟 踪 的 ， 所 以 这 就 是 O y e n t e 目 前 存 在 一 个 巨 大 的 问 题 。 S e c u r i f y 符 号 抽 象 分 析 符 号 抽 象 分 析 在 这 个 问 题 的 基 础 上 ， 像 S e c u r i f y 他 们 就 提 供 了 另 外 一 种 方 法 ， 它 们 认 为 现 在 合 约 代 码 其 实 是 特 别 容 易 解 耦 合 的 ， 不 像 我 们 传 统 的 代 码 一 样 ， 它 的 耦 合 性 特 别 高 ， 但 像 合 约 代 码 里 面 ， 就 有 t r a n s f e r 等 等 一 些 比 较 固 定 解 耦 合 的 一 些 结 构 和 模 块 ， 我 们 并 不 是 需 要 对 整 个 合 约 的 逻 辑 进 行 的 校 验 ， 可 能 我 们 就 是 对 合 约 解 耦 合 的 各 个 模 块 进 行 校 验 分 析 ， 因 此 可 以 提 高 它 的 自 动 化 程 度 。 这 张 图 也 就 是 他 们 整 个 在 验 证 的 一 个 流 程 ： 它 们 把 c o n t r a c t   b y t e c o d e 转 化 成 一 种 他 们 自 定 义 的 一 种 语 义 语 言 ， 然 后 通 过 自 定 义 的 语 义 语 言 ， 它 们 之 后 有 一 个 验 证 模 块 ， 这 个 验 证 模 块 就 特 别 像 我 们 之 前 说 的 那 种 模 式 匹 配 ， 就 是 把 一 些 漏 洞 转 化 成 一 种 它 验 证 语 言 的 模 式 匹 配 的 框 架 ， 然 后 去 验 证 它 这 个 语 意 在 此 是 否 满 足 他 这 个 比 较 ， 最 终 会 生 成 一 个 安 全 报 告 。 这 里 也 给 出 了 一 个 p a r i t y 的 例 子 ， 通 过 自 动 化 审 计 的 方 法 ， 最 终 可 以 输 出 钱 包 的 o w n e r 其 实 是 可 以 被 修 改 的 。 再 具 体 一 点 ， 它 是 怎 么 做 语 义 分 析 的 呢 ？ S e c u r i f y 分 析 这 种 合 约 代 码 ， 是 从 两 个 维 度 ， 第 一 个 是 逻 辑 ， 第 二 个 是 数 据 。 在 逻 辑 方 向 的 话 ， 它 定 义 了 两 种 逻 辑 ， 第 一 个 叫 M a y F o l l o w ， 第 二 叫 M u s t F o l l o w 。 M a y F o l l o w 的 意 思 是 说 L 2 是 有 一 条 路 径 是 跟 在 L 1 后 面 的 ， 而 M u s t F o l l o w 是 说 L 2 每 一 条 路 径 都 跟 在 L 1 后 面 。 这 两 种 区 别 定 了 它 整 个 逻 辑 的 一 个 框 架 。 第 一 个 就 是 它 的 一 个 数 据 ， 它 怎 么 定 义 合 约 里 面 的 数 据 变 化 ？ 分 了 三 种 ， 第 一 种 是 M a y D e p O n ， 就 是 两 个 因 素 ， 一 个 叫 Y 、 一 个 叫 T ， T 变 Y 可 能 变 也 可 能 不 变 。
第 二 个 就 是 E q ， 就 是 说 Y 是 由 T 来 决 定 的 第 三 个 就 是 大 家 把 D e t B y 和 Y 和 T 是 一 一 对 应 的 ， 只 要 T 变 Y 就 肯 定 要 变 了 。 这 里 面 就 用 更 加 形 象 的 方 法 ， 我 们 想 象 一 下 ， M a y D e p O n 就 是 ， 变 量 是 T ， 在 一 段 时 间 当 中 Y 可 能 是 一 个 值 ， 然 后 有 的 说 T 变 Y 可 能 不 变 ， 第 三 个 D e t B y 就 是 说 一 对 一 的 关 系 ， 就 比 如 说 我 们 知 道 哈 希 ， 哈 希 如 果 T 变 ， Y 就 肯 定 要 变 。 通 过 逻 辑 和 数 据 这 两 个 维 度 进 行 了 一 些 验 证 ， 最 终 验 证 模 块 的 话 ， 现 在 提 供 了 大 概 六 七 个 智 能 合 约 漏 洞 的 验 证 性 的 语 言 ， 而 且 这 种 语 言 都 是 以 插 件 化 的 形 式 来 写 的 ， 其 他 的 安 全 开 发 者 可 以 不 断 去 丰 富 这 个 漏 洞 的 验 证 语 言 ， 最 终 我 们 在 对 自 动 化 审 计 进 行 一 个 评 估 的 时 候 ， 我 们 其 实 是 要 从 它 的 自 动 化 程 度 ， 漏 报 率 、 误 报 率 来 评 估 这 件 事 情 的 。 像 我 们 现 在 知 道 的 一 些 数 据 就 可 以 表 明 出 来 ， 其 实 像 M y t h r i l 跟 O y e n t e ， 它 里 面 存 在 大 量 的 误 报 ， 比 如 说 它 检 测 出 来 的 数 据 还 是 需 要 人 工 进 行 二 次 确 认 ， 这 个 工 作 其 实 是 非 常 繁 琐 ， 而 S e c u r i f y 这 种 方 法 可 能 误 报 率 会 降 低 。 这 也 是 两 种 比 较 现 在 比 较 流 行 的 符 号 执 行 和 抽 象 的 自 动 化 审 计 方 法 。 四 、 总 结 回 顾 四 、 总 结 回 顾 最 后 我 们 回 顾 一 下 ， 现 在 做 的 智 能 合 约 审 计 的 话 可 能 分 为 三 种 ， ： 特 征 代 码 匹 配 、 形 式 化 验 证 以 及 符 号 抽 象 。 回 顾 整 个 解 释 的 过 程 当 中 ， 我 们 可 以 清 楚 地 知 道 ， 现 在 自 动 化 审 计 的 方 法 其 实 是 出 于 一 个 很 不 成 熟 的 阶 段 。 它 们 主 要 面 临 三 大 问 题 ： 第 一 个 就 是 误 报 率 高 ， 其 实 它 并 不 能 做 到 完 全 自 动 化 ， 它 还 需 要 人 工 的 一 些 参 与 。 第 二 个 就 是 它 的 自 动 化 其 实 程 度 比 较 低 ， 还 需 要 不 断 有 f e e d b a c k 去 去 审 计 。 第 三 就 是 审 计 时 间 比 较 长 ， 比 如 说 像 M y t h r i l ， 平 均 在 6 0 秒 ， O y e n t e 大 概 在 3 0 秒 ， 而 S e c u r i f y 大 概 在 2 0 秒 。 * 本 文 作 者 ： 猎 豹 区 块 链 安 全 实 验 室 ， 转 载 请 注 明 来 自 本 文 作 者 ： 猎 豹 区 块 链 安 全 实 验 室 ， 转 载 请 注 明 来 自 F r e e B u f . C O M
阅 读 原 文
回复

举报

高级模式
B Color Image Link Quote Code Smilies
您需要登录后才可以回帖 登录 | 立即注册

本版积分规则

使用Markdown编辑器编辑 使用富文本编辑器编辑

Archiver| 手机版| 小黑屋|
Powered by Discuz! X3.4 Copyright © 2001-2020, Tencent Cloud. 商业源码建议获取授权，如侵犯您的权益，请联系客服处理