Randomizing snake-oil

Posted May 12, 2017 14:07 UTC (Fri) by ebiederm (subscriber, #35028)
In reply to: Randomizing snake-oil by matthias
Parent article: Randomizing structure layout

Provably secure is pretty much a non-starter as it requires a full and accurate theory of everything, and a proof the hardware you run on meets it's specification. Short of that you will have assumptions that may be wrong somewhere in your approach.

That said it is possible to manage the assumptions and prove certain properties about code. Which could in principle could close many lines of attack. The kernel deliberately does not implement any turning machines not even with eBPF so the halting problem should not be an issue.

The practical problem and what most attacks today exploit is that to be able to reason soundly about logic or algorithms requires the abstractions you build those out of to be well defined. Currently C explicitly is not well defined with respect to memory management. When you add in devices that can perform DMA and are not restricted by an IOMMU (as a kernel must) there is an additional problem.

To my knowledge no one has yet demonstrated a system that can build operating systems that is sufficiently well defined as to allow proofs of correctness for anything interesting. Which unfortunately leaves proofs of correctness needing a proof of concept before anyone will believe in them.

Which is all to say people are adding kernel defenses some of the randomization because no one has been clever enough yet to think of something better.

Randomizing snake-oil

Posted May 12, 2017 18:40 UTC (Fri) by walters (subscriber, #7396) [Link]

https://sel4.systems/ is pretty interesting on this topic. That said, I thought Coccinelle was an intimidating but https://github.com/seL4/l4v/commit/df7693b687a5ad541d1bee... is totally unintelligible to me. (Why are there almost no comments?)

Randomizing snake-oil

Posted May 13, 2017 18:04 UTC (Sat) by NAR (subscriber, #1313) [Link] (1 responses)

"To my knowledge no one has yet demonstrated a system that can build operating systems that is sufficiently well defined as to allow proofs of correctness for anything interesting"

I remember 20 years ago someone mentioned to me that the VMS kernel (the OS running on VAX computers) was formally proven to be correct (to some degree). Of course, in that case DEC provided the hardware and the software too. Unfortunately I don't remember the details.

Randomizing snake-oil

Posted May 18, 2017 0:52 UTC (Thu) by smoogen (subscriber, #97) [Link]

I was told by a Dec guy was that the original story was that with the right assumptions you could make anything provably secure and then showed how it could be done with the VMS system. You basically start by assuming all sorts of things like not having an active attacker, a set of actions that the system will only do, dropping down all the hardware to the bare minimum etc etc. All of these are things that various "provable" had used in one set or another.. so why not put them all together. You basically had a brick with VMS installed on it, but it was provable that it was secure within the parameters that could be used.

The problem was that the joke got out hand as someone took it seriously and started passing around about how VMS was superior to Unix because it was provably secure.

How true this story is versus all the others... I don't know.

Randomizing snake-oil

Posted May 25, 2017 20:47 UTC (Thu) by Wol (subscriber, #4433) [Link]

> Provably secure is pretty much a non-starter as it requires a full and accurate theory of everything, and a proof the hardware you run on meets it's specification. Short of that you will have assumptions that may be wrong somewhere in your approach.

A correctness proof is mathematics.

Hardware is reality.

Congratulations on finding a proof that reality and mathematics coincide ... :-)

Cheers,
Wol