3 ms·

An Intel CPU is a pretty large design. I'm not sure it's feasible to run all formal verification benchmarks on a full RTL design of the entire chip, including c

by q3k 7y ago

An Intel CPU is a pretty large design. I'm not sure it's feasible to run all formal verification benchmarks on a full RTL design of the entire chip, including caches, memory controllers, etc. Not to mention - these sort of fault injection attacks are way past issues in high-level RTL, and instead are in the post-synethesis, analog/metastable domain specific to a given target process. Simulating those effects sounds prohibitively expensive, and I'm not sure there is any existing formal verification suite that can even do that. Unless someone modeled at a higher-level that modifying an MSR can cause undervolting, and then this undervolting can in turn cause bitflips to occur, this wouldn't have been caught. And if they did model it, they would have probably thought of this attack anyway :).

kyboren 7y ago
> An Intel CPU is a pretty large design. I'm not sure it's feasible to run all formal verification benchmarks on a full RTL design of the entire chip, including caches, memory controllers, etc. Agreed. It's still possible to verify smaller components of the design, though. > [...] These sort of fault injection attacks are way past issues in high-level RTL. [...] Simulating those effects sounds prohibitively expensive, and I'm not sure there is any existing formal verification suite that can even do that. It's possible to have a "high-level RTL" design that inherently resists some types of fault injection attacks. TMR is a trivial example: https://en.wikipedia.org/wiki/Triple_modular_redundancy https://en.wikipedia.org/wiki/Triple_modular_redundancy In fact, there is a wide body of literature studying the application of formal verification to side-channel and fault-injection analysis. Some systems can even synthesize a fault-injection resistant design. Unfortunately it is not realistic to be resistant to "all types of [fault injection] attacks according to the current laws of physics". We can, however, make different models of fault attacks and then prove (or synthesize) that some design is resistant to attacks in that model. If you're interested, look for publications in CHES, TCAD, FMCAD, DAC, DATE, etc. with keywords like "DFA", "DFIA", "SAT", "fault injection", etc.

by q3k 7y ago

kyboren 7y ago

> An Intel CPU is a pretty large design. I'm not sure it's feasible to run all formal verification benchmarks on a full RTL design of the entire chip, including caches, memory controllers, etc. Agreed. It's still possible to verify smaller components of the design, though. > [...] These sort of fault injection attacks are way past issues in high-level RTL. [...] Simulating those effects sounds prohibitively expensive, and I'm not sure there is any existing formal verification suite that can even do that. It's possible to have a "high-level RTL" design that inherently resists some types of fault injection attacks. TMR is a trivial example: https://en.wikipedia.org/wiki/Triple_modular_redundancy https://en.wikipedia.org/wiki/Triple_modular_redundancy In fact, there is a wide body of literature studying the application of formal verification to side-channel and fault-injection analysis. Some systems can even synthesize a fault-injection resistant design. Unfortunately it is not realistic to be resistant to "all types of [fault injection] attacks according to the current laws of physics". We can, however, make different models of fault attacks and then prove (or synthesize) that some design is resistant to attacks in that model. If you're interested, look for publications in CHES, TCAD, FMCAD, DAC, DATE, etc. with keywords like "DFA", "DFIA", "SAT", "fault injection", etc.