能否证明时间保护？
摘要：计时通道在计算机系统中是一个重要且不断增长的安全威胁，目前还没有确定的解决方案。我们最近认为，操作系统必须提供时间保护，类似于已经建立的内存保护，以保护应用程序不受通过计时通道泄露的信息。基于seL4微内核中最近提出的时间保护实现，我们研究了如何通过形式化证明来防止计时通道。我们假设通过推理共享的硬件资源的高度抽象化表示，应该可以实现这一点。
作者：Gernot Heiser and Gerwin Klein and Toby Murray
论文ID：1901.08338
分类：Operating Systems
分类简称：cs.OS
提交时间：2019-01-25