Formal Verification of Data-Obliviousness in Hardware

Abstract:
The importance of preventing microarchitectural timing side channels in security-critical applications has surged in the last years. Constant-time programming has emerged as a best-practice technique to prevent leaking secret information through timing. It relies on the assumption that the timing of certain basic machine instructions is independent of their respective input data. However, whether an instruction fulfills this data-independent timing criterion varies between processor microarchitectures. In this overview paper, we present a recently published methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. In addition, recent enhancements that enable scalability even to complex out-of-order cores are sketched.