低信任架构的安全验证
2023年8月21日·
,
,
,
,
,
·
0 分钟阅读时长
Qinhan Tan
Yonathan Fiesseha
陈士博
Lauren Biernacki
Jean-Baptiste Jeannin
Sharad Malik
Todd Austin
摘要
低信任架构从软件视角看，始终处理加密数据，并将硬件信任边界显著收缩到一个无软件参与的小型 enclave 组件。本文对一种具体低信任架构 Sequestered Encryption（SE）进行完整形式化验证，证明其在所有程序下都能抵御直接数据泄露与数字侧信道泄露。我们首先定义 SE 架构 ISA 层的安全需求。向上看，该 ISA 作为软件可见的硬件抽象，用于证明任何由这些指令组成的程序都不会泄露信息（包括数字侧信道）；向下看，该 ISA 又是硬件实现规范，用于导出 RTL 实现需满足的证明义务，覆盖功能正确性与数字侧信道安全。随后，我们展示如何借助商用形式化验证工具完成这些证明义务。最后，我们在 7 个正确与缺陷并存的 SE 架构实现上验证了该 RTL 安全验证方法的有效性。
类型
出版物
发表在 The ACM Conference on Computer and Communications Security 2023
