Randomizing snake-oil

Posted May 13, 2017 18:04 UTC (Sat) by NAR (subscriber, #1313)
In reply to: Randomizing snake-oil by ebiederm
Parent article: Randomizing structure layout

"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.