Towards a Formally Verified Hardware Root-of-Trust for Data-Oblivious Computing*
TimeWednesday, July 13th4:50pm - 5:10pm PDT
Location3005, Level 3
Event Type
Research Manuscript
Hardware Security: Primitives, Architecture, Design & Test
DescriptionConstant-time programming has emerged as a best-practice technique to prevent leaking secret information through timing side channels.
It builds on the assumption that certain basic machine instructions execute timing-indepently w.r.t. their input data.
However, whether or not individual instructions have this property may vary strongly between processor implementations.
Subtle optimizations of the microarchitecture can render the assumption of timing independence invalid.
In this paper, we propose a novel methodology to formally verify data-oblivious behavior of hardware using standard property checking techniques.
We evaluate the proposed methodology in multiple case studies, ranging from small arithmetic cores to medium-sized processors.