4 ms·

Verifying Hardware Security with RTL Simulation

15 points by kungfudoi 3y ago

stn8188 3y ago
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/2019/201922LatticeSynthesisEngine https://www.latticesemi.com/en/About/Newsroom/PressReleases/...
hedora 3y ago
Perl 5 supports this too! I haven’t heard of any other languages that can perform runtime taint tracking.
- lmz 3y ago
  Ruby (probably inspired by Perl), but removed now: https://blog.saeloun.com/2020/02/18/ruby-2-7-access-and-setting-of-safe-warned-will-become-global-variable/ https://blog.saeloun.com/2020/02/18/ruby-2-7-access-and-sett...
1letterunixname 3y ago
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.
- matthewfcarlson 3y ago
  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.
zachbee 3y ago
I'm a hardware security engineer, and I've actually used similar tools before! It's nifty, but overall, hardware security tooling is unfortunately seriously lacking. 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 https://www.iacr.org/archive/ches2014/87310197/87310197.pdf
andutu 3y ago
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=ygUZQnVubmllIGh1YW5nIG5hdGlvbiBzdGF0ZQ%3D%3D https://m.youtube.com/watch?v=RqQhWitJ1As&t=3s&pp=ygUZQnVubm...
kyboren 3y ago
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...

15 points by kungfudoi 3y ago

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/2019/201922LatticeSynthesisEngine https://www.latticesemi.com/en/About/Newsroom/PressReleases/...

hedora 3y ago

Perl 5 supports this too! I haven’t heard of any other languages that can perform runtime taint tracking.

lmz 3y ago
Ruby (probably inspired by Perl), but removed now: https://blog.saeloun.com/2020/02/18/ruby-2-7-access-and-setting-of-safe-warned-will-become-global-variable/ https://blog.saeloun.com/2020/02/18/ruby-2-7-access-and-sett...

1letterunixname 3y ago

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.

matthewfcarlson 3y ago
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.

zachbee 3y ago

I'm a hardware security engineer, and I've actually used similar tools before! It's nifty, but overall, hardware security tooling is unfortunately seriously lacking. 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 https://www.iacr.org/archive/ches2014/87310197/87310197.pdf

andutu 3y ago

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=ygUZQnVubmllIGh1YW5nIG5hdGlvbiBzdGF0ZQ%3D%3D https://m.youtube.com/watch?v=RqQhWitJ1As&t=3s&pp=ygUZQnVubm...

kyboren 3y ago

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