nickharris808/ct-mask

# ct-mask **你的掩码器件是一阶安全的——或者这里是重组了秘密的精确探测线。两份独立且可重放的证书，而且都不是 t-test。** [](LICENSE) [](pyproject.toml) [](#the-model-read-this-first) [](.github/workflows/ci.yml) ## 为什么需要它 大多数掩码验证通过**依赖性**来进行分析：如果一次探测最多只触及每个秘密的一份份额，那么它就是安全的。这条规则是可靠的，但还不够。它会拒绝那些实际上至关重要的器件。 以一个面向域的掩码 AND 为例。它的输出份额 `c0` 触及了某一个操作数的**两**份额。仅分析依赖性的工具会将其标记出来。但它是完全安全的，因为有一个全新的掩码刷新了交叉项——而任何依赖性推理都无法看到这一点。 ct-mask 补全了缺失的证书。如果一根探测线*每当全新的掩码位翻转时就翻转*，那么它在该掩码上是均匀分布的，因此与任何秘密都无关，**无论它触及了多少份额**。两份证书都可归结为简单的不可满足性，因此它们都是经过机器验证的驳斥，而非统计测试。 ## 模型，请先阅读此部分 **无毛刺的门值探测，一阶（`d = 1`），双份额。** 探测观察的是单根内部连线的稳定布尔值。毛刺、转换、耦合和物理测量均不属于此模型。如果你的威胁模型包含这些情况，这里的 `SECURE` 结论将无法为你提供保障。这是此类工具的标准模型，已明确说明而非隐藏在脚注中。 ## 安装说明 ``` git clone https://github.com/nickharris808/ct-mask.git && cd ct-mask pip install . ``` 一旦发布，这将成为 `pip install ct-mask`。 发布包名是 `ct-mask`；导入名是 `ctmask`。 ## 30秒快速入门 ``` ct-mask corpus # every bundled gadget against its expected verdict ct-mask list # what is in the corpus ct-mask check dom_and # full probe-by-probe report ``` ## 实际示例 ``` $ ct-mask check dom_and dom_and ================================================================== model glitch-free gate-value probing, first order (d=1), 2-share verdict SECURE probe secure certificate refreshed by -------------------------------------------------------- a0b0 yes dependence - a0b1 yes dependence - a1b0 yes dependence - a1b1 yes dependence - cross0 yes dependence - cross1 yes dependence - c0 yes uniformity z c1 yes uniformity z modelled leakage over 4 secret classes (Hamming weight, glitch-free, unit weight): mean invariant across classes True whole distribution invariant False -> first-order secure. An adversary observing more than a mean is NOT covered by this verdict; that is a limit, not a defect. ``` `c0` 和 `c1` 是仅依靠依赖性分析的工具无法认证的两根连线。这正是均匀性证书发挥作用的所在。 ### 而当器件确实发生泄漏时 ``` $ ct-mask check naive_and verdict LEAKY LEAKY PROBES (these recombine a secret): c0 touches a: a0; b: b0, b1 c1 touches a: a1; b: b0, b1 ``` `c0 = (a0 & b0) XOR (a0 & b1)` 可简化为 `a0 & b` —— 即一个秘密的份额与另一个秘密的*整体*进行 AND 操作，并且没有掩码来刷新它。退出状态码为 `1`。 ## 声明结论未涵盖的内容 一阶证书是关于建模泄漏的**一阶矩**的声明，仅此而已。ct-mask 不会将这一点留在脚注中——它会针对每一个秘密类别，在全新的随机性上精确枚举完整的建模泄漏分布，并记录**两项独立的判定结果**： | 判定 | DOM-AND | |---|---| | 均值在各秘密类别间保持不变 | `True` | | 整体分布保持不变 | `False` | 这两者都会写入报告中。*均值*不保持不变的器件会被直接拒绝；而记录在案的分布依赖性是通过验证的结论中**披露的局限性**，而非被容忍的失败。如果你的对手能看到比均值更多的信息，证书本身会告诉你这一点。 ## 内置语料库 每一个安全的器件旁边都附带了一个损坏的对应物，就像基准测试需要对照组一样——因为一个对所有东西都报告 `SECURE` 的工具毫无价值。 | 器件 | 预期结果 | 它是什么 | |---|---|---| | `dom_and` | SECURE | 面向域的掩码 AND，双份额，一个全新掩码 | | `refreshed_share` | SECURE | 由全新掩码刷新的单个份额 | | `naive_and` | LEAKY | 与 `dom_and` 结构相同，无刷新 | | `unmasked_and` | LEAKY | 完全没有掩码 | | `recombining_xor` | LEAKY | `a0 XOR a1` 在一个门中重建了秘密 | `naive_and` 在*功能上是正确*的——测试套件证明了 `c0 XOR c1 == a AND b`。它在安全性上是损坏的，而不是在功能上，这是唯一有意义的损坏。 ## 构建你自己的器件 ``` from ctmask import Netlist, analyse n = Netlist("my_gadget") n.add_input("a0", "share", of_secret="a") n.add_input("a1", "share", of_secret="a") n.add_input("z", "mask") n.add_gate("t", "xor", "a0", "z") r = analyse(n) print(r.to_dict()["verdict"], r.probes[0].certificate) # SECURE dependence ``` 输入类型包括 `secret`、`share`（命名其共享的秘密）、`mask`（全新随机性）和 `public`。门类型包括 `and`、`or`、`xor`、`xnor`、`not`、`buf`。 ## 精确性 依赖性是**语义上通过驳斥来决定**的，而不是通过查看表达式中出现的变量名。`(a0 AND z) XOR (a0 AND NOT z)` 提到了两次 `z`，但根本不依赖于它；ct-mask 能够正确识别这一点，并且有相应的测试。同样，均匀性要求掩码*始终*翻转探测，而不仅仅是偶尔翻转——一个偶尔改变连线的掩码什么也证明不了。 符号评估器和具体评估器在每个内置器件的整个输入空间上进行了交叉检查。如果验证器的评估器与其求解器不一致，那它证明的内容就与它所报告的不同。 ## 诚实的局限性 - **仅限 `d = 1`。** 不支持高阶或多变量分析。未对第二个探测点进行建模。 - **无毛刺。** 不涵盖转换和毛刺扩展探测。 - **建模泄漏，而非测量。** Hamming weight 函数只是一个模型，而不是示波器。这里的任何东西都不能替代实验室评估。 - **器件规模。** 精确分布枚举会在整个输入空间上运行，因此它适用于器件，而不适用于完整的密码算法。探测认证本身则具有更大的扩展性。 - **充分但不必要。** 两份证书都是充分条件。`LEAKY` 结论意味着“两份证书都不适用”，并指出了该连线的名称，以便你自行判断。 ## 在不展示你的 netlist 的情况下进行证明 ct-mask 在你**手动提交**的 netlist 上验证掩码。在不披露器件的情况下向第三方证明一阶安全性，以及通过机器检查的泄漏契约将硬件时序结果带入软件分析中，这些是商业能力，不包含在此包中。这里的所有操作都在你已经完全控制的设计上运行。 ## hw-verify 工具包的一部分 五个开源工具、一个数据集和一个浏览器演示，用于证明硬件和边界检查的安全属性。它们共享一个边界：**所有开源分析都是在完全披露的设计上进行的。** | 项目 | 功能描述 | |---|---| | **▶ [在线演示](https://huggingface.co/spaces/nickh007/hw-verify)** | 在浏览器中尝试 constant-time 检查器——通过 Pyodide 运行真正的分析器 | | [`ctbench`](https://github.com/nickharris808/ctbench) | 匹配的 constant-time RTL 基准测试 + 排行榜 | | [`patchproof`](https://github.com/nickharris808/patchproof) | 证明边界检查修复消除了*每一个*违规输入 | | **`ct-mask`**（你正在这里） | 通过两份证书进行的一阶掩码验证 | | [`hw-verify-mcp`](https://github.com/nickharris808/hw-verify-mcp) | MCP server——所有三个检查器，可由 AI 代理调用 | | [`ct-audit-action`](https://github.com/nickharris808/ct-audit-action) | GitHub Action——因泄漏的完成信号而导致 PR 失败 | | [`hw-verify` dataset](https://huggingface.co/datasets/nickh007/hw-verify) | 49 条记录，3 个数据集划分，可通过这些工具实现字节级复现 | | [`hw-verify-static`](https://github.com/nickharris808/hw-verify-static) · [`hw-verify-space`](https://github.com/nickharris808/hw-verify-space) | 在线演示的源码（Pyodide）以及更完整的 Gradio 构建 | **商业边界。** 向永远无法获取设计的第三方证明属性——将结论绑定到一个保持隐藏的设计承诺上——这是一个不同的问题，也是一个商业问题。它不包含在上述任何一个包中。 ## 许可证 Apache-2.0。参见 [LICENSE](LICENSE)。 ## 贡献指南 新的器件——尤其是那些你认为我们会判断错误的器件——是最有价值的贡献。参见 [CONTRIBUTING.md](CONTRIBUTING.md)。

标签：Python, 侧信道分析, 密码学, 形式化验证, 手动系统调用, 掩码防护, 无后门, 逆向工具