3 ms·

I wonder, with formal verification being a thing, could you formally verify that a chip would be resistant to all types of power attacks according to the curren

I wonder, with formal verification being a thing, could you formally verify that a chip would be resistant to all types of power attacks according to the current laws of physics? Such a proof can never be final, because the laws of physics aren't either. But just because it's not perfect doesn't mean it wouldn't be good.

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.
wyldfire 7y ago
I think formal methods are all using some kind of discrete logic. Implementing physics with these things sounds really, really, hard. I guess designing your model would require feedback from layout and fabrication techniques, and it would suffer this same maintenance burden. Once you have the simulation, it would take ages of computation power (much more than functional RTL simulations do). I think this is the kind of thing that might happen in 2050 but for now it just sounds infeasible.
wmf 7y ago
Undervolting glitches are a fundamental property of synchronous logic and can't be fixed. Asynchronous logic, OTOH...
trevyn 7y ago
Probably not, because you can inject voltage in an effectively infinite number of physical locations. (For example, nondestructively, with RF.)

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.

wyldfire 7y ago

I think formal methods are all using some kind of discrete logic. Implementing physics with these things sounds really, really, hard. I guess designing your model would require feedback from layout and fabrication techniques, and it would suffer this same maintenance burden. Once you have the simulation, it would take ages of computation power (much more than functional RTL simulations do). I think this is the kind of thing that might happen in 2050 but for now it just sounds infeasible.

wmf 7y ago

Undervolting glitches are a fundamental property of synchronous logic and can't be fixed. Asynchronous logic, OTOH...

trevyn 7y ago

Probably not, because you can inject voltage in an effectively infinite number of physical locations. (For example, nondestructively, with RF.)