Fiat Crypto

什么是 Fiat Crypto？

 

Fiat Crypto（也常写作 Fiat-Crypto 或 Fiat Cryptography）是一个开源系统，用于生成高效且经过形式化验证的密码学算术代码。

 

该系统旨在将高层数学描述转换为低层实现，并附带经机器检查的正确性证明。

 

该项目主要关注椭圆曲线密码学、数字签名、密钥交换、身份验证及其他密码系统中使用的算术运算。

 

加密货币软件高度依赖这类算术计算，因为区块链交易通过数字签名授权，并利用有限域上的代数计算进行验证。

 

Fiat Crypto 不是加密货币、代币、区块链、稳定币、钱包、交易平台或法币支持的数字资产。

 

其名称中的“fiat”指的是编程语言领域中根据规范生成软件的含义，而不是政府发行货币的金融含义。

 

官方 Fiat-Crypto 代码库将该项目描述为一个用于合成密码学原语正确构造代码的系统。

 

该项目源于麻省理工学院编程语言与验证研究组相关的研究。

 

该项目的核心目标是降低安全关键型密码学软件中出现隐蔽算术错误的风险。

为什么密码学算术运算很难？

 

许多密码算法可以很容易地用数学方程表示，但要在真实计算机处理器上高效实现却并不容易。

 

数学规范可能需要对包含数百位的整数进行运算。

 

普通处理器通常只能处理小得多的固定长度数值，例如 32 位或 64 位机器字。

 

开发者必须将大数拆分成多个较小部分，并谨慎处理进位、借位、乘法结果和模约简。

 

一个进位错误或一次遗漏的约简，就可能导致签名错误、拒绝有效交易、接受无效数值，或泄露机密信息。

 

最快的实现通常由一长串底层算术操作构成。

 

这类程序可能难以供人工审查者理解，也难以进行全面测试。

 

传统测试可以证明代码在选定输入下能够正常工作。

 

但它无法证明实现对所有可能的有效输入都能正常工作。

 

Fiat Crypto 通过根据数学规范生成代码，并同时生成可由机器检查的证据，证明生成的算术运算符合这些规范，从而解决这一问题。

“正确构造”是什么意思？

 

“正确构造”是指在创建软件的过程中就将正确性纳入其中。

 

开发者首先给出所需运算的数学描述。

 

系统随后通过一系列经过证明的编译和优化步骤转换该描述。

 

每个经过验证的步骤都会保留原始运算的含义。

 

因此，最终的算术程序通过形式化证明与高层规范相联系。

 

这种方法不同于先手动编写优化代码，再尝试证明其正确性。

 

在支持新的素数模数或处理器字长时，这种方法还可以减少重复证明工作。

 

研究论文 《面向密码学算术的简洁高层代码》介绍了该项目如何使用简短的高层程序和经机器检查的功能正确性证明。

什么是形式化验证？

 

形式化验证使用数理逻辑证明软件满足明确定义的属性。

 

证明助手会根据一小组可信的逻辑规则检查每项证明。

 

Fiat Crypto 使用 Coq 证明助手来处理其规范、证明、编译器组件和代码生成过程。

 

Coq 允许开发者定义数学对象、编写程序、陈述定理，并构造由系统机械检查的证明。

 

成功的证明并非仅依赖运行一系列测试用例。

 

它针对形式化规范及其假设所涵盖的每个输入，确立已证明的属性。

 

形式化验证并不能证明完整加密货币应用中所有可以想象的属性。

 

它证明的是开发者在经过验证的模型中定义的特定命题。

Fiat Crypto 如何运作？

 

Fiat Crypto 从模算术的高层描述开始。

 

开发者需要指定素数模数、处理器字长、limb 排列方式、实现策略以及要生成的运算等信息。

 

系统在 Coq 中表示这些算术运算。

 

随后，系统应用经过验证的转换步骤，简化表达式、计算安全的数值界限、删除不必要的运算，并将程序逐步转换为机器字算术运算。

 

转换后的程序会成为直线式的类 C 内部表示。

 

后端会将该表示转换为目标编程语言或另一种经过验证的中间语言。

 

生成的函数可以包括加法、减法、乘法、平方、进位、条件选择和字节转换。

 

经过适当审查、集成、编译和测试后，生成的代码可以纳入更大型的密码学库。

什么是模算术？

 

模算术将相差模数整数倍的数视为等价，并以此进行计算。

 

时钟是一个简单的例子：13:00 和 1:00 在 12 小时制时钟上表示相同的位置。

 

密码学模算术使用大得多的模数，通常是大素数。

 

假设运算的模数为 17。

 

20 与 3 等价，因为 20 减去 17 后等于 3。

 

该表达式可以写作

。

 

椭圆曲线系统会反复执行对大素数取模的加法、减法、乘法、平方和求逆运算。

 

Fiat Crypto 会针对选定的模数专门优化这些运算。

什么是有限域？

 

有限域是一个有限集合，其中定义了明确的加法、减法、乘法和除法运算。

 

密码系统通常使用基于大素数模整数的有限域。

 

域中的数值范围从 0 到比该素数小 1 的数。

 

每个非零数值在域中都有一个乘法逆元。

 

椭圆曲线点使用坐标定义，其运算在有限域中进行。

 

因此，数字签名和密钥协商系统依赖正确的有限域运算。

 

Fiat Crypto 主要用于生成执行这些域运算的底层程序。

什么是 limb？

 

limb 是较大整数中一个机器字长的部分。

 

一个 256 位域元素可以用 4 个 64 位 limb 表示。

 

另一种实现方式可以使用 5 个 limb，每个大约包含 51 位。

 

在每个 limb 中留出未使用的位，可以为进位和中间结果预留空间。

 

最佳 limb 排列方式取决于模数、处理器、乘法指令、约简策略和性能目标。

 

如果选择了错误的界限，中间结果可能超出机器类型的表示范围。

 

Fiat Crypto 会计算并证明数值在生成程序中流转时所需的界限。

什么是模约简？

 

模约简会将较大的中间数转换为模数范围内的等价数值。

 

两个 256 位数相乘，产生的中间值最多可能需要 512 位表示。

 

实现必须对该数值按选定的素数取模约简。

 

通用除法运算可能速度较慢，且未必能满足时间行为方面的要求。

 

因此，密码学实现会根据模数的结构使用专门的约简方法。

 

Fiat Crypto 支持多种实现策略，用于生成高效的约简代码。

支持的算术策略

饱和 Solinas 算术

 

饱和表示法使用的 limb 会占满大部分或全部可用机器字范围。

 

Solinas 风格的算术会利用可表示为 2 的幂与少量其他项之和的素数。

 

与通用除法相比，这种结构可以加快约简速度。

非饱和 Solinas 算术

 

非饱和表示法会在每个 limb 的高位留出未使用空间。

 

这些额外空间允许连续执行若干算术运算，而不必立即进行完整进位或约简。

 

在 64 位机器上，Curve25519 域算术通常使用 5 个约 51 位的 limb。

逐字 Montgomery 算术

 

Montgomery 算术使用一种特殊数值域表示，使模乘无需对模数进行普通除法。

 

逐字 Montgomery 约简会按机器字大小分段处理结果。

 

这种方法适用于不具备便捷 Solinas 形式的一般奇数模数。

Dettman 乘法

 

Dettman 风格的乘法是一种实现技术，与某些素数域表示中的高效算术有关。

 

该技术会组织乘法和约简过程，以利用模数和 limb 结构的特点。

Solinas 约简

 

Solinas 约简利用 2 的幂与选定素数之间的特殊关系。

 

根据这些关系，可以将中间数的高位部分折叠回较低位。

基数转换

 

基数转换会改变域值在各 limb 之间的拆分方式。

 

当密码系统的两个部分使用不同内部表示时，可能需要执行基数转换。

 

当前代码库通过统一的

代码生成接口说明了这些策略。

Fiat Crypto 可以生成哪些运算？

 

Fiat Crypto 可以生成模加法和模减法程序。

 

它可以生成乘法和平方程序。

 

它可以生成进位和约简函数，将数值调整到可接受的范围内。

 

它可以生成取负函数以及乘以指定常数的函数。

 

它可以生成旨在避免普通机密数据相关分支的条件选择函数。

 

它可以生成在内部 limb 与标准字节串之间进行转换的函数。

 

具体可用函数取决于所选策略和命令行选项。

 

完整的签名或密钥交换实现还需要额外的群运算、哈希、随机数生成、协议验证和应用逻辑，而这些都超出了域运算程序的范围。

Fiat Crypto 支持哪些密码学素数？

 

Fiat Crypto 旨在为多种素数模数生成算术代码，而不是只支持某一条固定曲线。

 

官方代码库包含针对素数

的生成示例，该素数用于 Curve25519 系列密码学。

 

其中还包括 NIST P-256 域素数的示例。

 

其代码库也包含与 secp256k1 域相关的支持和证明工作，该域用于主流区块链签名系统。

 

Bedrock2 生成示例包括 Poly1305 身份验证中使用的素数

。

 

支持某个域素数并不意味着自动提供了所有使用该域的协议的完整实现。

 

开发者仍需将生成的算术代码与正确实现的点运算、签名、哈希、序列化、验证和密钥管理集成。

为什么 secp256k1 与 Fiat Crypto 有关？

 

secp256k1 是多种主流加密货币协议使用的一条椭圆曲线。

 

钱包使用 secp256k1 私钥生成签名，以授权区块链交易。

 

节点会在接受交易有效之前验证这些签名。

 

该曲线的坐标运算依赖于对特定 256 位素数取模的算术运算。

 

如果域算术出错，可能会产生错误的曲线点、签名或验证结果。

 

Fiat Crypto 对 secp256k1 相关算术的支持，使其与区块链实现研究和高保证钱包软件有关。

 

相关的 CryptOpt 研究项目也将 Fiat Cryptography 的经过验证的中间代码与优化汇编代码生成联系起来，其中包括涉及 secp256k1 算术的工作。

Fiat Crypto 与椭圆曲线密码学

 

椭圆曲线密码学使用满足有限域上代数方程的点。

 

公钥通过将曲线点乘以秘密标量得出。

 

签名生成和验证需要反复执行点加法、倍点、标量乘法和域运算。

 

Fiat Crypto 为这些高层算法底层的部分算术运算提供经过验证的基础。

 

代码库还包含 Edwards、Montgomery 和 Weierstrass 曲线表示的证明和定义。

 

仅有正确的域算术，并不能证明完整的椭圆曲线协议安全。

 

曲线、点验证、标量处理、随机数生成、签名构造和外围软件也必须正确。

Fiat Crypto 支持哪些编程语言？

 

当前代码库维护了一个主要的 C 后端。

 

它还支持 Bedrock2/C 路径，该路径对内部语法树与 Bedrock2 之间关系的证明覆盖更强。

 

由社区或外部维护的后端包括 Go、Rust 和 Zig。

 

JSON 后端被标记为实验性功能。

 

代码库指出，其 Java 后端已停止维护，并且已知存在问题。

 

后端状态可能会发生变化，因此开发者在选择生成代码之前，应查看当前的后端状态表。

 

该项目明确表示，并不对每个后端提供相同质量的保证。

编译器如何生成？

 

经过验证的定义和转换步骤在 Coq 中编写。

 

Fiat Crypto 可以将可执行编译器代码提取为 OCaml 或 Haskell。

 

生成的命令行程序接受描述算术实现方式的参数。

 

该程序会将生成的源代码写入标准输出。

 

采用这种方法后，用户每次生成代码时无需加载完整的证明助手即可运行代码生成。

 

证明开发确立了可执行编译器所提取自的那些转换步骤的属性。

 

用户在构建完整代码库时，仍需安装文档中列出的 Coq、OCaml、构建系统和软件包依赖项。

Fiat Crypto 能证明什么？

 

Fiat Crypto 旨在证明生成的算术代码相对于其形式化规范具有功能正确性。

 

功能正确性是指，对于满足文档所列前置条件的输入，生成的运算会计算出数学上预期的结果。

 

系统还会推理数值范围，确保中间值适合选定的机器整数大小。

 

经过验证的重写和编译步骤旨在保留表达式的含义。

 

端到端证明的具体范围取决于后端和集成路径。

 

代码库指出，Bedrock2 后端包含一项证明，将 Bedrock2 抽象语法树与内部抽象语法树联系起来。

 

其他将代码转换为语言字符串的后端目前不具备相同的证明覆盖范围。

 

在评估生成的源代码是否“完全经过验证”时，这一区别非常重要。

Fiat Crypto 无法证明什么？

 

Fiat Crypto 无法证明所有外围钱包、区块链节点、智能合约或应用都安全。

 

它不会自动证明密码学协议能够抵御所有数学攻击。

 

它无法证明私钥是使用足够随机性生成的。

 

它无法阻止开发者传入无效参数或错误使用生成的函数。

 

它无法保证每种编译器、链接器、操作系统、处理器或硬件设备都保留了所有预期属性。

 

大多数输出后端都没有一套完全经过证明的转换流程，能将内部表示转换为最终源代码文本。

 

代码库还指出，普通 C 编译器的整数表达式行为仍属于可信环境的一部分，或需要单独审查。

 

因此，应将形式化验证理解为范围明确、强有力的保证，而不是适用于所有情况的普遍保证。

Fiat Crypto 能保证恒定时间执行吗？

 

密码学代码通常需要避免控制流和内存访问模式依赖机密数值。

 

这种编程规范通常称为恒定时间编码。

 

生成的直线式算术和条件选择原语可以支持恒定时间实现。

 

但是，实际时间行为取决于生成代码所用的后端、编译器、目标处理器、外围代码和微架构。

 

功能正确性证明并不自动构成对所有计时、缓存、功耗、电磁、推测执行或故障注入攻击的完整证明。

 

开发者必须审查所选流程提供的具体保证，并进行适当的侧信道测试和分析。

Fiat Crypto 与手写密码学代码

 

由经验丰富的专家编写的手写密码学代码可以非常快速。

 

但这类代码也可能包含难以通过普通审查发现的错误。

 

每种素数、字长、处理器和算术表示通常都需要单独编写手动实现。

 

Fiat Crypto 可以基于可重复使用的数学框架自动完成其中许多专门化工作。

 

当假设或目标发生变化时，生成代码可能更容易重新生成。

 

仍需在实际目标平台上测量性能。

 

在某些专用环境中，精心编写的汇编代码仍可能比普通生成的 C 代码更快。

 

CryptOpt 等项目正在探索如何将 Fiat Crypto 经过验证的基础扩展为高度优化的汇编代码。

Fiat Crypto 与传统测试

 

测试会将有限数量示例的实际输出与预期输出进行比较。

 

形式化验证会针对定理所涵盖的完整输入范围，证明某个已定义属性成立。

 

测试仍然很有价值，因为它可以发现形式化证明以外的集成、构建、平台、序列化和性能问题。

 

Fiat Crypto 代码库使用一套成熟的密码学测试套件测试生成的 C 代码。

 

其 Rust 输出则使用另一套密码学库测试套件进行测试。

 

因此，形式化证明和实际测试是互为补充，而非互相取代。

Fiat Crypto 与法定货币

 

法定货币是政府发行的货币，例如美元、欧元或日元。

 

Fiat Crypto 是一个软件验证和代码生成项目。

 

该项目不发行货币，也不将代币与国家货币挂钩。

 

它不提供银行支付、银行卡支付、法币充值或加密货币购买服务。

 

搜索“fiat crypto”可能会出现将政府发行货币兑换成加密货币的信息。

 

这种金融含义与 Fiat-Crypto 软件项目无关。

Fiat Crypto 与法币兑换加密货币

 

法币兑换加密货币指将政府发行的货币兑换成加密货币或数字资产。

 

法币入金通道可能会处理银行转账、银行卡支付、身份验证、货币兑换和区块链转账。

 

Fiat Crypto 则用于生成密码学算术实现。

 

它不运营法币入金或出金通道。

 

这一区别很重要，因为两个术语看起来相似，却指向加密生态系统中完全不同的领域。

Fiat Crypto 与 Fiat–Shamir 变换

 

Fiat–Shamir 变换会将某些交互式证明协议转换为非交互式证明或签名。

 

其名称来自密码学家 Amos Fiat 和 Adi Shamir。

 

Fiat Crypto 是一个独立的形式化方法项目，用于合成密码学算术代码。

 

两者都属于密码学领域，但解决的问题不同。

 

Fiat–Shamir 关注协议交互和挑战生成。

 

Fiat Crypto 关注底层数学计算的形式化验证实现。

Fiat Crypto 与密码学库

 

完整的密码学库会提供可直接使用的 API，用于签名、加密、哈希、密钥交换、证书和其他协议。

 

Fiat Crypto 主要是用于生成算术组件的工具和证明框架。

 

其输出可以集成到更全面的库中。

 

更全面的库仍需负责协议逻辑、公共接口、内存管理、随机性、输入验证、错误处理和密钥安全存储。

 

开发者不应将一个生成的乘法程序视为完整的签名实现。

Fiat Crypto 与通用编译器

 

通用编译器可以处理涵盖多种计算类型的程序。

 

Fiat Crypto 是一个专注于密码学算术的领域专用系统。

 

这种专门用途使其能够利用有关素数域、limb、进位和模约简的数学知识。

 

它可以根据普通源代码中通用编译器可能无法推断的细节对代码进行专门优化。

 

生成的 C 代码或其他源代码之后仍可交由通用编译器编译。

 

因此，完整的可信流程既包括 Fiat Crypto 生成流程，也包括后续构建工具链。

Fiat Crypto 对区块链安全为何重要？

 

区块链协议通过密码学密钥控制有价值的资产。

 

即使区块链的经济规则正确，域算术错误仍可能破坏数字签名的安全性。

 

节点可能会处理从网络收到的不可信公钥、签名、证明和交易数据。

 

因此，密码学实现必须正确处理所有允许的边界情况。

 

对于输入空间极大的算术程序，形式化方法可以提供比普通测试更有力的证据。

 

Fiat Crypto 还可以更轻松地为不同处理器字长和素数域生成一致的实现。

 

这有助于减少对少数专家手动重写精细算术代码的依赖。

Fiat Crypto 如何帮助加密钱包？

 

钱包使用密码学算术生成公钥和签名。

 

移动钱包可能需要在 32 位或 64 位处理器上使用安全且高效的代码。

 

硬件钱包可能受到内存、时序和处理器能力的严格限制。

 

生成的域运算程序可以为密钥和签名操作提供经过验证的基础。

 

钱包开发者仍需验证公钥、保护私钥、安全生成随机数，并防止侧信道信息泄露。

 

用户界面和交易解析错误也不在算术证明的范围内。

Fiat Crypto 如何帮助区块链节点？

 

区块链节点可能需要验证数千个签名或密码学证明。

 

性能非常重要，因为低效的验证会降低交易吞吐量，并提高硬件要求。

 

正确性同样重要，因为不同节点必须对有效性得出相同结论。

 

罕见的算术结果不一致可能导致共识失败，例如某些实现接受一笔交易，而其他实现拒绝该交易。

 

经过验证的算术可以减少一种可能导致实现不一致的因素。

 

节点仍需进行共识测试、制定协议规范、保障网络安全和数据库安全，并完成全面的实现审查。

零知识系统如何从中受益？

 

零知识证明系统会执行大量有限域算术运算。

 

证明者和验证者可能使用多种不同的素数域。

 

域运算错误可能导致无效证明、错误拒绝或严重安全故障。

 

针对证明系统所用模数专门优化算术运算的代码生成器，可以提高可移植性和保证水平。

 

Fiat Crypto 不会自动生成完整的零知识证明系统。

 

多项式承诺、交互记录构造、证明方程、电路逻辑和密码学假设都需要单独实现和证明。

如何安全使用 Fiat Crypto

 

开发者应从官方代码库开始，并阅读最新的构建和后端文档。

 

他们应选择适用于相关模数和目标架构的受支持算术策略。

 

应检查生成的代码，使用受支持的设置进行编译，并针对独立的已知答案测试向量进行测试。

 

使用该代码的应用程序安全审查应记录项目的证明范围和后端限制。

 

开发者应测试格式错误的输入、边界值、最大进位、零值和非规范编码。

 

应在实际的编译器与硬件组合上评估侧信道行为。

 

对生成器、证明助手、编译器或后端进行更新后，应重新测试和审查。

 

生产团队不应把“形式化验证”视为跳过集成审计的理由。

Fiat Crypto 的优势

 

Fiat Crypto 针对重要的算术转换提供经机器检查的功能正确性证明。

 

它可以为多种素数模数和机器字长生成实现。

 

它减少了创建优化域算术代码时重复的手动工作。

 

与数千条手写底层操作相比，其高层规范更容易推理。

 

该项目是开源的，可以接受独立审查。

 

它支持可重复的代码生成，而不是只依赖来源不明的算术代码文件副本。

 

其生成程序已与广泛部署的密码学软件和大量测试套件集成。

Fiat Crypto 的局限

 

Fiat Crypto 只覆盖完整密码学软件栈的一部分。

 

不同后端所提供的证明保证有所不同。

 

构建和修改证明开发流程需要掌握 Coq、形式化方法、编译器和密码学算术等专业知识。

 

生成的源代码仍需经过普通编译器和平台工具链。

 

功能正确性并不会自动证明代码能够抵御所有侧信道攻击。

 

性能会因处理器和编译器而异。

 

不受支持的参数或停止维护的后端可能带来额外风险。

 

形式上正确地实现不安全的密码学设计，结果仍然是不安全的。

关于 Fiat Crypto 的常见误解

 

Fiat Crypto 不是加密货币。

 

它与政府发行的法定货币无关。

 

它不将现金兑换成数字资产。

 

它不是 Fiat–Shamir 变换。

 

它不会自动生成完整的区块链应用。

 

它无法证明所有使用其输出的程序都安全。

 

它不能免除测试和代码审查的必要性。

 

它不会对所有受支持的语言后端提供相同的证明保证。

 

它无法让弱密钥、不安全协议或不安全的钱包界面变得安全。

常见问题

什么是 Fiat Crypto？

 

Fiat Crypto 是一个开源项目，可根据高层规范生成高效的密码学算术代码，并提供经机器检查的正确性证明。

Fiat Crypto 是加密货币吗？

 

不是。它是一个软件验证和代码生成项目，而不是数字资产。

Fiat Crypto 与法定货币有关吗？

 

没有关系。它不发行、处理或兑换政府货币。

Fiat Crypto 和 Fiat Cryptography 是同一个项目吗？

 

是的，Fiat-Crypto 和 Fiat Cryptography 通常是同一项目和研究工作的不同名称。

谁开发了 Fiat Crypto？

 

该项目源自与 MIT 编程语言与验证研究组及外部贡献者相关的形式化验证和密码学实现研究。

Fiat Crypto 使用什么证明助手？

 

它使用 Coq 定义规范、实现转换并检查正确性证明。

Fiat Crypto 会生成什么类型的代码？

 

它主要生成用于密码学有限域的底层模算术程序。

Fiat Crypto 会生成 C 代码吗？

 

会，C 是其主要维护的输出目标之一。

Fiat Crypto 支持 Rust 吗？

 

代码库包含一个由外部维护的 Rust 后端，并对生成的代码进行测试。

Fiat Crypto 支持 Go 吗？

 

支持，其代码库列出了一个由外部维护的 Go 后端。

Fiat Crypto 支持 Zig 吗？

 

支持，代码库将 Zig 列为由外部维护的后端，并在测试中使用其生成代码。

是否建议使用 Java 后端？

 

当前代码库指出，Java 后端已停止维护，并且已知存在问题。

什么是有限域？

 

有限域是一个包含有限个值的集合，并具有许多密码算法使用的算术运算。

什么是 limb？

 

limb 是较大密码学整数中一个机器字长的部分。

什么是模约简？

 

模约简会将算术结果转换为相对于选定模数的等价值。

什么是 Montgomery 算术？

 

Montgomery 算术使用特殊的数值表示，在无需对模数进行普通除法的情况下高效执行模乘。

什么是 Solinas 算术？

 

Solinas 算术利用具有特定形式的素数模数，通过 2 的幂和较小常数实现高效约简。

Fiat Crypto 支持 Curve25519 算术吗？

 

支持。官方代码库包含 Curve25519 系列密码学所用素数的生成示例。

Fiat Crypto 支持 secp256k1 吗？

 

该项目包含与 secp256k1 相关的域和椭圆曲线工作，可用于区块链签名实现。

Fiat Crypto 会创建数字签名吗？

 

它会生成可用于签名实现的算术组件，但本身并不是完整的签名应用程序。

Fiat Crypto 能证明签名方案安全吗？

 

不能。算术的功能正确性与证明整个签名方案的数学安全性并不相同。

Fiat Crypto 能防止算术溢出吗？

 

其经过验证的流程会推理数值界限，并选择旨在容纳规范所涵盖中间值的整数大小。

Fiat Crypto 能保证代码以恒定时间执行吗？

 

其设计支持控制流固定的密码学算术运算，但完整的侧信道安全性取决于后端、编译器、处理器和外围应用程序。

测试可以取代 Fiat Crypto 的证明吗？

 

不可以。测试和形式化证明提供不同类型的保证，结合使用最为有效。

形式化验证可以取代安全审计吗？

 

不可以。审计还必须检查协议逻辑、集成、随机性、内存安全、密钥处理、侧信道和应用行为。

Fiat Crypto 的每个后端都经过形式化验证吗？

 

不是。代码库记录了其输出后端在证明、维护和测试方面的不同水平。

文档中保证程度最高的后端路径是什么？

 

Bedrock2 后端额外提供了一项证明，将其抽象语法树与 Fiat Crypto 的内部表示联系起来。

Fiat Crypto 为什么适用于区块链？

 

它可以减少区块链软件在处理数字签名、密钥、证明及其他加密算法计算时出现的算术实现错误。

Fiat Crypto 可以用于钱包吗？

 

生成的算术代码可以集成到钱包密码学中，但完整钱包仍需要单独进行安全工程。

Fiat Crypto 与法币兑换加密货币是一回事吗？

 

不是。法币兑换加密货币是一种使用政府货币购买数字资产的金融服务。

Fiat Crypto 和 Fiat–Shamir 是一回事吗？

 

不是。Fiat–Shamir 用于转换交互式证明，而 Fiat Crypto 用于合成经过验证的算术实现。

Fiat Crypto 是开源的吗？

 

是的。该项目以多种宽松的开源许可证公开发布，具体许可证选择见其代码库文档。

结论

 

Fiat Crypto 是一个形式化验证和代码生成系统，用于生成高效的密码学算术代码。

 

它使开发者能够以高层方式描述模运算，并通过经机器检查的转换推导出底层实现。

 

该项目与加密货币密切相关，因为区块链签名、公钥、钱包、节点和零知识系统都依赖正确的有限域算术。

 

Fiat Crypto 可以针对重要素数域以及 Solinas 和 Montgomery 算术等实现策略生成运算代码。

 

它支持维护中的 C 和 Bedrock2/C 路径，以及由外部维护的语言后端。

 

具体保证程度取决于所选后端和形式化证明的范围。

 

形式化验证可以降低算术错误的风险，但无法证明完整密码学应用的所有属性。

 

开发者仍需审查协议安全性、私钥处理、随机性、序列化、编译器行为、硬件行为和侧信道防护。

 

因此，应将 Fiat Crypto 理解为构建高保证密码学软件的强大基础，而不是测试、审计和安全系统设计的完整替代方案。