搜索

[12707] 2018-05-15_Z3Py在CTF逆向中的运用

文档创建者：s7ckTeam
浏览次数：0
最后更新：2025-01-18
2018-05-15_Z3Py在CTF逆向中的运用 Z 3 P y 在 C T F 逆 向 中 的 运 用 f o y j o g   F r e e B u f   2 0 1 8 - 0 5 - 1 5 前 言 前 言 Z 3 是 是 M i c r o s o f t   R e s e a r c h 开 发 的 高 性 能 定 理 证 明 器 。 开 发 的 高 性 能 定 理 证 明 器 。 Z 3 拥 有 者 非 常 广 泛 的 应 用 场 景 ： 软 件 拥 有 者 非 常 广 泛 的 应 用 场 景 ： 软 件 / 硬 件 验 证 和 测 试 ， 约 硬 件 验 证 和 测 试 ， 约 束 求 解 ， 混 合 系 统 分 析 ， 安 全 性 研 究 ， 生 物 学 研 究 （ 计 算 机 分 析 ） 以 及 几 何 问 题 。 束 求 解 ， 混 合 系 统 分 析 ， 安 全 性 研 究 ， 生 物 学 研 究 （ 计 算 机 分 析 ） 以 及 几 何 问 题 。 Z 3 P y 是 使 用 是 使 用 P y t h o n 脚 本 来 解 脚 本 来 解 决 一 些 实 际 问 题 。 决 一 些 实 际 问 题 。 C T F 逆 向 中 的 应 用 逆 向 中 的 应 用 现 在 的 C T F 逆 向 中 ， 求 解 方 程 式 或 者 求 解 约 束 条 件 是 非 常 常 见 的 一 种 考 察 方 式 ， 而 c t f 比 赛 都 是 限 时 的 ， 当 我 们 已 经 逆 向 出 来 f l a g 的 约 束 条 件 时 ， 可 能 还 需 要 花 一 定 的 时 间 去 求 解 逆 过 程 。 而 Z 3 求 解 器 就 给 我 们 提 供 了 一 个 非 常 便 利 求 解 方 式 ， 我 们 只 需 要 定 义 未 知 量 （ x , y 等 ） ， 然 后 为 这 些 未 知 量 添 加 约 束 方 式 即 可 求 解 。 Z 3 求 解 器 能 够 求 解 任 意 多 项 式 ， 但 是 要 注 意 的 是 ， 当 方 程 的 方 式 为 2 * * x 这 种 次 方 运 算 的 时 候 ， 方 程 式 已 经 不 是 多 项 式 的 范 畴 了 ， Z 3 便 无 法 求 解 。 基 本 使 用 基 本 使 用 现 在 我 们 利 用 官 方 文 档 中 的 一 个 例 子 来 粗 略 的 看 一 下 Z 3 P y 的 使 用 。 代 码 非 常 简 单 ， 首 先 利 用 I n t ( ) 定 义 两 个 i n t 型 未 知 数 x 和 y ， 然 后 利 用 三 个 约 束 条 件 进 行 相 应 的 求 解 ： 1 .   x   >   2 2 .   y   <   1 0 3 .   x   +   2 * y   = =   7 由 上 述 的 代 码 看 得 出 来 Z 3 P y 的 使 用 方 式 比 较 简 单 ， 1 .   定 义 未 知 量 2 .   添 加 约 束 条 件 3 .   然 后 求 解 C T F 中 的 示 例 中 的 示 例 X X X 比 赛 中 的 逆 向 题 比 赛 中 的 逆 向 题 首 先 我 们 利 用 I D A 去 打 开 该 文 件 ， 定 位 到 关 键 点 ， 发 现 关 键 函 数 如 下 ：
可 以 看 得 出 来 这 个 题 目 的 目 的 就 是 找 出 满 足 方 程 的 f l a g 。 我 们 可 以 很 方 便 的 把 方 程 式 列 出 来 ， 但 是 求 解 对 于 一 些 数 学 不 是 很 好 的 人 来 说 简 直 就 是 噩 梦 ， 这 时 候 Z 3 求 解 器 就 可 以 很 方 便 的 给 我 们 帮 助 。 我 们 按 照 题 目 的 意 思 一 步 一 步 利 用 Z 3 求 解 器 来 求 解 ： S o l v e r ( ) 命 令 创 建 一 个 通 用 求 解 器 。 我 们 可 以 通 过 a d d 函 数 添 加 约 束 条 件 。 我 们 称 之 为 声 明 约 束 条 件 。 c h e c k ( ) 函 数 解 决 声 明 的 约 束 条 件 ， s a t 结 果 表 示 找 到 某 个 合 适 的 解 ， u n s a t 结 果 表 示 没 有 解 。 这 时 候 我 们 称 约 束 系 统 无 解 。 最 后 ， 求 解 器
可 能 无 法 解 决 约 束 系 统 并 返 回 未 知 作 为 结 果 。 对 于 上 面 的 题 目 我 们 首 先 定 义 x 1 , x 2 , x 3 , x 4 四 个 i n t 变 量 ， 然 后 添 加 逆 向 中 的 约 束 条 件 ， 最 后 进 行 求 解 。 Z 3 会 在 找 到 合 适 解 的 时 候 返 回 s a t 。 我 们 认 为 Z 3 能 够 满 足 这 些 约 束 条 件 并 得 到 解 决 方 案 。 该 解 决 方 案 被 看 做 一 组 解 决 约 束 条 件 的 模 型 。 模 型 能 够 使 求 解 器 中 的 每 个 约 束 条 件 都 成 立 。 最 后 我 们 遍 历 m o d e l 中 的 解 。 得 到 x 1 , x 2 , x 3 , x 4 的 解 后 ， 我 们 将 其 代 入 逆 向 题 中 ， 得 出 v 1 , v 2 , v 7 , v 8 , v 9 , v 9 , v 1 0 , v 1 1 , v 1 2 的 值 ， 然 后 进 行 下 一 步 的 求 解 ： 这 样 的 话 我 们 就 花 了 比 较 少 的 时 间 得 到 我 们 想 要 的 f l a g ， 还 是 比 较 方 便 的 。 但 是 现 实 中 很 多 的 逆 向 题 都 是 基 于 位 运 算 的 ， 同 样 在 Z 3 P y 中 可 以 使 用 B i t _ V e c t o r s 进 行 机 器 运 算 。 它 们 能 够 实 现 无 符 号 和 有 符 号 二 进 制 运 算 。 Z 3 为 符 号 数 运 算 提 供 了 一 个 特 殊 的 运 算 符 操 作 版 本 ， 其 中 运 算 符 < ， < = ， > ， >   = ， / ， ％ 和 > > 对 应 于 有 符 号 运 算 。   相 应 的 无 符 号 运 算 符 是 U L T ， U L E ， U G T ， U G E ， U D i v ， U R e m 和 L S h R 。 我 们 看 一 下 如 下 的 代 码 就 能 清 楚 许 多 ： Z 3 P y 同 样 支 持 了 P y t h o n 中 的 创 建 L i s t 的 方 式 ， 我 们 看 如 下 代 码 ：
在 上 面 的 例 子 中 ， 表 达 式 “ x ％ s ” ％ i 返 回 一 个 字 符 串 ， 其 中 ％ s 被 替 换 为 i 的 值 。 命 令 p p 与 p r i n t 类 似 ， 但 是 它 使 用 Z 3 P y 格 式 化 程 序 而 不 是 P y t h o n 的 格 式 化 程 序 来 使 用 列 表 和 元 组 。 第 八 届 极 客 大 挑 战 的 第 八 届 极 客 大 挑 战 的 R E C o n v o l u t i o n 我 们 打 开 文 件 ， 也 是 比 较 直 观 的 看 到 约 束 条 件 ， 我 试 着 逆 向 了 这 个 过 程 ， 花 费 了 挺 多 的 时 间 才 得 到 答 案 ， 但 是 如 果 我 们 使 用 Z 3 P y 来 求 解 的 话 就 会 非 常 的 快 。 函 数 关 键 部 分 如 下 ：
很 简 洁 明 了 ， 我 们 利 用 Z 3 P y 来 进 行 变 量 的 声 明 和 约 束 的 增 加 并 进 行 求 解
很 简 单 的 几 行 代 码 ， 声 明 0 x 2 2 个 8 位 B i t V e c 的 未 知 数 ， 获 取 数 据 ， 然 后 增 加 约 束 条 件 ， 求 解 ， 这 样 就 能 够 帮 助 我 们 获 取 f l a g 。 题 目 链 接 ： h t t p s : / / p a n . b a i d u . c o m / s / 1 o 8 Q d F I E 总 结 总 结 虽 然 C T F 逆 向 比 赛 中 重 点 考 察 的 是 逆 向 的 能 力 ， 采 用 求 解 器 的 方 式 来 求 解 并 不 能 锻 炼 到 自 己 的 逆 向 逻 辑 ， R E C o n v o l u t i o n 逆 向 题 目 有 一 个 非 常 清 晰 明 了 的 逆 过 程 ， 还 是 很 有 趣 的 。 *   本 文 作 者 ： f o y j o g ， 转 载 请 注 明 来 自 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. 商业源码建议获取授权，如侵犯您的权益，请联系客服处理