I don't have any experience with Synopsys's system here, and I don't want to fill out a contact form to download their whitepaper, but I have some experience wi

I don't have any experience with Synopsys's system here, and I don't want to fill out a contact form to download their whitepaper, but I have some experience with information flow tracking. > Any simulator capable of security verification must be able to apply taints and track their propagation through the RTL design. The simulator must have an “algebra” to model how taints propagate through all types of RTL code constructs and design elements. Finally, taints must check for security vulnerabilities while not modifying the design behavior. This paragraph is hiding some real difficulties and limitations with information flow tracking models. Generating completely precise (i.e. no false negatives, no false positives) taint propagation logic is an NP-hard problem[0] that is intractable for practical circuits (at least for gate-level IFT, probably also for RTL-level IFT). Thus a more relaxed approach (called the 'Constructive Approach' in the above-cited paper) is generally used, which introduces many false-positives, reducing the SnR for real information flows along with the utility of taint propagation modeling. To make matters worse, SAT queries on these already-imprecise GLIFT models might take weeks or months, if they ever terminate. There are some attempts at optimizing or simplifying the GLIFT models to be more tractable[1][2], but realistically you're still probably left with simulation and/or dynamic taint tracking. Don't get me wrong, simulation with IFT models could be very useful and help catch lots of bugs, but I'm skeptical of calling it "verifying hardware security", especially when even an unobtainable perfectly precise GLIFT model leaves open the possibility of information flows due to analog physical design effects beyond the scope of the model (e.g. RowHammer). [0]: https://cseweb.ucsd.edu/~kastner/papers/tifs12-complexity_glift.pdf https://cseweb.ucsd.edu/~kastner/papers/tifs12-complexity_gl... [1]: http://kastner.ucsd.edu/wp-content/uploads/2013/08/admin/iccad16-imprecise_security.pdf http://kastner.ucsd.edu/wp-content/uploads/2013/08/admin/icc... [2]: https://kastner.ucsd.edu/wp-content/uploads/2013/08/admin/dac17-arbitrary_precision_glift.pdf https://kastner.ucsd.edu/wp-content/uploads/2013/08/admin/da...