Hacker News Reader

Comment by lacksconfidence | Hacker News Reader

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.

View on HN

We do have formal proofs of various security properties at the architectural level that consider the entire architecture with all its complexities and warts. Speculative execution is of course a concern (and is an active area of research for us), though our belief is that the bounds information now present at the hardware level allows it to be tamed. Another concern is the interaction between undefined behaviour and CHERI; the former needs to be sufficiently constrained in order to not inadvertently turn code that would be memory safe with a naive CHERI compiler into code that is not. We also know there are still memory safety-like issues we can't protect against; we can stop pointer injection, but we can't stop tricking programs into copying the "wrong" pointer somewhere, or type confusion bugs that result in using pointers in an unintended way. Many of those exploit chains today rely on exploiting some other memory safety vulnerability we do protect against, but we cannot predict if people will come up with alternative approaches that avoid those in a world with CHERI.

Thank you. Your response's here and throughout this thread have been quite enlightening.

There are no CVEs related to Solaris SPARC Application Data Integrity, or Unisys ClearPath MCP.

Either they aren't interesting for hackers, or they actually did a good job with hardware memory tagging.

I might imagine the former over latter

Might be, then again most of their customers are government agencies, not really something that hackers care about.

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.

Reply on news.ycombinator.com