Information Flow Tracking at RTL. Innovation in Verification

Explicit and implicit sneak paths to leak or compromise information continue to represent a threat to security. This paper looks a refinement of existing gate level information flow tracking (IFT) techniques extended to RTL, encouraging early-stage security optimization. Paul Cunningham (Senior VP/GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and now Silvaco CTO) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is Register Transfer Level Information Flow Tracking for Provably Secure Hardware Design. This article appeared at DATE 2017 and has gathered an impressive 53 citations. The authors are from the University of California San Diego.

This group earlier developed gate-level IFT (GLIFT) technology, launching as a product under Tortuga Logic (later rebranded as Cycuity). Information flow techniques offer a more general and formal approach to modeling and reasoning about security properties than testing by vulnerability use-cases. The method generalizes by propagating taint information alongside regular logic evaluation, flagging say a signal sourced from an insecure domain controlling a condition selection in a secure domain. Combining this with formal verification methods offers potential for strong security guarantees.

Extending analysis to RTL enable several improvements: scalability to larger circuits, application earlier in design and a somewhat improved understanding of higher-level dependencies in design intent without need for user-supplied annotations. The authors also describe a method by which designers can tradeoff between security and verification performance in serving differing market needs.

Paul’s view

Security verification is something I care about deeply – we can’t trust digital data without it, and this includes my own personal data! This month’s paper is an easy read highlighting one of the mainstream techniques in security verification: adding “tainted” (i.e. compromised or no longer trusted) bits to all signals in a design and enhancing gate models propagate tainted bits through gates as well as signal values.

Tainted bit propagation is conceptually almost identical to “X-propagation” in mainstream design verification flows: if a signal is tainted then it’s as if we don’t know its value since we don’t trust the value it has.

This paper proposes two things: first, doing tainted bit annotation and propagation at the RTL level rather than the gate level; and second, doing the equivalent of what mainstream EDA tools call “X-pessimism removal”. The latter refers to not marking the result of an operator as X simply because at least one of its inputs is X, but rather to mark it as X only if it truly is X based on the definition of that operator. For example, consider c = a & b. If a=0 then c=0 even if b is X. Equivalently, in security verification speak, if a=0 and a is not tainted, then c=0 and is not tainted even if b is tainted. Seems easy for “&”, gets a bit more tricky for if, else and case constructs.

As you can expect, the paper concludes with some benchmarking that clearly shows propagating tainted bits at RTL is much faster than at gate-level, and that “precise” tainted-bit propagation (i.e. tainted-bit pessimism removal) reduces the false positive rate for tainted-bits at design outputs by a significant %. All this benchmarking is done in a formal proof context, not a logic simulation context. Case closed.

Wish you all a Happy Holidays!

Raúl’s view

Information Flow Tracking (IFT) is a computer security technique which models how information propagates as a system computes. It was introduced back in the 70’s by Denning, a good introduction and survey can be found here. The basic idea is to label data with a security class and then track these labels as the data is used for computations. For the purposes of the reviewed paper, the label is just a bit indicating data is “taint” (label=1, untrusted).  The most conservative approach in using this label, is that the output of any operation involving taint data is taint; or said inversely, only operations with all input data being not taint yield a not taint output. The paper relaxes this approach somehow as I’ll explain later.

Computer security aims at maintaining information confidentiality and integrity. Confidentiality means that information is only disclosed to authorized entities. IFT verifies if secret information can ever be disclosed by tracking that all locations it flows to are also secret (not taint), e.g., a secret key does not leak outside a restricted memory space. Integrity is the inverse: to maintain the accuracy and consistency of data, untrusted entities are not allowed to operate on trusted information. How information flows throughout a computing system is crucial to determine confidentiality and integrity. IFT is among the most used techniques for modeling and reasoning about security.

The paper reviews existing IFT approaches at the gate level and RTL level. At the gate level reconvergence is a source of imprecision. In a multiplexer a taint select signal will yield a taint output even if both inputs are not taint. Modeling a multiplexer at the RTL level allows to fix this. Existing RTL level approaches involve the need of modifying the RTL code. The system implemented by the authors, RTLIFT, fixes both above shortcomings. It provides a library of RTL operators which allows to implement different approaches to IFT such at tainting outputs if any input is taint (conservative) or a more nuanced approach such as tainting outputs for a multiplexer only if one of the data inputs is taint (avoids false positives). It also provides an automatic translation of an RTL design in Verilog to an IFT-enhanced version which can be used for verification purposes.

The results on cryptographic cores show RTLIFT to be about 5 times faster than gate-level IFT (GLIFT). On a collection of 8 adders, multipliers, and control path logic, RTLIFT shows a 5%-37% decrease in false positives (false taint) over GLIFT for a simulation of 2²⁰ random input samples.

A comprehensive paper on security, that extends IFT to RTL, a very enjoyable read!

Also Read:

ML-Guided Model Abstraction. Innovation in Verification

Cadence Integrates Power Integrity Analysis and Fix into Design

Accelerating Development for Audio and Vision AI Pipelines