Verifying Hardware Security with RTL Simulation(semiengineering.com)
semiengineering.com
Verifying Hardware Security with RTL Simulation
https://semiengineering.com/verifying-hardware-security-with-rtl-simulation/
6 comments
I'm seeing a fun resurgence of popularity with regards to deeply technical semiconductor articles here on HN lately! Seems almost daily there's a new semi engineering article or similar.
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/...
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/...
Somewhat related, but there is a great talk by Andrew "bunnie" Huang on hardware supply chain security:
https://m.youtube.com/watch?v=RqQhWitJ1As&t=3s&pp=ygUZQnVubm...
https://m.youtube.com/watch?v=RqQhWitJ1As&t=3s&pp=ygUZQnVubm...
We need open source chips, firmware, and supply chain surveillance to verify firmware, PCB, and chip designs are unmodified. This risks are too great to not assure that consumer and industrial products aren't being tampered with or contain backdoors.
Not sure why you’re being downvoted. Open source doesn’t necessarily fix these issues but a less opaque chain of trust would be helpful. It would be trivial to shove a backdoor into some open source riscv core or onto an open core platform. Open source doesn’t automatically mean secure.
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_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...
> 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...
Perl 5 supports this too!
I haven’t heard of any other languages that can perform runtime taint tracking.
I haven’t heard of any other languages that can perform runtime taint tracking.
Ruby (probably inspired by Perl), but removed now: https://blog.saeloun.com/2020/02/18/ruby-2-7-access-and-sett...
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