随着我们的个人数据越来越多地用于从广告到金融到医疗保健的许多应用程序，保护敏感信息已成为计算架构的一项基本功能。处理此类数据的应用程序必须信任其所依赖的系统软件，如操作系统和虚拟机监控程序，但此类系统软件很复杂，通常存在可能危及数据机密性和完整性的漏洞。
在过去两年中，哥伦比亚工程公司的研究人员一直在与领先的半导体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固件的更新，并确保始终验证可用的最新固件。
顾和聂补充说，他们“从我们的工作中看到了形式验证的力量和潜力，我们相信，形式验证是一种必要的技术，在不久的将来将取代当前使用的软件测试。”