一篇题为“前景:可证明的安全投机恒定时间政策(扩展版)”的技术论文由imec-DistriNet在KU Leuven, CEA, List, Université Paris Saclay和INRIA的研究人员发表。
文摘:
“我们提出了ProSpeCT，一个通用的形式化处理器模型，为常数时间策略提供可证明的安全推测。对于非推测性语义下的常数时间程序，ProSpeCT保证推测性和乱序执行不会导致微架构泄漏。这种保证是通过跟踪处理器管道中的秘密并确保它们在推测执行期间不会影响微架构状态来实现的。我们的形式化方法涵盖了一大类推测机制，概括了之前的工作。因此，我们的安全证明涵盖了所有已知的Spectre攻击，包括负载值注入(LVI)攻击。
除了正式模型之外，我们还提供了一个基于RISC-V处理器的ProSpeCT原型硬件实现，并证明了它对硬件成本、性能和所需软件更改的低影响。特别是，实验评估证实了我们的预期，对于兼容的常数时间二进制文件，启用ProSpeCT不会引起性能开销。”
找到这里是技术文件．2023年2月。第32届USENIX安全研讨会(2023)接受的论文技术报告。
作者:丹尼尔,Lesly-Ann;Bognar Marton;Noorman工作;Bardin Sebastien;Rezk,塔玛拉;Piessens,弗兰克。v1 arXiv: 2302.12108
Imec的计算路线图;美国对华为为目标;美印。特遣部队;China-Bolivia交易;布鲁克揭开了白光干涉测量系统;三星量化可持续性;麦肯锡指出了美国晶圆厂建设的问题;发光二极管。
留下回复