当前状态

2026-10-25 · 工程状态说明 · 已验证的数字与明确未完成项

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

合并门禁（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
• 形式化仓：github.com/Lennonhaha/vwz-formalization
• 归档代码（v1.0.1，Apache-2.0）：10.5281/zenodo.23622795（concept DOI 10.5281/zenodo.23622177）
• 技术说明（中文，CC BY 4.0）：10.5281/zenodo.23632173
• 方法学分析（英文 preprint，CC BY 4.0）：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（An Empirical Study of Depth-Multiplicative Trapdoor Constructions: Model Correction and Negative Results — DMTH 负面结果，不作安全声称，未经同行评审）
• 论文（首发版）：v1.0.0-paper
• 贡献指南：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。用代码和证据说话，比什么都快。