问题

低信任架构让软件始终在加密数据上运算，并把需要信任的硬件缩小到一个不运行软件的小型 enclave。这类安全声明必须对所有程序、所有实现都成立，靠测试无法证明。

思路

我们在 Sequestered Encryption（SE）架构的 ISA 层定义安全需求。向上看，ISA 证明任何由这些指令组成的程序都不会泄露数据，无论是直接泄露还是数字侧信道。向下看，同一份 ISA 给出了每个 RTL 实现必须满足的证明义务，并用商用形式化工具完成证明。

Softwareany program on always-encrypted dataISA security specificationno disclosure, no digital side channelRTL implementations7 designs, correct and buggyholds forall programsproofobligations(formal tools)
一份 ISA 层规格覆盖所有程序，并约束每个 RTL 实现。

结果

7个 RTL 实现完成验证（含正确与有缺陷的版本）
🏆CCS 2023 Distinguished Paper Award

我的工作

共同第一作者（贡献相同）。

论文： CCS 2023