Constant-time foundations for the new spectre era
Constant-time foundations for the new spectre era
复制标题
DOI：
10.1145/3385412.3385970
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
Sunjay Cauligi;Craig Disselkoen;K. V. Gleissenthall;D. Tullsen;D. Stefan;Tamara Rezk;G. Barthe
中科院分区：
文献类型：
--
作者：
Sunjay Cauligi;Craig Disselkoen;K. V. Gleissenthall;D. Tullsen;D. Stefan;Tamara Rezk;G. Barthe
恒定时间原则是一种基于软件的对策，用于保护高保证加密实现免受定时边信道攻击。常数时间是有效的（它可以防止许多已知的攻击），严格的（它可以使用程序语义形式化），并服从自动验证。然而，微体系结构攻击的出现使得今天存在的恒定时间变得不那么有用。本文奠定了基础，在投机和乱序执行的存在下，常数时间编程。我们提出了一个操作语义和恒时程序的正式定义，在这个扩展的设置。我们的语义避免形式化的微架构功能（而不是假设对手的控制下），并产生一个概念的恒定时间，保持优雅和易处理的通常的概念。我们证明了我们的语义在两个方面的相关性：第一，通过对比现有的幽灵般的攻击与我们的定义的恒定时间。第二，通过实现一个静态分析工具，Pitchfork，它可以检测真实的世界密码库中违反我们扩展的恒定时间属性的行为。
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time is effective (it protects against many known attacks), rigorous (it can be formalized using program semantics), and amenable to automated verification. Yet, the advent of micro-architectural attacks makes constant-time as it exists today far less useful. This paper lays foundations for constant-time programming in the presence of speculative and out-of-order execution. We present an operational semantics and a formal definition of constant-time programs in this extended setting. Our semantics eschews formalization of microarchitectural features (that are instead assumed under adversary control), and yields a notion of constant-time that retains the elegance and tractability of the usual notion. We demonstrate the relevance of our semantics in two ways: First, by contrasting existing Spectre-like attacks with our definition of constant-time. Second, by implementing a static analysis tool, Pitchfork, which detects violations of our extended constant-time property in real world cryptographic libraries.