Verifying Hardware Security with RTL Simulation

When you try to apply masking or hiding schemes to prevent side-channel leakage of logic (see [1]), the design tools will often optimize your designs away and make your logic insecure! The same goes for certain parity and polarity propagation schemes used to protect data on busses from snooping attacks.

[1] https://www.iacr.org/archive/ches2014/87310197/87310197.pdf

Slightly related to this article, if anyone is interested in playing with the Synopsys Verilog/VHDL synthesis tool (Synplify), there was a version bundled with the Lattice FPGA tools last time I used them. It was provided as an alternate to the Lattice Synthesis Engine, and it looks like that relationship continues [0]. I also just love Lattice FPGAs, and this article reminded me of that :)

0. https://www.latticesemi.com/en/About/Newsroom/PressReleases/...

https://m.youtube.com/watch?v=RqQhWitJ1As&t=3s&pp=ygUZQnVubm...

> 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_gl...

[1]: http://kastner.ucsd.edu/wp-content/uploads/2013/08/admin/icc...

[2]: https://kastner.ucsd.edu/wp-content/uploads/2013/08/admin/da...

I haven’t heard of any other languages that can perform runtime taint tracking.