8.2 LLM提假设、angr验证

8.2 LLM提假设、angr验证

本节摘要：本章核心一节。8.1 节的流程里有个体力活：读伪代码、猜校验函数在哪、猜成功与失败各输出什么、猜口令长度——这恰是大模型的强项，但让大模型直接「下结论」又是幻觉的重灾区。本节的闭环架构把两者各放在擅长的一侧：LLM 读反编译伪代码，输出结构化「假设」（校验函数、成功串、失败串、长度四字段）；程序按假设渲染 8.1 节的 angr 探索脚本；沙箱运行后，found 与 avoid 与超时三种结果回填——结论由求解器背书，失败信息回喂模型修正假设。本节先立「模型不下结论」的规矩，再拆五环节架构与最小实现，随后给出三条反幻觉机理与一次 REFUTED 迭代的实录示例，最后介绍 angr 官方 MCP server，把闭环升级为模型可直接调用的工具。

学习目标

• 画出并讲解「LLM 提假设、angr 验证」闭环的五个环节。
• 理解假设输出必须结构化（JSON 四字段）的原因。
• 说清该分工反幻觉的三条机理。
• 正确处理 REFUTED 结果（回喂而非丢弃）。
• 了解 angr 官方 MCP 与本章闭环的关系。

一、从「模型下结论」到「模型提假设」

先看一个典型幻觉场景：把伪代码丢给大模型，问「口令是什么」，它有相当概率自信地给出一个错误答案——把比较常量当口令、进制换算出错、甚至编造一个「看起来像」的字符串。第 11.1 节会系统归纳幻觉三形态，这里先给结论：让生成式模型直接输出事实性断言，等于让最会讲故事的人做法官。

换一种问法，幻觉率立刻下降：不问「口令是什么」，而问「校验逻辑在哪、成功与失败各输出什么、输入多长」——这些是「读代码就能形成」的假设性判断，模型的阅读能力货真价实。假设的正确与否，交给约束求解器去判。一句话立好本章规矩：

# division.txt —— 分工的边界线
模型：读得快、猜得广、会讲故事 → 提假设
求解器：不会讲故事、只会判定 → 下结论
​

为什么结构化 JSON 是硬要求：散文式回答无法被程序消费，也无法被审计——「大概在 check 函数里」既不能填进脚本模板，也不能进证据链复盘。四字段（func、ok_str、bad_str、length）每个都直接对应脚本模板里的一个空位，缺一个就拒绝执行。

二、闭环架构：五个环节

# loop_arch.txt —— 假设验证闭环的五环节

  ① 反编译伪代码            ② LLM 提假设
  （第 01 章产出）   ────▶  只输出 JSON 四字段：
                           func / ok_str / bad_str / length
                                   │
  ⑤ 结论回填证据链                 ▼
  （第 11.1 节四列）      ③ 渲染 angr 脚本
        ▲                （复用 8.1 节模板）
        │                        │
        │                 ④ 隔离环境运行
        │                        │
        │        ┌─── found ──┬── avoid ──┬── 超时 ───┐
        └────────┘            └──失败输出回喂模型修正──┘
​

五个环节各有纪律：①伪代码要带函数名与字符串引用，删掉无关函数减少干扰；②假设必须是结构化 JSON，禁止模型输出散文式结论——结构化才能被程序消费，也才能被审计；③脚本由模板渲染而非模型自由生成，模型只填空，不写代码——这是把「生成自由度」压到最小的关键设计；④运行在隔离沙箱，超时兜底；⑤三种结果都回填：found 是正结论，avoid 与超时是负结论，负结论回喂模型改假设再来一轮。

三、最小实现骨架

# hypothesis_loop.py —— LLM 提假设、angr 验证的最小闭环骨架
import json

PROMPT = """你在协助分析一个自编译的口令校验程序。下面是主函数的反编译伪代码。
提出一个可被符号执行验证的假设，只输出 JSON，不要输出任何解释：
{{"func": "校验逻辑所在函数名", "ok_str": "成功输出串", "bad_str": "失败输出串", "length": 口令字节长度}}
伪代码：
{pseudocode}"""

TPL = """# gen_solve.py —— 由假设自动渲染的 angr 探索脚本
import angr
import claripy

proj = angr.Project("./crackme", auto_load_libs=False)
flag = claripy.BVS("flag", 8 * {length})
state = proj.factory.full_init_state(
    stdin=angr.SimFileStream(content=flag, name="stdin"))
simgr = proj.factory.simulation_manager(state)
simgr.explore(
    find=lambda s: b"{ok_str}" in s.posix.dumps(1),
    avoid=lambda s: b"{bad_str}" in s.posix.dumps(1))
if simgr.found:
    print("VERIFIED", simgr.found[0].solver.eval(flag, cast_to=bytes))
else:
    print("REFUTED")
"""

def build_hypothesis(pseudocode: str) -> dict:
    """调用你自己的模型入口，解析出假设 JSON；解析失败即整体失败，不猜"""
    raise NotImplementedError("接入任意本地或远端模型")

def main(pseudocode_path: str) -> None:
    pseudocode = open(pseudocode_path, encoding="utf-8").read()
    hyp = build_hypothesis(pseudocode)
    assert set(hyp) == {"func", "ok_str", "bad_str", "length"}
    with open("gen_solve.py", "w", encoding="utf-8") as f:
        f.write(TPL.format(**hyp))
    print(json.dumps(hyp, ensure_ascii=False, indent=2))
    # 下一步：在隔离环境运行 python gen_solve.py
    # VERIFIED → 结论由求解器背书，连同假设与输出写入证据链
    # REFUTED 或超时 → 把失败输出回喂模型，修正假设后重渲染
​

骨架里三处设计值得咀嚼：断言校验字段齐全，模型少给一个字段就拒绝执行，而不是程序替它编一个默认值；模板里 find 与 avoid 完全由假设字段填充，模型没有任何写代码的机会；VERIFIED 与 REFUTED 两个字符串是程序与外部世界的唯一接口——证据链只认这两个词（第 11.1 节）。

四、为什么这个分工反幻觉

三条机理，层层递进：

• 结论不可编造。最终报告里的每个字（口令、路径）都来自求解器输出，模型输出只出现在「假设」栏，性质从「事实断言」降级为「待验证猜想」。
• 错误可被系统捕获。假设错了的表现是 REFUTED 或超时，失败被闭环自然吞掉并转化为下一轮输入——错误假设的成本是一次脚本运行，而不是一个错误结论。
• 过程可审计。假设是 JSON、脚本是模板渲染、运行有输出——三个中间产物都是明文，事后复查（第 11.1 节的四列表）能把任何结论还原到「当时模型看到了什么」。

一次 REFUTED 迭代的实录形态（示意）：

# refuted_log.txt —— 假设被证伪后的一轮修正（示意）
第一轮假设：{"func": "main", "ok_str": "Success", "bad_str": "Fail", "length": 8}
运行输出：REFUTED（超时上限内无 found）
回喂提示：上轮假设失败。请重新阅读字符串表：成功输出究竟是什么？
第二轮假设：{"func": "check", "ok_str": "Access granted", "bad_str": "Denied", "length": 16}
运行输出：VERIFIED b'AI4RE_2026'
​

注意第二轮改了三处：函数定位、两个输出串、长度——模型从失败里学到的是「字符串要按原文」，这类修正模式本身就是提示词迭代的素材。

这套思路与开源社区 reverify 项目（约 1.3k stars，2026-10 社区口径）的理念同构：AI 提出假设、确定性工具验证的反幻觉框架。本书不依赖该项目，但理念归属要说清楚。

五、angr 官方 MCP：闭环的工业化形态

逐段手工串联闭环适合学习，生产形态是工具化：angr 官方提供 MCP server，把反编译、CFG、交叉引用等能力暴露为模型可调用的工具——模型在会话里先查函数清单、读目标函数反编译，再触发符号执行，全程不需要人写模板。这与第 03 章《GhidraMCP实战》的思路同构：把专业工具变成模型的手脚；也呼应第 05 章《REA聚合层》：多个 MCP 工具在聚合层之下各自独立、之上统一编排。工具能力清单与版本以 angr 官方文档为准。

值得提醒的是接法差异：MCP 形态下模型「自己决定」下一步调用什么工具，自由度高于本章的固定模板。两者并不矛盾——关键路径（最终下结论的那一步）仍然必须是确定性工具的输出，MCP 只是让「提假设」之前的侦察步骤更顺畅。这条原则在第 11.1 节会升格为团队纪律。

本节要点回顾

• 闭环五环节：伪代码、结构化假设、模板渲染、沙箱运行、结果回填。
• 三条反幻觉机理：结论不可编造、错误可被捕获、过程可审计。
• 失败假设是信息不是事故：REFUTED 回喂模型构成迭代，修正模式是提示词素材。
• angr 官方 MCP 是闭环的工业化形态，理念与 reverify 同源；下结论环节不因 MCP 而松绑。

求解器说 found，只能说「存在一条可行的路径与输入」；真实程序在真实操作系统里跑起来什么样、寄存器里到底是什么值，还要到调试器面前见分晓。下一节请出 pwndbg，把闭环的最后一环「动态复核」补上。