MarinJursic/patchproof-verification

# PatchProof **针对人类和 AI 生成补丁的对抗性软件验证。** [](https://marinjursic.github.io/patchproof-verification/) [](https://github.com/MarinJursic/patchproof-verification/actions/workflows/pages.yml) PatchProof 不仅询问现有测试是否通过。它会询问是否能构造出一个使补丁违反不变式的输入——并且只有在拥有可执行证据时才报告缺陷。  ## 功能展示 最简明的实用演练如下： 1. 阅读红/绿 diff：识别区域的 `toLocaleLowerCase(locale)` 被替换 为与区域无关的 `toLowerCase()`。 2. 选择 **Replay verification** 以确定性顺序展示每个阶段。 3. 沿着证明图，从三个标记的 demo 固定数据到可执行 的属性、收缩和差分检查。 4. 检查最小化的反例：参考实现在 `tr-TR` 下对 `["İ", "i"]` 返回 `true`；而补丁返回 `false`。 5. 在页眉处在 **Light** 和 **Dark** 之间切换。该偏好设置会在 设备上持久化保存，并在首次使用时默认采用操作系统偏好。 6. 使用指针或左/右箭头键打开 **Confidence report**。其 评分描述的是证据质量，而不是补丁正确的概率。 该截图刻意保留了正在运行的产品原貌，而非合成的 模型图。该应用是响应式的，支持减弱动态效果偏好，保留了 可见的键盘焦点，并通过 ARIA 标签和实时区域暴露其状态。 ## 本项目为何存在 一个全绿的测试套件只能证明该套件中已编码的测试用例通过了。PatchProof 协调额外的验证策略，跟踪每个策略实际确立了什么，并明确报告在执行预算之外还剩下什么。 包含的场景模拟了一个真实的回归： ``` - return a.toLocaleLowerCase(locale) === b.toLocaleLowerCase(locale) + return a.toLowerCase() === b.toLowerCase() ``` 所有原始测试均通过。一个变异引导的属性探测器会针对被移除的区域设置分支，发现一个土耳其语大小写映射差异，并进行最小化： ``` ["İSTANBUL PORTAL", "istanbul portal"] → 14 accepted reductions, all preserving the failure → ["İ", "i"] reference implementation (tr-TR): true patched implementation: false ``` 其结果是一个生成的回归测试和一个 **request changes** 建议——而不是猜测性的模型意见。 ## 已实现的功能 - 一个响应式的 Next.js/TypeScript 验证控制台，包含： - 补丁 diff 和原始测试状态； - 确定性的 worker 动画； - 带有通过、警告和失败分支的证明图； - 生成的属性失败和收缩追踪； - 旧/补丁后执行对比； - 证据置信度、已验证属性、未验证行为、生成的测试、性能差异、API 兼容性和建议； - 键盘可访问的标签页、可见焦点、减弱动态效果支持，以及带有本地持久化的 无障碍明/暗主题切换。 - 一个强类型的 Python/FastAPI 验证器，包含： - 源自每个请求字段的内容寻址作业 ID； - 确定性的时间戳、随机种子、语料库、执行预算和报告； - 变异引导的输入排序； - 属性评估； - 配对的 delta-debugging、字符删除，以及可重放的收缩追踪； - 差分参考/补丁后执行； - 类型化的报告和内存中的作业查询 API。 - 一个本地 `patchproof` CLI，支持人类可读和 JSON 输出。 - 一个可运行的 GitHub 集成，包含： - 一个仓库本地的 composite Action 以及 pull-request/workflow-dispatch 检查； - 无需凭证的 Checks API payload 和作业摘要生成； - 可选的 token 认证检查发布，无需检入凭证； - 一个 FastAPI payload 预览端点和一个经过测试的框架中立适配器。 - 一个打包的 VS Code 扩展，包含三个命令、工作区信任处理、 无需 shell 的验证器执行、超时/输出限制、诊断，以及完整的 输出通道报告。 - 前端源码测试、Python 单元/API/CLI 测试，以及一键式验证脚本。 ## 架构 ``` flowchart LR A["Patch intake
diff · refs · locale"] --> B["FastAPI orchestrator
typed job · seed · budget"] B --> C["Existing tests
(fixture evidence)"] B --> D["Type/API contract
(fixture evidence)"] B --> E["Mutation probe
surviving locale mutant"] E --> F["Property corpus
guided Unicode cases"] F --> G["Differential execution
reference vs patch"] G --> H["Counterexample minimizer
paired delta debugging"] C --> I["Verification report"] D --> I H --> I I --> J["Web proof graph"] I --> K["CLI / JSON"] I --> L["GitHub Action / Check Run"] I --> M["Packaged VS Code extension"] ``` Web UI 和 Python 服务刻意共享相同的理念报告结构。UI 的置信度评分描述的是**证据质量**，而不是补丁正确的概率。PatchProof 并不宣称进行了详尽的形式化验证。 ## 快速开始 前置条件： - Node.js 22.13 或更高版本 - Python 3.11 或更高版本 ### Web 应用 ``` npm install npm run dev ``` 打开 `http://localhost:3000`，然后选择 **Replay verification**。 生产环境检查： ``` npm run build npm test npm run lint npm run typecheck ``` ### Python 验证器和 CLI ``` python3 -m venv python/.venv python/.venv/bin/pip install -e "python[dev]" python/.venv/bin/patchproof demo ``` 机器可读报告： ``` python/.venv/bin/patchproof demo --format json ``` 发现问题时以非零退出码退出（CI 风格）： ``` python/.venv/bin/patchproof demo --fail-on-finding # 打印 executable finding 后 exit 2 ``` ### GitHub Check 在没有网络访问的情况下生成完整的 Checks API 请求： ``` GITHUB_REPOSITORY=owner/repository \ GITHUB_SHA="$(git rev-parse HEAD)" \ python/.venv/bin/patchproof github-check ``` 已检入的 [composite Action](./.github/actions/patchproof/action.yml) 和 [workflow](./.github/workflows/patchproof.yml) 运行相同的证据路径，并 编写 GitHub 作业摘要。工作流运行本身作为一个仓库 检查可见。当选择 `post_check` 时，`workflow_dispatch` 还可以 额外发布一个单独的 Check Run。 已检入的 pull-request 工作流是一个 **integration smoke check**（集成冒烟检查）：它 证明了 CLI、报告和 GitHub 呈现能在 GitHub runner 上执行。 它不分析 pull request 的 diff。由于内置场景 包含已知的回归，因此选择启用 `post_check` 会刻意创建一个 状态为 `failure` 结论的单独 Check Run。 发布是可选的，并且仅从环境中读取 token： ``` export GITHUB_TOKEN="token with checks:write" python/.venv/bin/patchproof github-check \ --repository owner/repository \ --sha "$(git rev-parse HEAD)" \ --post ``` 不要将 token 放置在命令参数或配置文件中。GitHub Enterprise 用户可以设置 HTTPS `GITHUB_API_URL`。请参阅 GitHub 官方的 [工作流权限参考](https://docs.github.com/en/actions/reference/workflows-and-actions/workflow-syntax#permissions) 和 [Check Runs API](https://docs.github.com/en/rest/checks/runs)。 ### VS Code 扩展 构建并检查可安装的 VSIX： ``` npm run package:vscode unzip -t integrations/vscode-extension/dist/patchproof-vscode-0.1.0.vsix code --install-extension \ integrations/vscode-extension/dist/patchproof-vscode-0.1.0.vsix ``` 如上所述安装 Python CLI，打开此工作区，然后运行 **PatchProof: Run Deterministic Demo**。该扩展会自动检测 项目本地的虚拟环境；`patchproof.executable` 可覆盖它。 启动进程需要工作区信任。该进程在没有 shell 的情况下运行， 在配置的超时时间被终止，并且输出不能超过 1 MiB。 这些控制遵循 VS Code 官方的 [工作区信任扩展指南](https://code.visualstudio.com/api/extension-guides/workspace-trust)； 该包是使用官方文档记载的 [`vsce package` 工作流](https://code.visualstudio.com/api/working-with-extensions/publishing-extension) 生成的。 运行所有检查： ``` ./scripts/verify-all.sh ``` ## API 启动服务： ``` python/.venv/bin/uvicorn patchproof.api:app --app-dir python/src --reload ``` 交互式 OpenAPI 文档位于 `http://127.0.0.1:8000/docs`。 ### 提交验证作业 ``` curl -s http://127.0.0.1:8000/v1/verify \ -H 'content-type: application/json' \ -d '{ "repository": "demo/search-service", "base_ref": "main", "patch_ref": "8f29d1a", "patch": "demo://unicode-locale-regression", "locale": "tr-TR", "seed": 20260725, "max_examples": 64 }' ``` MVP 同步执行并返回已完成的 `JobEnvelope`。使用以下命令检索同一个内存中作业： ``` curl -s http://127.0.0.1:8000/v1/jobs/pp_496349FCE8 ``` 端点： | 方法 | 路径 | 目的 | |---|---|---| | `GET` | `/health` | 存活探针 | | `POST` | `/v1/verify` | 验证输入并执行类型化的验证作业 | | `GET` | `/v1/jobs/{id}` | 检索在此进程中创建的报告 | | `POST` | `/v1/integrations/github/check-payload` | 构建无需凭证的 GitHub Checks API payload | ## 流水线详情 1. **Baseline evidence** 记录 demo 仓库的原始测试和类型契约结果。 2. **Mutation probe** 观察到用通用的 `lower()` 替换区域感知折叠后，仍能通过原始测试套件。 3. **Mutation guidance** 将带点/不带点 I 对移动到确定性 Unicode 语料库的前面。 4. **Property execution** 评估契约：在声明的区域设置下相等的值必须保持相等。 5. **Differential execution** 要求参考实现满足契约，而补丁违反该契约。 6. **Minimization** 删除配对后缀，然后删除单个码位，同时重放相同的可执行谓词。报告保留了全部 15 个状态（原始状态加上 14 个接受的缩减），而不仅仅是最终对。 7. **Reporting** 包含证明、差距、生成的回归测试、兼容性/性能固定数据，以及具体的下一步操作。 作业 ID 对整个已验证请求的规范化序列化进行哈希处理，因此基础参考、补丁参考、区域设置、随机种子、预算、仓库或补丁不同的请求不会互相默默覆盖。固定的随机种子会影响作业标识和时间戳；语料库排序和收缩是确定性的。重复相同的请求会产生字节等价的 Pydantic 模型。 ### 证据分类 PatchProof 区分可执行发现和 demo 固定数据： | 产品设计中的策略 | MVP 状态 | 本仓库中的证据 | |---|---|---| | 现有单元/集成测试 | 固定数据 | 类型化检查记录内置 demo 仓库的 `214 / 214` 基准；PatchProof 不宣称执行外部仓库 | | 测试用例增强 | 可执行输出 | 最小化的对将作为语法有效的 pytest 回归测试输出 | | 属性/蜕变测试 | 可执行 | 在确定性、变异引导的 Unicode 语料库上评估区域等价性蕴涵 | | 变异测试 | 固定数据 + 可执行引导 | 存活的移除区域设置变异体是固定数据；其引导改变了语料库排序并到达了可执行属性 | | 模糊测试 | 确定性语料库 MVP | 有边界的 Unicode 案例以稳定顺序执行；这不是覆盖引导的模糊测试 | | 差分执行 | 可执行 | 参考和打补丁的函数在相同的最小化输入上运行 | | 反例最小化 | 可执行 | 每个接受的缩减都会被保留，并针对分歧谓词重新检查 | | 类型/静态/API 兼容性 | 固定数据 | 类型化报告字段明确标记未更改的 demo 签名；未调用外部检查器 | | 复杂度/性能 | 固定数据 | `−3.1%` 数值被标记为确定性固定数据，不得用作仓库基准证据 | | 资源泄漏和竞态调度 | 未验证 | 作为差距而不是通过报告 | | 有状态的基于模型的测试 | 未实现 | 未来的沙箱 runner 可以在不更改报告消费者的情况下添加此项 | 内置运行不需要 LLM。不会仅仅因为模型提出了建议就接受任何发现。 ## 生成的回归测试 ``` def test_equal_folded_tr_tr_counterexample(): assert equal_folded("İ", "i", locale="tr-TR") is True ``` ## 集成 ### GitHub `patchproof.github_check` 将完整的审查数据包——置信度、已验证 属性、显式差距、生成的测试、反例、性能、 兼容性和建议——映射到 Checks API 正文。CLI 默认为 无需凭证的 dry run。`--post` 需要 `GITHUB_TOKEN`，验证 HTTPS API 来源，发送 15 秒请求，并且从不将 token 序列化到 报告中。发布过程使用模拟的 opener 进行覆盖；测试从不调用 GitHub。 该 composite Action 将 Python 包安装到隔离的 runner 环境中，在 `RUNNER_TEMP` 下写入 JSON，并将 Markdown 摘要附加到 `GITHUB_STEP_SUMMARY`。包含的工作流使用 `pull_request` 而不是 `pull_request_target`，从而防止在特权基础仓库 上下文中执行。其结果是本仓库的真实 Actions 检查。 这不构成已注册的 webhook GitHub App。可分发的 App 仍然需要 GitHub 注册、安装流程、webhook 密钥、 送达验证、检入沙箱化和持久作业存储。这些 凭证和外部资源是刻意缺失的。 ### VS Code `integrations/vscode-adapter.ts` 仍然是可测试的、与宿主无关的边界。 `integrations/vscode-extension/` 是具体的宿主：它捆绑该适配器， 注册命令，启动 CLI，将反例映射到 `DiagnosticCollection`，并将 JSON 报告保留在 `LogOutputChannel` 中。 该 VSIX 不包含凭证、遥测、网络客户端或更新 机制。它可以在本地安装，但未发布到 VS Code Marketplace。 ## 验证 项目的本地验证命令涵盖： | 范围 | 检查 | |---|---| | 前端 | vinext/兼容 Cloudflare 的生产构建 | | 前端 | Node 源码/元数据测试 | | GitHub | Payload、作业摘要、dry-run CLI、缺失 token、安全来源、模拟 POST、API、Action/workflow 契约测试 | | VS Code | 严格的扩展类型检查、esbuild 打包、VSIX 打包、归档完整性、清单和安全控制测试 | | 前端 | ESLint | | 前端 | TypeScript 严格类型检查 | | 引擎 | Unicode 参考和打补丁的行为 | | 引擎 | 确定性 14 步最小化至 `["İ", "i"]`，每个追踪条目都经过重新检查| Orchestrator | 完整且可重复的报告 | | API | 健康、提交、检索、GitHub payload、404、无效预算、未知字段和不支持的补丁路径 | | CLI | JSON、人类可读摘要、GitHub dry-run/摘要/发布失败、无定论运行、无效输入和退出代码契约 | | 冒烟测试 | `json.tool` 解析的 CLI 报告 | Web 控制台是内置报告的确定性呈现，而 不是 API 客户端。其重放控制会重置证明图并 按顺序揭示所有六个阶段。Python 服务仍然是权威的 可执行引擎。前三个 Web 阶段被明确标记为 `FIXTURE`；属性、 最小化和行为差异阶段被标记为 `EXECUTABLE`。 ## 范围与限制 这是一个作品集质量、可本地执行的 MVP，不是安全的任意代码执行服务。 - 包含的验证器仅接受 `demo://unicode-locale-regression` 并拒绝带有 HTTP `422` 的不受支持的补丁 payload。它**不会**克隆或运行不受信任的仓库。 - 现有测试、类型、性能和 API 兼容性结果是显式的 demo 固定数据；Unicode 属性、差分结果、最小化器、API 和 CLI 是可执行的。 - 作业是同步的，并存储在进程内存中。 - 没有身份验证、数据库、队列、容器沙箱、已注册的 webhook GitHub App 或发布到 Marketplace 的 VS Code 扩展。本地的 Action/检查发布者和可安装的 VSIX 是可执行的。 - 属性语料库是确定性的且专门构建的；生产环境应为 Hypothesis、模糊测试器、变异工具、类型检查器、性能分析器和密封测试运行器添加适配器。 - Unicode 无大小写匹配依赖于领域。此 demo 模拟一个显式的 `tr-TR` 应用程序契约；它不是一个通用的身份算法。 - “未找到反例”仅意味着“在此策略和预算内未找到”。 对于生产环境，请在临时的、禁用网络的沙箱中隔离每次检出；锁定工具链和依赖项锁定文件；验证仓库和 webhook 身份；隐去敏感信息；限制 CPU、内存、进程数、输出和执行时间；并持久化内容寻址的证据。 ## 研究基础 PatchProof 基于执行优先验证： - [SWE-bench](https://www.swebench.com/SWE-bench/) 通过将补丁应用到 真实仓库并在可重现的容器化环境中运行测试来评估 它们；[SWE-bench Verified](https://www.swebench.com/verified.html) 是一个经过人工验证的 500 实例子集。 - [SWE-smith](https://arxiv.org/abs/2504.21798) 描述了可执行软件工程任务数据的可扩展构建。 - [Hypothesis](https://hypothesis.readthedocs.io/en/latest/reference/api.html#hypothesis.Phase) 记录了分离的生成、重用、定位和收缩阶段。 PatchProof 镜像了执行和收缩的形状，但使用了一个小得多的、 专门构建的确定性语料库；它不嵌入 Hypothesis。 - [mutmut](https://mutmut.readthedocs.io/en/latest/) 将变异测试描述 为更改代码并检查测试套件是否注意到。PatchProof 的 “mutation probe”明确是一个固定数据加上输入排序提示，而不是真正的 mutmut 执行。 - Zeller 和 Hildebrandt 最初的 [delta debugging 论文](https://www.st.cs.uni-saarland.de/papers/tse2002/tse2002.pdf) 推动了导致失败的输入的系统性缩减。 - Unicode 规范性的 [SpecialCasing 数据](https://www.unicode.org/Public/UCD/latest/ucd/SpecialCasing.txt) 记录了上下文和语言敏感的映射，包括土耳其语带点和不带点的 I。 - [FastAPI 请求模型](https://fastapi.tiangolo.com/tutorial/body/) 提供了运行时验证和基于 Pydantic 类型的 OpenAPI schema 生成。 ## 仓库结构图 ``` app/ Next.js verification console .github/actions/patchproof/ Repository-local composite GitHub Action .github/workflows/ Pull-request and manual integration check integrations/github-check.ts TypeScript Checks API adapter integrations/vscode-adapter.ts Editor-independent diagnostic boundary integrations/vscode-extension/ Buildable, packaged VS Code extension public/demo/ README preview asset python/src/patchproof/ FastAPI, CLI, engines, GitHub publisher python/tests/ Engine, API, integration, and CLI tests scripts/verify-all.sh Complete local verification tests/ Frontend and integration source tests ``` ## 许可证 MIT — 请参阅 [`LICENSE`](./LICENSE)。

标签：pocsuite3, 形式化验证, 补丁验证, 软件测试, 逆向工具