3 ms·

Side-channel attacks, attacks that depend on physical characteristics of the system, are a thing [0] and formal correctness doesn't really prevent them. Also t

by sklivvz1971 10y ago

Side-channel attacks, attacks that depend on physical characteristics of the system, are a thing [0] and formal correctness doesn't really prevent them. Also there's crazy stuff like Row Hammer [1] which depends on escaping the abstraction that memory bytes are independent entities. While these are maybe crazy or extreme attacks, they are still practical in some cases. Any abstraction can eventually be hacked simply because an abstraction is a simplification of a more complex system which can be manipulated. Reminds me of the joke of the junior functional programmer convinced that their code is side effects free and who then proceeds to crash the garbage collector because memory allocation is not considered a side effect... [0]: https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack [1]: https://en.wikipedia.org/wiki/Row_hammer https://en.wikipedia.org/wiki/Row_hammer

nickpsecurity 10y ago
I addressed this here: https://news.ycombinator.com/item?id=12762323 https://news.ycombinator.com/item?id=12762323 The military, EE's, and even RAM suppliers knew about those issues. There are products in high-security (esp Defense) that try to counter as many as they can afford to. The problem was the knowledge was ignored or intentionally not applied. The first just keeps happening in general in so-called INFOSEC. The second is a result of market incentives where the suppliers' goal is to hit specific performance, energy, area, cost, etc targets to maximize market share and profit. On cost, they also want to minimize that in general for the executives and shareholders to pocket more income. This really affects RAM vendors as people involved in QA have said on various forums that they're basically just pushed to get shit out the door as quickly as possible since competition is intense. That they do this with ever-increasing complexity in designs and physics in shrinking nodes means problems can only go up. So, it's not a new discovery in terms of hardware correctness or even an accident. These problems are intentionally there to increase profits. Compare that to the design of things like 1802, NonStop, AAMP7G, rad-hard ASIC's... all that trade off marketable criteria at higher prices to get higher reliability. They exist but almost nobody buys them. That's why such practices aren't and won't be status quo. EDIT to add NonStop link to show what earlier systems accomplished with careful hardware and software design. Similar, even more clever, techniques were used inside ASIC's as well. http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf
- sklivvz1971 10y ago
  The point that I was trying to make is that they have proven correctness within a specific abstraction, but the article incorrectly say the code is "hacker-proof". Hacking in most cases happens because we can break through abstractions.
  - nickpsecurity 10y ago
    "The point that I was trying to make is that they have proven correctness within a specific abstraction, but the article incorrectly say the code is "hacker-proof"." The title is terrible as several of us argued here. The article itself at least describes the process accurately with many quotes talking about how tricky it is or that you should test it anyway. Just a terrible title...
  - Houshalter 10y ago
    They said hacker proof code, not hacker proof hardware.

nickpsecurity 10y ago

I addressed this here: https://news.ycombinator.com/item?id=12762323 https://news.ycombinator.com/item?id=12762323 The military, EE's, and even RAM suppliers knew about those issues. There are products in high-security (esp Defense) that try to counter as many as they can afford to. The problem was the knowledge was ignored or intentionally not applied. The first just keeps happening in general in so-called INFOSEC. The second is a result of market incentives where the suppliers' goal is to hit specific performance, energy, area, cost, etc targets to maximize market share and profit. On cost, they also want to minimize that in general for the executives and shareholders to pocket more income. This really affects RAM vendors as people involved in QA have said on various forums that they're basically just pushed to get shit out the door as quickly as possible since competition is intense. That they do this with ever-increasing complexity in designs and physics in shrinking nodes means problems can only go up. So, it's not a new discovery in terms of hardware correctness or even an accident. These problems are intentionally there to increase profits. Compare that to the design of things like 1802, NonStop, AAMP7G, rad-hard ASIC's... all that trade off marketable criteria at higher prices to get higher reliability. They exist but almost nobody buys them. That's why such practices aren't and won't be status quo. EDIT to add NonStop link to show what earlier systems accomplished with careful hardware and software design. Similar, even more clever, techniques were used inside ASIC's as well. http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf http://www.hpl.hp.com/techreports/tandem/TR-86.2.pdf

sklivvz1971 10y ago
The point that I was trying to make is that they have proven correctness within a specific abstraction, but the article incorrectly say the code is "hacker-proof". Hacking in most cases happens because we can break through abstractions.
- nickpsecurity 10y ago
  "The point that I was trying to make is that they have proven correctness within a specific abstraction, but the article incorrectly say the code is "hacker-proof"." The title is terrible as several of us argued here. The article itself at least describes the process accurately with many quotes talking about how tricky it is or that you should test it anyway. Just a terrible title...
- Houshalter 10y ago
  They said hacker proof code, not hacker proof hardware.