无需共享源代码的证明：SJV、SJP 与信任边界

在软件开发领域，有时你需要在不共享源代码的情况下证明软件按预期运行。本文探讨了一种在保持源代码私密的同时证明软件属性的方法。

理解面临的挑战

在处理软件时，尤其是在涉及专有组件或敏感数据的项目中，共享源代码可能会带来风险。通常的选择并不怎么吸引人。你可能不得不共享整个实现，这可能会暴露你的知识产权。或者，你可能不得不信任一份声称软件已通过验证的报告，但这往往缺乏透明度。

介绍 SJV 和 SJP

为了应对这些挑战，人们正在探索一种基于两个关键概念的新方法：SJV 和 SJP。

• SJV（软件验证合约）： 这是一份概述软件应具备属性的文档。它指明了需要证明的内容，而无需透露软件是如何构建的。
• SJP（软件论证证明）： 这是在验证过程中生成的证据。SJP 表明该软件符合 SJV 中定义的属性。

其基本思想是将软件的实现与合约及证明分离开来。这意味着源代码保留在开发者手中，而 SJV 和 SJP 则可以共享给接收方。

工作原理

以下是该流程工作原理的简要分解：

步骤 1：定义 SJV

开发者创建一个描述软件预期属性的 SJV。例如，它可以声明某个值绝不能超过定义的最大值。

步骤 2：生成 SJP

在根据 SJV 验证软件后，开发者会生成一个 SJP。该工件包含验证证据，其中包括：

• 验证清单
• 有关输入和配置的信息
• 验证结果
• 数学义务
• 完整性数据
• 清单签名

步骤 3：共享 SJV 和 SJP

开发者将 SJV 和 SJP 共享给接收方。接收方随后可以检查 SJV 以了解所声明的属性，并核验 SJP 的完整性。

步骤 4：验证声明

使用 Z3 等工具，接收方可以重放存储在 SJP 中的数学义务。这使得他们无需访问源代码即可验证 SJV 中提出的声明是否属实。

信任边界

在此过程中，一个重要的概念是 信任边界。这是系统中划分不同信任级别区域的一条分界线。例如，开发者信任自己的代码，但可能不放心将源代码提供给接收方。信任边界有助于明确哪些内容可以独立验证，哪些内容需要信任。

有两个关键陈述需要考虑：

• 陈述 A： 数学义务是有效的。
• 陈述 B： 这些义务是由开发者所声明的特定私有实现生成的。

SJP 有助于确立陈述 A，但在没有源代码的情况下无法证实陈述 B。

局限性与注意事项

尽管该方法提供了一种在不共享源代码的情况下验证软件属性的途径，但它也存在局限性。接收方必须确保 SJV 中概述的属性确实是他们所关心的。成功的验证仅能确认所定义的属性在建模范围内成立；它并不能保证软件没有错误。

为了加强出处证明，可以引入额外的机制，例如：

• 由独立审计人员审查源代码。
• 在受控环境中生成 SJP。
• 仅向受信任的第三方披露源代码。

结论

使用 SJV 和 SJP 的方法提供了一种更安全的方式来验证软件属性，而无需共享敏感的源代码。在当今信任与安全至关重要的软件环境中，这种方法尤为适用。

优点

• 无需公开源代码即可进行验证。
• 允许明确分离声明、证据与实现。
• 提供可独立验证的结构化证明。

缺点

• 不能保证软件没有错误。
• 依赖于接收方对 SJV 的理解和信任。
• 需要额外的机制来提供出处证明。

注意事项

本文仅供教育目的。在实际应用中，任何占位符值都必须替换为实际数据。读者在依赖相关声明之前，应先核对其原始来源。

常见问题

• 什么是 SJV？ — SJV 代表软件验证合约，它概述了软件模块应具备的属性。
• 什么是 SJP？ — SJP 代表软件论证证明，是一个包含证明软件模块满足其指定属性的证据的工件。
• 为什么分离 SJV 和 SJP 很重要？ — 它允许在不公开源代码的情况下验证软件属性，从而增强安全性和信任度。
• 在没有源代码的情况下如何进行验证？ — 通过使用 Z3 等工具重放存储在 SJP 中的数学义务。
• 什么是信任边界？ — 信任边界是一条概念上的分界线，用于划分系统内不同信任级别的区域。
• SJP 能保证软件的正确性吗？ — 不能，SJP 只验证特定属性，但不能保证软件没有错误。

标签

#software #verification #trust-boundary