开源RISC-V处理器精确且可靠的泄漏契约自动合成
密码学与安全
2025-09-09 v1
摘要
泄漏契约已被提出作为指令集架构层面的一种新的安全抽象。泄漏契约旨在捕获处理器可能通过微架构侧信道泄露的信息。最近，第一个用于验证处理器是否满足给定契约的工具应运而生。然而，为给定处理器提出一个既可靠又精确的契约具有挑战性、耗时且容易出错，因为这需要对微架构优化引入的时序侧信道有深入的了解。在本文中，我们通过提出LeaSyn来解决这一挑战，LeaSyn是第一个用于自动合成既可靠又精确的泄漏契约的工具，适用于寄存器传输级（register-transfer level）的处理器设计。从一个捕获可能契约空间、用户提供的契约模板出发，LeaSyn自动构建一个契约，在基于处理器泄漏经验特征的契约合成（确保精确性）和基于契约验证（确保可靠性）之间交替进行。使用LeaSyn，我们为各种契约模板自动合成了六个开源RISC-V CPU的契约。我们的实验表明，LeaSyn的契约是可靠的，并且比现有方法构建的契约更精确（即更忠实地表示目标处理器中的实际泄漏）。
引用
@article{arxiv.2509.06509,
title = {Synthesis of Sound and Precise Leakage Contracts for Open-Source RISC-V Processors},
author = {Zilong Wang and Gideon Mohr and Klaus von Gleissenthall and Jan Reineke and Marco Guarnieri},
journal= {arXiv preprint arXiv:2509.06509},
year = {2025}
}
备注
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 32nd ACM SIGSAC Conference on Computer and Communication Security (CCS 2025)