# FIBEMATE 当前状态：已验证的数字，与没做完的部分

> 2026-10-25 · 工程状态说明（形式化账本与依赖两项数字按 10-24 / 10-25 复核）

FIBEMATE 是一个后量子密码（PQC）的工程验证平台：ML-KEM / ML-DSA / SLH-DSA 与 SM2/SM3/SM4 的实现、跨语言互操作、CBOM 供应链物料清单，以及一条在 Isabelle/HOL 中推进的 VWZ 构造形式化线。

它不是产品发布，也不是融资贴。发这篇的原因很具体：主仓的 OpenSSF Scorecard 里 Code-Review 一项是 0（0/28 个有审批的变更集），这是单人维护结构的硬伤，只能靠外部评审补。下面把当前状态、已验证的数字、以及明确没做完的部分分开写清楚——凡是能复跑的都给出命令或入口。


## 一、工程基建：哪些是真的，哪些还不是


### 合并门禁（main 分支，ruleset 强制）

- 7 项必需检查：`lint`、`bom-check`、`bench`、`sbom`、`docs-check`、`dco`、`interop`。
- 分支必须与 base 同步；禁止强推、禁止删分支；所有变更走 PR。
- 每个提交必须带 DCO `Signed-off-by`。这一条拦下过真实的违规：GitHub 网页端 "Update branch" 生成的 merge commit 不带 signoff，会被门禁拒绝——所以流程要求本地 rebase + `--force-with-lease`。


### 供应链

- `fibemate` 仓的 GitHub Actions 引用：**91 处全部固定到 40 位 commit SHA，浮动 tag 为 0**（按 `.github/workflows/*.yml` 逐文件扫描）。
- 但"全部依赖已按 hash 固定"不成立：npm / pip / 容器镜像层仍有未按 hash 固定的项，Scorecard 的 Pinned-Dependencies 因此是 **8/10**。这是开放缺口，不是已完成项。


### 外部评分（照抄，不解释）

- 主仓 OpenSSF Scorecard **8.1 / 10**（2026-10-25T03:27:27Z，commit `2de752d`，scorecard v5.6.0）。
- 桌面端（`fibemate-tauri`）**7.6 / 10**（2026-10-19T03:34:38Z，commit `64f8980`）。两个数字不是同一个仓，别混用。

主仓失分项（同一份报告）：

| 检查项 | 得分 | 说明 |
|---|---|---|
| Code-Review | 0 | 0/28 个有审批的变更集 |
| Branch-Protection | 4 | 开发与所有发布分支未达最严配置 |
| Contributors | 3 | 仅 1 个贡献组织 |
| Packaging | −1 | 未检测到打包工作流 |
| Binary-Artifacts | 8 | 源码树中存在二进制文件 |
| Pinned-Dependencies | 8 | 存在未按 hash 固定的依赖 |
| Signed-Releases | 8 | 3 个发布各有签名产物，缺 provenance |
| CII-Best-Practices | 5 | 已获 Passing 徽章 |

桌面端的 2 条 RUSTSEC 告警（`proc-macro-error`、`glib`）来自固定的 GTK 0.18 传递依赖，上游没有已发布补丁；`deny.toml` 没有 ignore 列表，靠作用域限定，缺口在仓内备案。


### 依赖告警

- Dependabot 开放告警：`fibemate`、`fibemate-tools`、`pqc-hw-bench` 均为 **0**（2026-10-25 复核）。`fibemate` 此前积压 11 条，其中 3 条 `body-parser` 拒绝服务（`GHSA-27r3-jxmh-p828`）是运行路径上的真实告警，已按同一 advisory 的两段 range 分别修掉：1.x 线升到 1.20.9，2.x 线升到 2.4.0。
- 另有 8 条 `electron` 告警位于 `tools/pqc-desktop`，`scope=development`，不随产物分发，按 `tolerable_risk` 关闭并在告警里写明「为什么不可达 + 何时重做」。这类关闭不是「已修复」，所以单独说明。

### 静态分析

- CodeQL 开放告警：`fibemate`、`fibemate-mobile`、`fibemate-tools`、`fibemate-tauri` 均为 **0**。
- `fibemate-react-native` 尚未启用 CodeQL（API 返回 `no analysis found`）。这是"没有分析"，不等于"没有告警"，所以不并入上面的 0。


### CBOM

- 按 CycloneDX **1.6** 生成，当前 **9 个原语组件**（AES、ML-DSA、ML-KEM、P-256/ECDH、SHA-256、SLH-DSA、SM2、SM3、SM4）；自造信息统一放 `fibemate:` 命名空间，不冒充标准字段。
- 生成器是确定性的（`SOURCE_DATE_EPOCH`、固定 `serialNumber`），发布流水线做两件事：drift 校验（`node scripts/build-cbom.js --check`）与官方 schema 校验（`tools/validate-cbom.cjs`；bom-1.6 / spdx / jsf 三份 schema 随仓 vendored）。
- PR 门禁里的 `bom-check` 目前覆盖 BOM、编码损坏扫描与实验代码隔离，CBOM 的 schema 校验还没进 PR 门禁——这也是缺口。


### 测试

- `fibemate-mobile` 有 **87 条 `node:test` 用例**（5 个文件，源码静态计数 16 / 10 / 15 / 37 / 9），含源码级静态守卫：某个修复被后续改动悄悄回退时，测试会红。
- 这里要说明口径：87 是源码静态计数，不是 CI 实跑日志的取证结果；把它写成"CI 真实执行 87 条"是不准确的，所以不这么写。

### ACVP 覆盖

| 算法 | 覆盖 | 口径 |
|---|---|---|
| ML-KEM-512/768/1024 | **240/240** | keyGen 75、encaps 75、decaps 30、encapsulationKeyCheck 30、decapsulationKeyCheck 30；向量已入库，离线可跑，接在 `ci.yml` 的 `mlkem-kat` 与 `kat-regression.yml` |
| ML-DSA-44/65/87 | 75/75 | 仅 keyGen，且由 Phase 1 包装的 `@noble/post-quantum` 后端产出；sigGen / sigVer 的向量级覆盖还没有 |

ML-KEM 的两个 key check 按 FIPS 203 §7.2 / §7.3 实现：`encapsKeyCheck` 做长度 + 12 位编码的规范性（`byteEncode12 ∘ byteDecode12` 必须等于原文，非规范系数 ≥ q 就此被挡住），`decapsKeyCheck` 做长度 + 存储的 `H(ek)` 与内嵌 `ek` 现算哈希一致。内嵌 `ek` 故意不再做模数检查——标准没要求，ACVP 的判定也只认哈希，加严会造出假阴性。


## 二、形式化线：6 条 sorry，四处被机器判定的陈述

形式化在独立仓 `vwz-formalization`（公开，Apache-2.0），Isabelle/HOL，session `VWZ_A3_Aligned`。与业务仓分开是因为工具链、发布节奏和体积都不同。

账本（由工具生成，不手填）：

| 层级 | 内容 | 引理 | sorry |
|---|---|---|---|
| T0 | 纯形式改写 | 17 | 0 |
| T1-A | 代数公理 | 16 | 0 |
| T1-D | 定义相关义务 | 5 | 2 |
| T2 | 线性代数 / 矩阵 | 10 | 2 |
| T3 | 安全 / 概率 / 解析器 | 8 | 2 |
| **合计** |  | **56** | **6** |


### 已经有实体的部分

- `F_3329` 域表示。
- 燃料参数化的 Gauss–Jordan 消元：`mat_rank`、`dim_nullspace`、`mat_inv` 不再是未解释常量。燃料让递归是结构递归，不需要终止性证明；但"消元到达行最简形""rank 等于域上秩""逆是双侧逆"这些没有被声称。
- §3.1 的 LCG 作为状态机（`nat ⇒ nat × nat`，返回值与后继状态）；拒绝采样采样器证的是部分正确性：返回值非空时，长度、互异、范围成立。终止性只以概率 1 成立，本 session 没有测度论，因此不作声称。
- §3.3 的行加法矩阵生成器（`m*m` 轮，`i=j` 时两次抽取都消耗后跳过）、按规范顺序生成四个矩阵、以及按 §3.6 字段填充的 KeyGen 实体。
- `hash_target` 有实体了：池内的部分 Fisher–Yates 走位 + 指示向量（`fy_fuel` / `swap_at`），稠密性由走位长度保证，不靠假设。


### 四处被机器判定的陈述

| 义务 | 缺陷 | 状态 |
|---|---|---|
| T2_B3 | 按整数陈述可逆，实现每步模 3329 归约（域错配） | 改述到 F_q 后**已闭合** |
| T2_D4 | 对非方阵系统误用行零化度（口径错配） | 改用列零化度后**已闭合** |
| T2_B7 | 断言 ψ 每片秩为 2，但前提不排除零切片 | 补非零 2×2 子式前提后**已闭合**（2026-10-24） |
| T2_D5 | `Eval` 收不到 k / msg，却要求目标位依赖消息 | **机器反证**，待签名语义 |

T2_B7 的反例满足前提而秩为 0，记录在 `VWZ_Refutations.thy`。原因是陈述缺良构前提——这是陈述缺陷，不是证明失败。把反例留在仓里，比悄悄删掉更有用。

改述后它已经闭合：补上「存在非零 2×2 子式」这一前提，秩 ≤ 2 由「每片是两个外积之和、因而行落在二维 span 内」得到（`rows_in_span_psi_slice_of` + `mat_rank_le_two_of_rows_in_span`），秩 ≥ 2 由非零子式得到（`rank_ge_two_of_nonzero_minor`），两侧夹出 `mat_rank (psi_slice …) = 2`。这条路只证明这一族切片，**没有建立通用秩理论**。

这不仅是诚实，更是后续迭代的锚点：每一次改述都有机器证据可回溯，下一个人不必重新争一遍。


### 已知缺口

- **T2_D5 是唯一剩余缺陷**：`Eval` 是 `consts`，不接收 k / msg，而义务要求目标位依赖消息。这是规范本身的冲突，不是证明欠账；要修它得先决定 `Sign` 的签名语义，所以保留 `sorry` 与缺陷标签，等规范决策。
- 原计划的通用秩理论（行最简形、子式在初等行变换下的不变性、`mat_rank (A·B) ≤ n_cols A`）标记为 **superseded**：T2_B7 已用二维 span 的窄路线闭合，这几个引理不再是前置条件。
- T3 剩余 **2 条**：概率与安全层的建模，需要先把签名语义定下来。
- `digest`、`Eval`、`Sign`、`Verify`、`sample_below`、`nullspace`、`mat_solve` 仍是未解释常量，逐个标 `TODO(define)` 并注明所缺的规范内容。不写"忽略参数的占位定义"——那会让引理变成关于一个自造矩阵的陈述，比留着洞更糟。
- 该仓目前没有 CI，也没有独立的 CONTRIBUTING；构建与计数命令在 README 里。构建：`isabelle build -D aligned`；负向对照：`isabelle build -D neg` 必须失败。


## 三、当前缺口（按上手难度排序）

1. **T2_D5 的规范决策**：给 `Sign` / `Eval` 定语义（消息与目标位如何联结），才能决定这条义务是改述还是删除。
2. **T3 剩余 2 条**：签名语义（Sign 的输入输出与 pk 的联结）定下来之后才能谈目标独立性。
3. **ACVP 向量走公共 API**：`fml-dsa` 已透传 FIPS 204 的 context / extraEntropy，并有行为对照；现有 75/75 的 keyGen KAT 由 Phase 1 包装的 `@noble/post-quantum` 后端产出（包装层 API 用同一批向量验证），且只覆盖 KeyGen，sigGen / sigVer 的向量级覆盖还没有。ML-KEM 这条线已经补齐（240/240，含 60 条 key check）。
4. **RN 仓测试与 CI**：`fibemate-mobile` 的 `node:test` 模式已跑通，`fibemate-react-native` 的 test 脚本只有 jest，无测试文件时是否会静默通过尚未实测。
5. **CBOM 进 PR 门禁**，以及 npm / pip / 镜像层的 hash 固定。
6. **外部 code review**：Scorecard 的 Code-Review 0/28，每一个实质性评审都直接改变这个数字。


## 四、协作约定

- 提交必须 DCO sign-off；PR 落后 base 时用本地 rebase，不要用 GitHub 网页的 "Update branch"（它会生成不带 signoff 的 merge commit）。
- 不接受掩盖错误。能用证据推翻既有结论的 PR 会被优先处理；被推翻的陈述会保留在仓里（T2_B7 就是例子）。
- 声称与实现必须对齐：文档里写"已实现"，代码里就得有对应实体；写不出来就标 `TODO(define)`，不编造语义。
- 提交前请自证：给出命令、输出，以及必要的字节级检查（编码、BOM）。


## 五、入口

- 主仓：[github.com/Lennonhaha/fibemate](https://github.com/Lennonhaha/fibemate)
- 形式化仓：[github.com/Lennonhaha/vwz-formalization](https://github.com/Lennonhaha/vwz-formalization)
- 归档代码（v1.0.1，Apache-2.0）：[10.5281/zenodo.23622795](https://doi.org/10.5281/zenodo.23622795)（concept DOI `10.5281/zenodo.23622177`）
- 技术说明（中文，CC BY 4.0）：[10.5281/zenodo.23632173](https://doi.org/10.5281/zenodo.23632173)
- 方法学分析（英文 preprint，CC BY 4.0）：[10.5281/zenodo.23637405](https://doi.org/10.5281/zenodo.23637405)（*Deterministic but Wrong: Why Behavior-Based Tests Miss Structural Errors in Keccak-f Implementations*，含源码包）
- 负面结果报告（英文技术报告，CC BY 4.0）：[10.5281/zenodo.23638522](https://doi.org/10.5281/zenodo.23638522)（*An Empirical Study of Depth-Multiplicative Trapdoor Constructions: Model Correction and Negative Results* — DMTH 负面结果，不作安全声称，未经同行评审）
- 论文（首发版）：[v1.0.0-paper](https://github.com/Lennonhaha/vwz-formalization/releases/tag/v1.0.0-paper)
- 贡献指南：[docs/CONTRIBUTORS-GUIDE.md](https://github.com/Lennonhaha/fibemate/blob/main/docs/CONTRIBUTORS-GUIDE.md)

本文数字的复核方式：

```
node tools/count-obligations.cjs
curl -s https://api.securityscorecards.dev/projects/github.com/Lennonhaha/fibemate
gh api "repos/Lennonhaha/fibemate/code-scanning/alerts?state=open" --jq length
gh api "repos/Lennonhaha/fibemate/dependabot/alerts?state=open" --jq length
```


## 六、不适合谁

- 需要一个能直接上线、带 SLA 的密码库的：这里不是。
- 只想要 star 数、不接受"未完成的证明必须显式标注"的：这里会更难受。
- 期待"AI 生成即合并"的：门禁会拦，评审也会拦。

如果你能补上面任何一块，直接开 issue 或 PR。用代码和证据说话，比什么都快。