固件安全更新通过形式化验证

《ACM Transactions on Cyber-Physical Systems》：Firmware Secure Updates meet Formal Verification

工业物联网固件安全更新需应对厂商碎片化、网络限制及安全关键性挑战，本文扩展IETF SUIT框架，集成SBOM机制和行为认证清单，通过原型验证其可行性与可扩展性。

　　

摘要

工业物联网（IIoT）系统需要强大的机制来确保固件更新的安全性。由于供应商之间的差异、网络限制以及许多IIoT应用的安全关键性，现有的方法往往不够充分。在本文中，我们通过扩展IETF SUIT（物联网软件更新）框架来解决这些挑战，以提高固件更新的安全性和可靠性。我们的贡献包括将软件物料清单（SBOM）机制和行为认证清单整合到SUIT架构中，以增加透明度并对外部更新内容提供正式的保证。该方法通过一个原型实现进行了验证，该原型使用实际基准测试展示了其可行性和可扩展性。