NPA

FAQ

常见问题

关于形式化验证、证书和审计策略的常见问答。

NPA 与标准 Lean kernel check 有什么不同?
标准 Lean checking 会在本地编译并验证文件。NPA 使用这些已验证的编译输出,配上确定性 hash,并封装为密码学签名证书(.npcert)。这样第三方用户无需重新编译或重新运行可能耗时数小时的证明搜索,也可以快速审计验证状态。
如何防止证书被篡改?
NPA 证书包含 module export data 的密码学签名 SHA-256 hash。站点生成器会验证磁盘上的实际文件与这些 hash 一致,reference checker 还会用 repositories.yaml 中登记的 trusted key 验证 producer 签名。
为什么一些 module source block 标为非可信 sidecar?
为保持严格安全性,只有 kernel 验证过的证明和签名(.npcert)代表可信证据。源代码文本、注释和 overlay 都被视为 metadata sidecar。即使源文本被修改,底层密码学检查仍能保证已验证定理本身不受影响。
checker 可以离线运行吗?
可以。NPA CLI 设计为可完全离线运行。下载包及其证书后,即可在本地无网络环境中验证全部内容。