Re:Formal Verification Creates Hacker-Proof Code
by sklivvz1971 on Friday October 21, 2016 @07:58PM
(#12766010)
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.
Re:Formal Verification Creates Hacker-Proof Code
by nickpsecurity on Friday October 21, 2016 @08:05PM
(#12766064)
"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...
Re:Formal Verification Creates Hacker-Proof Code
by Houshalter on Monday October 24, 2016 @01:43AM
(#12776912)
They said hacker proof code, not hacker proof hardware.
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