nickharris808/certkit-js

# certkit-js [](https://github.com/nickharris808/certkit-js/actions/workflows/ci.yml) [](package.json) [](LICENSE) [](package.json) **[certkit](https://github.com/nickharris808/certkit) 证书的第二个独立检查器 —— 使用 JavaScript 编写，无依赖且无构建步骤。** 同一个检查器的两套独立编写的实现，比一套被仔细阅读过的实现更有价值。如果两者都接受某张证书，就意味着两个独立的程序达成了一致。如果它们出现分歧，说明其中必然有一个是错的 —— 而 CI 会指出这一点，因为 Python 包生成了此测试套件运行的测试向量。 此包中任何地方都不使用浮点数。每个量都是由一对 BigInt 表示的。证明检查器中的舍入误差不是精度上的麻烦事，而是一个 soundness 漏洞。 ## 30秒快速入门 ``` git clone https://github.com/nickharris808/certkit-js && cd certkit-js node bin/certkit-js.js check --spec examples/heartbleed.spec.json --cert examples/heartbleed.cert.json ``` ``` ACCEPTED heartbleed obligation 0: ok ``` 现在来破坏它 —— 伪造的证书随包一起提供： ``` node bin/certkit-js.js check --spec examples/heartbleed.spec.json --cert examples/heartbleed.forged.json; echo "exit $?" ``` ``` REFUSED heartbleed obligation 0: FAIL -- non-strict combination needs const > 0, got -65535 one or more obligations failed exit 1 ``` 这两个文件与 Python 包内的文件逐字节相同。同一张证书，由不同的实现、用不同的语言检查，得到了相同的结果。 ## 作为库使用 ``` import { checkCertificate } from './src/index.js'; const report = checkCertificate(spec, cert); report.verdict; // 'ACCEPTED' | 'REFUSED' | 'UNVERIFIED' report.ok; // false for anything but ACCEPTED ``` 在浏览器中，无需打包工具和服务器： ``` ``` ## 三种判定结果 | 判定 | 退出码 | 含义 | |---|---|---| | `ACCEPTED` | 0 | 所有义务都被反驳，**并且**该证书绑定到此 spec。 | | `REFUSED` | 1 | 至少有一个义务未被反驳。这**并不**证明 guard 是错的。 | | `UNVERIFIED` | 3 | 算术验证通过，但未确立所需的先决条件。 | `UNVERIFIED` 是最重要的判定。传入 `{ requireFingerprint: false }` 将跳过绑定检查 —— multipliers 可能无可挑剔，但没有确立此证书是为*当前* spec 签发的，因此结果永远不能为 `ACCEPTED`。一个在此处报告通过的检查器，回答的是一个它并未询问的问题。 ## 测试方式 ``` npm test ``` **784 项测试。**有趣的不是单元测试： - **246 个由 Python `certkit` 包生成的差分向量** —— spec/证书对，以及 Python 得出的判定。此实现必须对每一个都得出相同的判定，包括故意刁难的那些（负数 multipliers、零分母、越界索引、自带 atoms 的证书）。246 个中的 200 个是生成的扫描，因此覆盖范围不受限于我所能想到的用例。 - **246 个 canonical-JSON 和指纹向量。** spec 指纹是对 `json.dumps(spec, sort_keys=True, separators=(",", ":"))` 计算的 SHA-256 哈希。与 CPython 的输出哪怕有一处转义字符不同的序列化器，都会拒绝所有真实的证书 —— 因此 CPython 生成的确切字节串已被提交并用于比对，包括非 ASCII 名称和辅助平面字符。 - **FIPS 180-4 SHA-256 向量**，因为哈希摘要是在此内部实现的，而不是导入的。 `tools/generate_vectors.py --check` 会在 CI 中运行。如果任一实现的行为发生变化，构建将变红报错，而不是让测试向量变得陈旧失效。 ### 测试本身也经过了测试 对检查器应用了六处单行突变，以观察测试套件是否能察觉： | 突变 | 是否捕获? | |---|---| | 非严格分支接受 `const == 0` | ✅ （在添加了一个用例之后 —— 见下文） | | 允许负数 multipliers | ✅ （同上） | | 零权重被计为使用了 atom | ✅ （同上） | | `negate` 停止翻转严格性 | ✅ | | 绑定到不同 spec 的证书被接受 | ✅ | | `--no-fingerprint` 报告 `ACCEPTED` | ✅ | 这六处中有三处在首次运行时被**遗漏**。740 个通过的测试中，没有任何一个能区分“加权和恰好抵消为零”和“抵消为正值”—— 一个接受 `0 <= 0` 作为矛盾的、存在 soundness 漏洞的检查器原本会通过整个测试套件。正是因为这个原因，才有了 `nonstrict-const-zero`、`negative-weight-trap` 和 `zero-weight-on-strict-atom` 这些用例，现在这六处突变都能被捕获。一个从未被证明会失败的测试套件仅仅是一种声明，而不是证据。 ## 真实范围 **这是什么：** 针对有理数线性算术的 `certkit/farkas/v1` 证书检查器。它从 specification 重新推导每个义务，并据此验证提供的 multipliers，忽略证书中携带的任何内容。 **这不是什么：** - **不是生成器。** 它不负责寻找 multipliers。必须由其他东西 —— Python `certkit`、求解器、或你自己的工具 —— 来提供。 - **不是判定过程。** `REFUSED` 的意思是“未被这些 multipliers 证明”，绝不代表“guard 不 sound”。未能找到证明并不等于证伪。 - **不是机器字长算术。** Atoms 是基于数学整数/有理数的关系。在这里通过的证明，对于你的 C 代码在溢出时的行为毫无意义。这属于建模的责任，也是在持有有效证书时依然可能出错的最常见原因。 - **不能替代阅读 spec。** 指纹可以检测偏移和意外，但防不住蓄意的伪造者，因为他们完全可以重新计算它。Soundness 建立在人类已经阅读过这些关系的基础之上 —— 它们足够小以至于易于阅读，这正是设计的全部核心。 有关更长版本的说明，请参见 [`SCOPE.md`](SCOPE.md)。 ## 与 Python 包的关系 | | [`certkit`](https://github.com/nickharris808/certkit) (Python) | `certkit-js` | |---|---|---| | 检查 `certkit/farkas/v1` | ✅ | ✅ | | 检查平方和（sum-of-squares）证书 | ✅ | ❌ | | 从书面关系生成 spec (`certkit init`) | ✅ | ❌ | | SMT-LIB 导入/导出 | ✅ | ❌ | | SARIF / JUnit / markdown 输出 | ✅ | ❌ (JSON 和文本) | | 在浏览器中运行 | 通过 Pyodide | 原生支持 | 两者的格式完全相同，并且指纹逐字节一致，因此在工具链中任何地方生成的证书都可以在两者中通过验证。 ## 安装 尚未发布到 npm —— 包元数据已完整，并且 `npm pack` 可生成有效的 tarball，但发布需要账号所有者执行一次浏览器操作（见 `PUBLISHING.md`）。在此之前： ``` npm install github:nickharris808/certkit-js ``` ## 许可证 Apache-2.0。 **[certified discovery](https://nickharris808.github.io/certified-discovery/)** 的一部分 —— 建立在一种不对称性之上的十项成果：检查证明成本低廉且可审计，因此不需要信任生成它的东西。

标签：BigInt, CMS安全, JavaScript, MITM代理, 形式化验证, 数据可视化, 校验工具, 自定义脚本, 证书验证, 零依赖