nickharris808/certkit

# certkit [](https://github.com/nickharris808/certkit/actions/workflows/ci.yml) [](https://www.python.org/) [](#install) [](LICENSE) [](pyproject.toml) **一种用于机器可检查程序准入的证书格式，以及一个独立的检查器。** 该检查器不引入任何 Python 标准库之外的内容。没有求解器，没有搜索，也没有 浮点运算。它只需一个下午就能通读，这正是其核心意义所在：为了相信一个证明，你 不需要去信任*生成*该证明的工具。 ``` pip install "certkit@git+https://github.com/nickharris808/certkit@main" ``` ## 30秒快速入门 该示例内置在包中，因此在 `pip install` 后可直接运行——无需检出仓库， 也无需创建任何文件： ``` certkit demo ``` ``` certkit demo -- CVE-2014-0160 (Heartbleed) shape claim: guard `19 + payload <= record_len` implies `3 + payload <= record_len` for payload in [0, 65535] valid certificate -> ACCEPTED obligation 0: ok forged certificate -> REFUSED obligation 0: FAIL -- non-strict combination needs const > 0, got -65535 As expected: the real certificate checks out and the forgery does not. ``` 要检查你自己的文件： ``` certkit check --spec my.spec.json --cert my.cert.json ``` **初次接触？** [`TUTORIAL.md`](TUTORIAL.md) 将在大约十五分钟内，带你从一个真实的 C 边界检查一路走到 CI 门禁—— 包括当 guard 错误时会是什么样子。 ## CLI 参考 ``` certkit {check,explain,init,sos,demo} ``` | 命令 | 作用 | |---|---| | `certkit demo` | 运行内置的 Heartbleed 示例：一个有效证书，一个伪造证书。无需任何文件。 | | `certkit init` | 根据编写的关系搭建一个 spec，因此你永远不需要手写 JSON 原子。 | | `certkit check` | 判定一个 spec/证书对。这是 CI 会运行的命令。 | | `certkit explain` | 打印反驳算术过程——涉及哪些原子、哪些权重、什么相互抵消了。 | | `certkit sos` | 检查一个有理数的平方和证书。 | | `certkit schema` | 打印格式的 JSON Schema，以便其他工具可以生成它。 | | `certkit export` | 将每项义务以 SMT-LIB 2 格式输出，供 z3 / cvc5 / 或其他任何工具使用。 | | `certkit import` | 将 SMT-LIB 2 脚本读取回 spec 中（线性整数片段）。 | | `certkit lsp` | 一个语言服务器：在你输入时，于编辑器中提供针对 spec 文件的诊断。 | ### `certkit init` ``` certkit init \ --domain "0 <= payload" --domain "payload <= 65535" \ --guard "19 + payload <= record_len" \ --safety "3 + payload <= record_len" \ --name heartbleed -o heartbleed.spec.json ``` | 标志 | 含义 | |---|---| | `--domain RELATION` | 对攻击者输入的约束。可重复使用。 | | `--guard RELATION` | 你的代码执行的检查。可重复使用。 | | `--safety RELATION` | 必须成立的属性。可重复使用；每项对应一个义务。 | | `--name`, `-o/--out` | Spec 名称；输出路径（如省略则输出到 stdout）。 | 接受 `<=`、`<`、`>=`、`>`，带 `*` 的整数系数，以及 `+`/`-`。拒绝 `==`（因为它包含两个 原子——请将两者都写出）、链式比较以及任何非线性内容，而不是进行猜测。解析上述 关系可以逐字节地重现手写的内置 spec，包括其指纹。 ### `certkit check` | 标志 | 含义 | |---|---| | `--spec`, `--cert` | 要检查的配对。必填。 | | `--no-fingerprint` | 跳过绑定检查。永远只能得出 `UNVERIFIED` 结果（退出码 3），绝不会是 `ACCEPTED`。 | | `--json` | `--format json` 的简写。 | | `--format` | `text`、`json`、`sarif`、`junit` 或 `markdown`。见下文。 | ### 输出格式 ``` certkit check --spec my.spec.json --cert my.cert.json --format sarif > certkit.sarif ``` | 格式 | 用途 | |---|---| | `text` | 终端 | | `json` | 脚本；报告原文，包括 `verdict` 和 `binding_verified` | | `sarif` | GitHub 代码扫描——拒绝将成为 PR 上的一个警报 | | `junit` | 大多数 CI 系统会原生渲染此格式 | | `markdown` | PR 评论或作业摘要 | 更改格式永远不会更改判定结果或退出码。`UNVERIFIED` 在每种格式中都有其 独立的级别——SARIF 规则 `certkit/unverified`，类型为 `unverified` 的 JUnit 失败——因为 如果一种格式将其渲染为通过，就会违背存在第三种判定结果的初衷。 ### 与求解器交互 (SMT-LIB 2) `certkit export` 将义务 `domain AND guard AND NOT(safety[i])` 编写为 SMT-LIB 脚本： ``` certkit export --spec heartbleed.spec.json -o obligation.smt2 z3 obligation.smt2 # unsat cvc5 obligation.smt2 # unsat ``` `unsat` 与 `ACCEPTED` 证书所做的声明相同，但这是由完全独立的 实现得出的。`sat` 意味着 guard 确实允许了禁止的状态，而该 model 就是你的 反例。两个方向都在一系列 guard/safety 配对上进行了交叉检查——如果 certkit 曾经接受了求解器判定为 `sat` 的内容，该测试就会失败。CI 在每次 推送时都会针对 **z3** 运行此操作，如果不存在求解器则会失败，因此检查不会降级为静默跳过；在安装了 第二个求解器 (**cvc5**) 的地方也会使用它，并且两者的结果必须一致。 另一个方向的导入被刻意设计为部分的： ``` certkit import --smtlib theirs.smt2 -o spec.json ``` certkit 处理无量词的**线性整数**算术。其他任何内容——非线性乘积、 `Real` 或 `BitVec` sort、未解释的函数、量词、等式——都会在指出具体构造名称后被拒绝， 而不是被丢弃： ``` error: sort 'Real' for 'x': certkit handles Int only (no Real, Bool, or BitVec) error: nonlinear multiplication: certkit handles linear arithmetic only error: an equality is two atoms; assert the two inequalities you mean instead ``` 一个静默忽略其不理解内容的部分导入器，将会生成一个证明了比文件内容 *更弱*结论的 spec，然后下游的所有内容都会针对错误的定理得出正确的 结论。拒绝是唯一安全的行为。 还要注意的是，SMT-LIB 文件不包含哪些关系是假设、哪个关系是检查的概念，因此 **每个断言都会成为一个 safety 联合子句**，你需要自行将它们移动到 `domain` 和 `guard` 中。这是一个建模决策；猜测它会改变被证明的内容。 ### 在你的编辑器中 ``` certkit lsp # speaks LSP over stdio; standard library only, no pygls ``` 将任何编辑器的 LSP 客户端指向它以处理 `*.spec.json`，你就可以在编写 guard 时获得诊断信息，而不是在 CI 阻止你合并之后。它报告三件事：spec 中的结构性问题、 检查相邻的 `*.cert.json` 的判定结果，以及 guard 使用了但 domain 从未对其进行约束的变量。 最后一条是信息，而不是错误——一个无约束的变量会使声明变得*更强*（该 义务必须对其可能取的每一个值都成立），因此也更难证明，当你认为正确的 guard 无法验证时，这是 首先要检查的事情。该服务器内部不包含任何生成器，因此它永远不会主动提出“修复” guard，也 永远不会告诉你某个 guard 是正确的：没有诊断信息意味着在*文件*中没有发现任何 错误。 ### 在 notebook 中 `CheckReport` 会在 Jupyter 中自我渲染——三种判定，三种颜色，并且 `UNVERIFIED` 会保持其 独立性，而不是被并入通过或失败中。`exploit-counter` 的 `Decision` 和 `OverAcceptance` 以及 `crs-mcp` 的 `Verdict` 也是如此。Notebook 是最容易被浏览而不是被仔细阅读结果的地方，因此 看起来像通过的弃权在那里会造成最大的损害。 ### 作为 pre-commit hook ``` repos: - repo: https://github.com/nickharris808/certkit rev: main hooks: - id: certkit ``` 每个暂存的 `*.cert.json` 都会根据其相邻的 `*.spec.json` 进行检查。没有 相邻 spec 的证书会**失败**，而不是被跳过——一个静默跳过其无法 检查的内容的门禁，在什么都没验证的情况下却报告“所有证书均已验证”。`UNVERIFIED` 也会阻止提交： 在门禁中，“拒绝认证”和“驳回”具有相同的后果。 `ci-templates/` 为 GitLab CI 和 CircleCI 提供了相同的作业，两者都输出了其 UI 可原生渲染的 JUnit。 ### 从你自己的工具中生成 certkit ``` certkit schema --format certkit/spec/v1 > spec.schema.json ``` 这两种格式都有已发布的 JSON Schema，内置于 wheel 中，并在 CI 中针对 每个内置示例和 200 个生成的 spec 进行了验证。`SPEC.md` 向人们解释了该格式；而 schema 则向程序解释它。 ``` from certkit.schemas import load_schema, schema_for load_schema("certkit/farkas/v1") # by format id schema_for(my_document) # by the document's own `schema` field ``` 根据它们进行验证需要 JSON Schema 库，这是这里的开发依赖项—— `certkit` 本身仍然不引入任何标准库之外的内容。 ### `certkit explain` 接受相同的 `--spec` 和 `--cert`。打印算术过程并**以与 `check` 相同的状态退出**， 因此将其放入脚本中并不会将拒绝洗白为成功。 ``` [2] payload - record_len + 19 <= 0 [3] -payload + record_len - 3 < 0 Multiply each atom by its nonnegative weight and add: 1 * [2] (payload - record_len + 19 <= 0) 1 * [3] (-payload + record_len - 3 < 0) Every variable cancels: payload, record_len all sum to 0. What remains is: 16 < 0 ``` ## 三种判定，以及为什么有三种 | 判定 | 退出码 | 含义 | |---|---|---| | `ACCEPTED` | 0 | 每个义务都被反驳，**并且**证书绑定到了此 spec。 | | `REFUSED` | 1 | 至少有一个义务未被反驳，或者输入格式错误。 | | `UNVERIFIED` | 3 | 算术检查通过，但所需的前置条件从未建立。**不是通过。** | `UNVERIFIED` 的存在是因为 `--no-fingerprint`。该标志跳过了将证书绑定到 spec 的检查——这在编写期间、指纹尚未计算时很有用。但是，从未与 此 spec 绑定的证书并没有被证明*关于*此 spec 说明了任何内容，因此 将其报告为接受，就意味着对检查器未完全验证的输入给予了通过。现在它会报告 `UNVERIFIED` 并以状态码 3 退出，原因行会用原话说明 `TRUST ANCHOR ABSENT`。 在 API 中，相同的区别是两个独立的布尔值，因为它们会分别失败： ``` report = check_certificate(spec, cert, require_fingerprint=False) report.obligations_ok # True -- the multipliers really do refute the obligation report.binding_verified # False -- but nothing ties this certificate to this spec report.ok # False -- so the overall answer is no report.verdict # 'UNVERIFIED' ``` 拒绝意味着*未获证明*——绝不意味着*被证伪*。`UNVERIFIED` 也是如此。 ## 工作示例 内置的示例是 CVE-2014-0160 (Heartbleed) 的形式。该声明指出 guard `19 + payload <= record_len` 蕴含了对于 `[0, 65535]` 中的每一个 payload，原始访问边界为 `3 + payload <= record_len`。 ``` from certkit import atom, make_spec, check_certificate domain = [atom({"payload": -1}), atom({"payload": 1}, -65535)] # 0 <= payload <= 65535 guard = [atom({"payload": 1, "record_len": -1}, 19)] # 19 + payload <= record_len safety = [atom({"payload": 1, "record_len": -1}, 3)] # 3 + payload <= record_len spec = make_spec(domain, guard, safety, name="heartbleed") cert = { "schema": "certkit/farkas/v1", "spec_fingerprint": spec["fingerprint"], "obligations": [{"multipliers": {"2": 1, "3": 1}}], } report = check_certificate(spec, cert) assert report # truthy when every obligation is refuted ``` 那些乘数构成了整个证明。原子 2 是 guard (`payload - record_len + 19 <= 0`)， 而原子 3 是取反的安全属性 (`-payload + record_len - 3 < 0`)。分别以权重 1 将它们相加：每个变量都会抵消，剩下 `16 < 0`，这是荒谬的——因此不存在反例。 ## 工作原理 一个 **Farkas 证书**证明了线性原子合取式是不可满足的。它是一个 非负乘数向量，使得加权原子之和为矛盾：所有变量 相互抵消，剩下的常量是不可能的。 一句话概括其可靠性：如果每个 `L_i <= 0` 并且每个 `m_i >= 0`，那么 `sum(m_i * L_i) <= 0` 必然成立——因此，如果乘数使得变量相互抵消并留下一个正的常数， 则该方程组无解。 因为整数是有理数的子集，有理数不可行意味着整数 不可行。反之则不然，这正是为什么找不到证书 并不构成可满足性证明的原因。该检查器拒绝；它不证明否定命题。 寻找乘数是别人的问题。该包不包含任何搜索。这种不对称性 使得携带证明的验证变得有用——生产者可以任意聪明并且 完全不受信任，因为检查成本低廉且可审计。 ## 重构：为什么伪造的证书会失败 一个简单的检查器从证书中读取原子，并针对*这些* 原子验证乘数。这几乎毫无价值——一个携带了简单、无关的方程组以及对其的有效 反驳的证书会通过检查，但对你的程序却什么也没证明。 `certkit` 忽略证书携带的任何原子。它从独立提供的 spec 中重建 义务： ``` system := domain AND guard AND NOT(safety) ``` 并让证书仅提供乘数。此外，证书还通过 SHA-256 指纹绑定到 spec。 该指纹用于检测漂移和意外的不匹配。它**不能** 防御蓄意的伪造者，因为伪造者只需在编辑过的 spec 上重新计算它即可。可靠性最终 建立在人类已阅读过 spec 关系的基础上——它们是微小的整数不等式， 故意设计得足够小以便于阅读。我们宁愿直言不讳，也不愿暗示某种该机制无法提供的保证。 ## 平方和证书 对于非线性义务 `target(x) >= 0`，类似的证书是有理恒等式 `scale * target == sum(q_i^2)` 且 `scale > 0`： 0 进行缩放必须 保持有效性；按 0 缩放必定破坏有效性）以及 CLI 退出码契约。 ## 工具包的其余部分 | | | |---|---| | **[certkit](https://github.com/nickharris808/certkit)** | 证书格式和独立的检查器 | | **[exploit-counter](https://github.com/nickharris808/exploit-counter)** | 如果 guard 不可靠，确切地计算出有多少状态会逃脱 | | **[crs-mcp](https://github.com/nickharris808/crs-mcp)** | AI 编码代理通过 MCP 调用的判定接口 | | **[soundnessbench](https://github.com/nickharris808/soundnessbench)** | 对上述所有内容进行评分的基准测试 | | **[certkit-action](https://github.com/nickharris808/certkit-action)** | 在你的 CI 中运行检查 | | **[pytest-mutation-verified](https://github.com/nickharris808/pytest-mutation-verified)** | 证明你的回归测试确实会失败 | | **[cve-proof-corpus](https://huggingface.co/datasets/nickh007/cve-proof-corpus)** | 六个带有机器可检查证明的真实 CVE | | **[在浏览器中尝试](https://huggingface.co/spaces/nickh007/certkit-demo)** | 无需安装；观看伪造被拒绝 | ## 文档 | | | |---|---| | [`TUTORIAL.md`](TUTORIAL.md) | 从一个真实的 C 边界检查到 CI 门禁的端到端过程 | | [`SCOPE.md`](SCOPE.md) | 判定证明了什么，以及没有证明什么 | | [`TROUBLESHOOTING.md`](TROUBLESHOOTING.md) | 每个错误字符串，以及修复它的方法 | | [`SPEC.md`](SPEC.md) | 磁盘上的格式，用于从你自己的求解器生成它 | ## 封闭的核心 这些包是*检查*的一半。它们刻意不包含证明搜索，这正是保持其 小到足以审计的原因——这也意味着上游必须有东西来生成 证书。 对于整个机器字域上的义务，枚举无法扩展，并且需要不枚举的决策 程序：无求解器消解并生成可重放的证书。该 引擎、从反驳中推导出最小 guard 的修复合成器，以及推动它们的进化 搜索**不**在本仓库中，需付费商业使用。 这种分割是刻意且永久的。**检查器是免费的，并且将永远免费**——你无法独立验证的证书一文不值，因此对验证收费将违背此格式的初衷。 需要花钱的是大规模*生产*证书。 ## 许可证 Apache-2.0。允许复制正是其意义所在——这是一种我们希望被采用的格式，而不是护城河。 **[certified discovery](https://nickharris808.github.io/certified-discovery/)** 的一部分——建立在一个不对称性上的十个构件：检查证明成本低廉且可审计，因此生成证明的工具不需要被信任。

标签：Python, 云安全监控, 形式化验证, 无后门, 程序正确性证明, 逆向工具, 静态分析