Register transfer level information flow tracking for provably secure hardware design

TLDR

Information Flow Tracking (IFT) is a formal method for modeling security properties such as integrity, confidentiality, and side‑channel resistance, and has recently been applied to secure hardware design, but existing hardware‑level IFT approaches either require rewriting specifications in a new language or fail to scale to large designs. This work proposes Register Transfer Level IFT (RTLIFT) to enable early‑phase verification of security properties directly on RTL code at a higher abstraction level. RTLIFT precisely models all logical flows in RTL designs and allows designers to adjust IFT precision trade‑offs. RTLIFT achieves more than five‑fold speedup over gate‑level IFT while reducing the effort required for designers to verify security properties on RTL designs.

Abstract

Information Flow Tracking (IFT) provides a formal methodology for modeling and reasoning about security properties related to integrity, confidentiality, and logical side channel. Recently, IFT has been employed for secure hardware design and verification. However, existing hardware IFT techniques either require designers to rewrite their hardware specifications in a new language or do not scale to large designs due to a low level of abstraction. In this work, we propose Register Transfer Level IFT (RTLIFT), which enables verification of security properties in an early design phase, at a higher level of abstraction, and directly on RTL code. The proposed method enables a precise understanding of all logical flows through RTL design and allows various tradeoffs in IFT precision. We show that RTLIFT achieves over 5x speedup in verification performance as compared to gate level IFT while minimizing the required effort for the designer to verify security properties on RTL designs.