A Scalable Formal Verification Methodology for Data-Oblivious Hardware

arXiv:2308.07757v2 Announce Type: replace
Abstract: The importance of preventing microarchitectural timing side channels in security-critical applications has surged in recent years. Constant-time programming has emerged as a best-practice technique for preventing the leakage of secret information through timing. It is based on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether or not an instruction satisfies this data-independent timing criterion varies between individual processor microarchitectures. In this paper, we propose …

applications arxiv basic critical cs.cr data hardware information machine methodology oblivious practice programming secret security verification