zlacker

>>zxombi+(OP)
I wager it will be hacked in under a year.

>>pluton+Y7
Nobody's claiming it's "hack-proof", that would be foolish, just that it removes certain classes of vulnerabilities that are the majority of CVEs for code written in memory-unsafe languages, thereby reducing the attack surface. Independent analysis by both Microsoft and Google has shown that's around 70% of vulnerabilities, which still leaves around 30%, but is a big step forward.

>>jrtc27+Qc
Not OP, but that's not how I interpreted their comment. I interepreted it as the 70% they hope to have fixed will end up having edge cases not yet considered, and the protections will end up weaker than desired. No-one designed a processor to be susceptable to spectre and meltdown, once something moves into production there is significantly more incentive to investigate and find these flaws.

>>lacksc+hf
Exactly - these formal methods have implicit assumptions in them. Within their axioms/priors they are proven correct. But the devil is in those assumptions. And that is disregarding the rather foggy notion of 'proof'. Is this proof written in a formal proof system that automates the proof? Because if it isn't you have another source of error. Even if it is in a formal proof system, who is to say that there is no error in the formal proof system? I admit that each layer adds more assurance - but appealing to 'formal proof' is a bit like appealing to god, it's an appeal to an unassailable authority. When in fact, once you know the details these things are never so clear cut.