基于泄漏契约的开源处理器侧信道安全性规约与验证
密码学与安全
2023-09-29 v2
摘要
泄漏契约近期被提出作为指令集架构（ISA）层的一种新安全抽象。此类契约旨在忠实刻画处理器可能通过其微架构实现的副作用所泄漏的信息。然而，迄今为止我们缺乏一种验证方法以检查处理器是否确实满足给定泄漏契约。本文通过开发 LeaVe 来解决该问题，LeaVe 是首个针对 ISA 层泄漏契约验证寄存器传输级（RTL）处理器设计的工具。为此，我们引入了一个解耦定理，在验证契约满足性时将安全性与功能正确性关注点分离。LeaVe 利用该解耦使契约满足性验证切实可行。为扩展到现实处理器设计，LeaVe 进一步在关系抽象上采用归纳推理。使用 LeaVe，我们精确刻画了三个开源 RISC-V 处理器所提供的侧信道安全保证，从而获得了首批 RTL 处理器设计的契约满足性证明。
引用
@article{arxiv.2305.06979,
title = {Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts},
author = {Zilong Wang and Gideon Mohr and Klaus von Gleissenthall and Jan Reineke and Marco Guarnieri},
journal= {arXiv preprint arXiv:2305.06979},
year = {2023}
}
备注
Technical report containing full formalization and proofs of all results. A short version of this report (with the same title) appears in the proceedings of the 30th ACM SIGSAC Conference on Computer and Communication Security (CCS 2023)