随着我们的个人数据越来越多地用于从广告到金融再到医疗保健的许多应用中，保护敏感信息已成为计算架构的基本功能。处理此类数据的应用程序必须信任它们所依赖的系统软件，例如操作系统和虚拟机管理程序，但此类系统软件很复杂，并且通常存在可能会危及数据机密性和完整性的漏洞。

过去两年，哥伦比亚工程公司的研究人员一直与领先的半导体 IP 和软件设计公司 Arm 合作，解决这些漏洞。该团队现已推出 Arm 机密计算架构 (Arm CCA) 的关键验证技术，这是 Armv9-A 架构的一项新功能。该论文于 7 月 12 日在加利福尼亚州卡尔斯巴德举行的第 16 届 USENIX 操作系统设计与实现研讨会 (OSDI '22) 上发表，展示了 Arm CCA 固件原型的首次正式验证。

Arm CCA 依靠固件来管理硬件以实施其安全保证，因此固件的正确性和安全性至关重要。虽然许多以前的系统依赖于固件，但它们都不能保证固件没有错误。形式验证是一种相对较新的方法，目前用于保证软件/硬件的正确性。形式验证不是测试，而是使用数学模型来证明软件和硬件绝对正确，从而提供最高级别的正确性保证。

该研究的主要作者、博士生李旭鹏表示：“我们首次证明了固件的正确性和安全性，从而首次演示了由正式验证的固件支持的机密计算架构。” 顾荣辉的学生，唐家计算机科学助理教授，以及计算机科学教授兼软件系统实验室联席主任Jason Nieh。

虽然有很多方法可以验证简单程序的正确性，但它们并不适合像 CCA 固件这样复杂的东西，因此研究人员必须开发新的验证技术，以使验证 Arm CCA 固件成为可能。例如，CCA 固件专为可扩展性和性能而设计，因此它允许高度并发操作并将 C 代码和汇编代码混合在一起。通过使用细粒度同步方法和具有数据竞争的代码可以实现并发操作。

Arm CCA 的设计原则是不受信任的软件必须保留对管理硬件资源的控制权，因此一个关键的挑战是证明即使不受信任的软件可以随心所欲地夺走硬件资源，系统仍然是安全的。以前的方法无法验证具有此类属性的程序。这种新的验证技术足够强大，可以使用 C 代码和汇编代码验证并发固件。

“通过经典的软件测试技术确实很难发现错误，”另一位博士生李旭恒说。聂和顾的学生，共同创作了该作品。“因此，我们展示了形式验证技术的重要性和价值，最终结果是由经过验证的固件支持的机密计算架构的首次演示。”

该团队对新的验证技术感到非常兴奋，这些技术可用于证明 Arm CCA 底层固件实现的正确性。Arm CPU 已部署在全球数十亿台设备上。随着 Arm CCA 越来越普遍地用于保护用户的私有数据（尤其是在云服务及其他服务中），本文中演示的验证技术将在数据保护和安全性方面提供显着改进。

将正式方法应用于软件的挑战之一是在软件更新时需要调整证明。研究人员正在研究新技术，以帮助他们逐步、快速地验证 Arm CCA 固件的更新，并确保始终验证可用的最新固件。

Gu 和 Nieh 补充说，他们“从我们的工作中看到了形式验证的力量和潜力，我们相信形式验证是一项基本技术，在不久的将来，它将取代当前使用的软件测试。”

2023年 12 月 14 日 更新