幽灵时代内核的安全性（扩展版）
密码学与安全
2025-04-14 v2
摘要
Abadi 等人曾在共享内存模型中正式证明了地址空间布局随机化的有效性，但这依赖于对受害者程序的特定假设。然而，现代操作系统在内核中实现布局随机化，与这些假设不同，并且运行在通过系统调用进行通信的独立内存模型上。在这项工作中，我们放宽了 Abadi 等人的语言假设，同时证明了在具有内存隔离的系统中，布局随机化提供了可比较的安全保证。然而在实践中，推测执行和侧信道被认为是布局随机化的已知威胁。我们表明，对于能够使用侧信道和推测执行的攻击者，内核安全性无法恢复，并引入了一个新条件，使我们能够在幽灵时代正式证明内核安全性。我们的研究表明，在该条件下，系统无需依赖布局随机化即可保持安全。我们还证明了我们的条件可以合理地弱化，从而产生能够保证幽灵时代安全系统调用内核安全性的执行机制。
引用
@article{arxiv.2406.07278,
title = {On Kernel's Safety in the Spectre Era (Extended Version)},
author = {Davide Davoli and Martin Avanzini and Tamara Rezk},
journal= {arXiv preprint arXiv:2406.07278},
year = {2025}
}