miniblink49 内核中的 fiat 目录：由 Coq 形式化验证生成的曲线域运算代码解析
miniblink49 内核中的 fiat 目录由 Coq 形式化验证生成的曲线域运算代码解析【免费下载链接】miniblink49a lighter, faster browser kernel of blink to integrate HTML UI in your app. 一个小巧、轻量的浏览器内核用来取代wke和libcef项目地址: https://gitcode.com/GitHub_Trending/mi/miniblink49导读本文聚焦 miniblink49 仓库 node/openssl/openssl/third_party/fiat 目录及其 README.md讲解这套随项目一起分发的fiat-crypto 生成代码它是什么、为何存在、如何从形式化验证工具链重新生成 Curve25519 与 P256 的域运算field arithmetic实现以及这些自动生成代码在仓库内如何被实际引用。读完本文你将能读懂 fiat 目录中每个文件的来源与作用理解仅素数模是规范性约束、其余都是编译器提示的生成哲学并掌握在本地用make命令重新生成对应.c文件的完整操作方式。一、fiat 目录是什么一份正确性由构造保证的密码学代码在 miniblink49 的 node/openssl 第三方依赖中fiat 目录存放的并非手写的椭圆曲线代码而是由Fiat即 MIT 形式化验证团队 mit-plv 的 fiat-crypto 项目自动生成的特殊化代码。从 README.md 的第一段可以明确两点事实本目录中部分代码由 fiat-crypto 生成这些生成文件遵循MIT 许可证许可证全文见同目录 LICENSE版权归 2015-2016 年的 fiat-crypto 作者。目录中的实际文件构成与 README 的说明完全对应见 目录列表文件内容curve25519.c生成的 Curve25519 域运算主文件32/64 位两套实现被整合进同一编译单元curve25519_32.h/curve25519_64.h32 位与 64 位两套由机器生成Autogenerated的域运算头文件curve25519_tables.h预计算表配合make_curve25519_tables.py生成p256.c、p256_32.h、p256_64.h生成的 P-256NIST P-256Montgomery 域运算internal.h手工维护的内部类型与接口声明README.chromium/METADATA/BUILD.gn/LICENSE第三方依赖元数据与许可证说明其中 internal.h 是理解整套代码的关键入口它定义了域元素fe与松域元素fe_loose两种表示64 位平台定义了BORINGSSL_CURVE25519_64BITfe为uint64_t v[5]即 5 个 limb、radix 2^51 的表示limb 上界约为 1.125×2^51fe_loose的 limb 上界放宽到约 3.375×2^51用于加减法结果乘法和进位归约后回到fe。32 位平台fe为uint32_t v[10]即 10 个 limb、radix 2^26/2^25 交替的表示。二、Curve25519 域运算的生成方式与参数语义2.1 标准生成命令按 README.md 的 Curve25519 一节在 fiat-crypto 的源码检出目录对应提交7892c66d5e0e5770c79463ce551193ceef870641中生成curve25519.c中的域运算过程需要执行make src/Specific/solinas32_2e255m19_10limbs/femul.c其中femul是占位符可替换为所需的其它域运算如fadd、fsub、fsquare等。整套流程的核心是先有 Coq 形式化定义再由工具链展开成 C 代码。2.2 参数文件CurveParameters.v真正指定有限域并引用实现策略的源文件是src/Specific/solinas32_2e255m19_10limbs/CurveParameters.vREADME 给出的参数语义可概括为一句关键描述使用 radix 2^25.5 的 10 个 32 位无符号整数 limb、单条进位链、两个环绕进位做模 2^255-19 的非饱和unsaturated算术。这里有一个非常重要的原则README 明确强调只有素数模2^255-19被视为规范性normative约束其余所有内容limb 数量、radix、进位策略等都只是编译器提示compiler hints。换言之生成代码的正确性由素数本身与 Coq 证明保证而性能相关的表示选择只是建议性参数。2.3 64 位变体来自 curve25519-donna 的指令调度对于 64 位平台README 说明其采用5 个 limb、radix 2^51的实现且指令调度取自 curve25519-donna-c64业界著名的参考实现。对应的目录是src/Specific/solinas64_2e255m19_5limbs_donna这一点与仓库源码相互印证在 internal.h 中64 位fe的注释明确写着元素 t 表示 t[0]2^51·t[1]2^102·t[2]2^153·t[3]2^204·t[4]正是 5×51 位布局。2.4 生成代码的头部证据打开实际的生成文件可以验证上述全部参数。例如 curve25519_64.h 第 1-7 行的头部注释直接记录了生成时的输入/* Autogenerated */ /* curve description: 25519 */ /* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */ /* n 5 (from 5) */ /* s 0x8000000000000000000000000000000000000000000000000000000000000000 (from 2^255) */ /* c [(1, 19)] (from 1,19) */ /* machine_wordsize 64 (from 64) */而 curve25519_32.h 的对应注释则是n 10、machine_wordsize 32即 10 个 limb 的 32 位版本。两份头文件都包含fiat_25519_carry_mul、fiat_25519_carry等由生成器输出的函数并带有严格的输入/输出边界注释如[0x0 ~ 0x7ffffffffffff]这些边界正是形式化验证所保证的数值范围约束为后续调用方提供契约。三、P256 域运算的生成方式与已知问题3.1 生成命令与参数对 P-256README 给出的生成命令为make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c对应的 Coq 源文件是src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/CurveParameters.v其参数语义为使用 64 位饱和saturated逐字 Montgomery 归约模数为 2^256 - 2^224 2^192 2^96 - 1。与 Curve25519 一样README 再次强调除素数外的一切都不可信untrusted。从目录名montgomery64_..._4limbs可以看出这是4 个 64 位 limb的 Montgomery 表示——256 位素数恰好由 4 个 64 位字承载这是与 Curve25519 的 Solinas 表示非饱和多 limb截然不同的另一种策略。实际生成文件同样在头部留下证据p256_64.h 的注释为/* Autogenerated */ /* curve description: p256 */ /* requested operations: (all) */ /* m 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff (from 2^256 - 2^224 2^192 2^96 - 1) */ /* machine_wordsize 64 (from 64) */并且该文件明确附加了一条使用前提所有合成函数的输入都必须严格小于素数模 m且处于唯一的饱和表示中所有返回值也保证满足这两条性质。这是 Montgomery 算术的典型调用契约任何上层调用方都必须遵守。3.2 P256 的 fesub.c 已知问题README 诚实记录了当前存在的一个已知问题fesub.cP256 的减法运算在 Coq 8.7.0 上无法在一周内完成构建specialization即特殊化展开。同时 README 提到一个备选分支fiat-crypto 的3e6851d...提交能够成功构建该文件但该分支的工作从未完成——其实现模板的正确性证明仍然有效但被遗弃的原型特殊化设施是未经验证的。因此在引入这类生成代码时需要意识到工具链本身也存在尚未收敛的工程边界生成能力 ≠ 所有运算都能在合理时间内完成。四、这些生成代码如何在仓库中落地4.1 依赖元数据来源、版本与本地修改README.chromium 表明这是一个随 Chromium/BoringSSL 依赖体系分发的第三方组件组件名Fiat-Crypto: Synthesizing Correct-by-Construction Code for Cryptographic Primitives许可证MIT许可证文件为 LICENSE安全关键性yesSecurity Critical: yes而 METADATA 记录了更精确的版本信息上游 git 版本为4441785fb44b88bb6943ddbf639d872c8c903281最近一次升级日期为 2019 年 1 月 16 日并注明一条本地修改Fiat 生成的代码已被整合进现有 BoringSSL 代码中local_modifications。这解释了为何 fiat 目录内的文件风格fiat_25519_*函数前缀、fe/fe_loose类型、x25519_ge_*接口与 BoringSSL 的 Curve25519 实现同源。BUILD.gn 中只有一个名为fiat_license的source_set其注释说明它只是为了让 Chromium 的tools/licenses.py脚本能识别README.chromium——即该文件是纯粹的许可证追踪占位目标不参与实际编译真正的编译集成发生在curve25519.c/p256.c被上层 crypto 模块 include 之时。4.2 上层如何调用从声明到使用从仓库源码的引用关系可以确认这些生成代码并非孤儿文件crypto/curve25519/spake25519.c 等文件依赖本目录提供的fe、ge类型与x25519_ge_*系列接口完成 SPAKE2 等协议的实现crypto/ec/ecp_nistp256.c 与 crypto/ec/ec_lcl.h 涉及对 P256 域运算的引用crypto/fipsmodule/bcm.c 将 Curve25519 相关实现整合进 FIPS 边界模块的构建。一个值得注意的细节是internal.h中x25519_NEON仅在OPENSSL_ARM !OPENSSL_NO_ASM !OPENSSL_APPLE时定义说明该目录的纯 C 生成代码与 ARM NEON 汇编asm/x25519-arm.S是互斥的优化路径优先使用汇编加速否则回退到 fiat 生成的通用 C 代码。五、深入 fiat-crypto 生态如何上手与进一步阅读README 的最后一节 Working With Fiat Crypto Field Arithmetic 为希望深入源码生成机制的读者指出了三条学习路径以下均为 README 提及的资料本仓库未随附仅供理解背景fiat-crypto 项目 README 的 arithmetic core 部分先概览实现模板再逐段阅读特殊化specialization机制Andres Erbsen 的博士论文第 3 章http://adam.chlipala.net/theses/andreser.pdf系统性地介绍该体系中不那么混乱的部分正在进行的重构工作社区正计划用更有原则的机制整体替换现有的特殊化机制fiat-crypto 项目面板 #4。结合本仓库可以这样理解这三条路径的意义curve25519_32.h/curve25519_64.h这类文件是特殊化机制的产物——生成器拿到CurveParameters.v中的参数后在 Coq 中完成证明并把证明驱动的算法展开为具体 C 函数。因此仅素数才是规范性的这句话的工程含义是当你修改 radix、limb 数量等提示参数时生成器会重新展开并重新证明最终产物依然正确只是速度与形态不同。六、总结miniblink49 的 node/openssl/openssl/third_party/fiat 目录是一份正确性由构造保证的密码学代码的完整样例来源MIT 的 fiat-crypto 形式化验证工具链自动生成MIT 许可证安全关键组件两大曲线Curve25519Solinas 非饱和算术32 位 10 limb / 64 位 5 limb 两套布局与 P-2564 limb 饱和 Montgomery 归约生成命令make src/Specific/solinas32_2e255m19_10limbs/femul.c与make src/Specific/montgomery64_2e256m2e224p2e192p2e96m1_4limbs/femul.c核心原则只有素数模是规范性的其余参数均为编译器提示已知边界P256 的fesub.c在 Coq 8.7.0 下存在无法按期完成特殊化的问题存在未经验证的备选分支集成方式internal.h统一声明fe/fe_loose与x25519_ge_*接口供 crypto/curve25519/spake25519.c、crypto/ec/ecp_nistp256.c、crypto/fipsmodule/bcm.c 等上层模块调用。对关注密码学实现可靠性的读者而言这套目录展示了用证明工具生成关键路径代码在真实浏览器内核/SSL 栈中的落地形态手写代码追求的是性能与可读性而 fiat 生成代码追求的是只要证明通过实现即正确的强保证。【免费下载链接】miniblink49a lighter, faster browser kernel of blink to integrate HTML UI in your app. 一个小巧、轻量的浏览器内核用来取代wke和libcef项目地址: https://gitcode.com/GitHub_Trending/mi/miniblink49创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考