Comment My experience with formally proven OS in the 80's (Score 2, Interesting) 517
This Slashdot article, referring to the so called "World's First Formally-Proven OS Kernel",was brought to my attention by a colleague who is aware of my experience with formally proven OS' in the 1980's. What follows is my response to the claim of being first, and the value of proving the correctness of an OS:
I am aware of at least two instances of operating system kernels that were built in the late 1970's / early 1980's using formal proofs of correctness. I will talk about my experience with one of them.
One of them, produced in the late 1970's was a kernel designed for a specialized environment. This kernel/OS was a reasonably functional kernel complete with multiprocessing, time-sharing, file systems, etc. Unfortunately while the formal proof for this kernel was solid, the axiomatic set on which this formal proof was based did not perfectly match its operating environment. This mismatch proved to be fatal to the OS security.
This formally proven OS took years to create and prove its correctness. Those who developed and maintained the OS were very proud of their work. There were plans underway to create a commercial version of their work and to market it through a certain hardware vendor on which their OS ran.
When I was a student intern working for the organization where that developed this OS worked, I worked in their OS environment from time to time. I came in from the outside where my OS experience was with a wide variety OS' such as MVS, NOS, KRONOS, TOPS-10, RSTS/E, VMS, Multics, and Unix (5th/6th/7th edition). I had enough experience in jumping into new OS environments that I felt comfortable as a user in this one, even though it was unusual.
An important point to observe here is I was one of the first people who enter this OS environment from the outside. I was not steeped in the development world of the OS. I brought with me, ideas that differed from the OS developers. As a young student, I believed that the OS should work for me instead of getting in my way. To help come up to speed, I ported over my collection of OS-independent tools and soon began coding away on my assigned tasks.
Then one day, working within my OS-independent tools, something very odd happened. By mistake, I did something that produced an unusual result. I quickly realized that something was very wrong because the result was "impossible" according to the formal proof of OS correctness. Under the rules set down by my employer I immediately contacted the appropriate security officer and the next thing I knew, I was in a long sequence of meetings with people trying to figure out what in the hell happened.
In the first meeting after my mistake, I learned that I had been reassigned to a new team. I was assured that I was not being disciplined, far from it: I had made a number of people very happy and they moved paperwork mountains to move me into their team. This team was given a task of attempting to repeat my previous "mistake" as well as to discover if exploits that are more general were possible against this OS. We were assigned to work âoeundercoverâ as developers under test/QA installations using this OS. In the end, the team was successful in discovering a much more general form of the OS hole I accidentally found.
What went wrong with the OS formal proof? Well the mapping from the formal logic world to the real world of hardware, physics, people, and the environment was flawed. In other words, when you added in the "real-world", the proof was incomplete. Attempts by the OS developers to expand their proof to address the "real-world" only produced a set of inconsistent theorems. I believe the OS project was abandoned after the OS developers failed multiple times to expand their formal proof to deal with âoereal-worldâ environments.
During this experience I was introduced to two "Security Camps": One, "the absolutists" as they called themselves, included people who worked on this formally proven OS. The opposing camp called themselves "the relativists" as a sign of opposition to the ideas put forward by "the absolutists". While there were many who saw value in both camps, some zealots saw their way as the only true way.
Allow me to state the extreme positions of both camps:
The extreme members of "the absolutists" believed that perfection in security could be obtained by starting with a small and provably secure axiomatic environment. The level of security could be maintained while the environment expanded through formal disciplines and procedures that were controlled by the security of the lower levels. In other words, they believed you could start with a small secure core and formally build on that core while maintaining provable security.
The extreme members of âoethe relativistsâ believed nothing was secure. They believed the products of "the absolutists" were, inconsistent (due to flaws in their proofs), incomplete (as I unknowingly demonstrated in my OS exploit), or trivial (to be so constrained as to be of limited practical value). I recall one member of the OS exploit team to which I had been reassigned, a particular zealot of "the relativists" camp would often say:
"All security is ultimately FUBARed. So for those things your security cannot prevent, try to mitigate the damage. All mitigation systems are ultimately FUBARed. So for those events your security cannot mitigate, try to at least detect attacks. All detection systems are ultimately FUBARed. For those situations that your detection systems cannot detect, life's a bitch." [ See FUBAR ]
Yes, he was a cheery fellow. :-)
Both camps have their good points. The zealots of both camps take things too far. Nevertheless, given the choice, I prefer to stay away from the absolutist camp.
I believe history shows that the relativists often are able to break systems constructed by the absolutists. Allow me to site a few examples/legends:
I am aware of at least two instances of operating system kernels that were built in the late 1970's / early 1980's using formal proofs of correctness. I will talk about my experience with one of them.
One of them, produced in the late 1970's was a kernel designed for a specialized environment. This kernel/OS was a reasonably functional kernel complete with multiprocessing, time-sharing, file systems, etc. Unfortunately while the formal proof for this kernel was solid, the axiomatic set on which this formal proof was based did not perfectly match its operating environment. This mismatch proved to be fatal to the OS security.
This formally proven OS took years to create and prove its correctness. Those who developed and maintained the OS were very proud of their work. There were plans underway to create a commercial version of their work and to market it through a certain hardware vendor on which their OS ran.
When I was a student intern working for the organization where that developed this OS worked, I worked in their OS environment from time to time. I came in from the outside where my OS experience was with a wide variety OS' such as MVS, NOS, KRONOS, TOPS-10, RSTS/E, VMS, Multics, and Unix (5th/6th/7th edition). I had enough experience in jumping into new OS environments that I felt comfortable as a user in this one, even though it was unusual.
An important point to observe here is I was one of the first people who enter this OS environment from the outside. I was not steeped in the development world of the OS. I brought with me, ideas that differed from the OS developers. As a young student, I believed that the OS should work for me instead of getting in my way. To help come up to speed, I ported over my collection of OS-independent tools and soon began coding away on my assigned tasks.
Then one day, working within my OS-independent tools, something very odd happened. By mistake, I did something that produced an unusual result. I quickly realized that something was very wrong because the result was "impossible" according to the formal proof of OS correctness. Under the rules set down by my employer I immediately contacted the appropriate security officer and the next thing I knew, I was in a long sequence of meetings with people trying to figure out what in the hell happened.
In the first meeting after my mistake, I learned that I had been reassigned to a new team. I was assured that I was not being disciplined, far from it: I had made a number of people very happy and they moved paperwork mountains to move me into their team. This team was given a task of attempting to repeat my previous "mistake" as well as to discover if exploits that are more general were possible against this OS. We were assigned to work âoeundercoverâ as developers under test/QA installations using this OS. In the end, the team was successful in discovering a much more general form of the OS hole I accidentally found.
What went wrong with the OS formal proof? Well the mapping from the formal logic world to the real world of hardware, physics, people, and the environment was flawed. In other words, when you added in the "real-world", the proof was incomplete. Attempts by the OS developers to expand their proof to address the "real-world" only produced a set of inconsistent theorems. I believe the OS project was abandoned after the OS developers failed multiple times to expand their formal proof to deal with âoereal-worldâ environments.
During this experience I was introduced to two "Security Camps": One, "the absolutists" as they called themselves, included people who worked on this formally proven OS. The opposing camp called themselves "the relativists" as a sign of opposition to the ideas put forward by "the absolutists". While there were many who saw value in both camps, some zealots saw their way as the only true way.
Allow me to state the extreme positions of both camps:
The extreme members of "the absolutists" believed that perfection in security could be obtained by starting with a small and provably secure axiomatic environment. The level of security could be maintained while the environment expanded through formal disciplines and procedures that were controlled by the security of the lower levels. In other words, they believed you could start with a small secure core and formally build on that core while maintaining provable security.
The extreme members of âoethe relativistsâ believed nothing was secure. They believed the products of "the absolutists" were, inconsistent (due to flaws in their proofs), incomplete (as I unknowingly demonstrated in my OS exploit), or trivial (to be so constrained as to be of limited practical value). I recall one member of the OS exploit team to which I had been reassigned, a particular zealot of "the relativists" camp would often say:
"All security is ultimately FUBARed. So for those things your security cannot prevent, try to mitigate the damage. All mitigation systems are ultimately FUBARed. So for those events your security cannot mitigate, try to at least detect attacks. All detection systems are ultimately FUBARed. For those situations that your detection systems cannot detect, life's a bitch." [ See FUBAR ]
Yes, he was a cheery fellow.
Both camps have their good points. The zealots of both camps take things too far. Nevertheless, given the choice, I prefer to stay away from the absolutist camp.
I believe history shows that the relativists often are able to break systems constructed by the absolutists. Allow me to site a few examples/legends:
- The absolutists built the impenetrable walls of the City of Troy [ http://en.wikipedia.org/wiki/Troy_VII ]. The relativists hacked Troy's defenses resulting in the sacking of the city. [ http://en.wikipedia.org/wiki/Trojan_War#Trojan_Horse ]
- The absolutists built the Maginot Line of defense [ http://en.wikipedia.org/wiki/Maginot_Line ]. The relativists hacked this line of defense [ http://en.wikipedia.org/wiki/Maginot_Line#German_invasion_in_World_War_II ].
- The absolutists believed the Enigma machine was unbreakable [ http://en.wikipedia.org/wiki/Enigma_machine ]. The relativists, and in particular Marian Rejewski et al. and later Alan Turing et al. hacked the cipher. [ http://en.wikipedia.org/wiki/Cryptanalysis_of_the_Enigma#Polish_breakthrough and http://en.wikipedia.org/wiki/Alan_Turing#Cryptanalysis ]
I will not be surprised to learn sometime in the future that a relativist minded hacker has managed to instruct the absolutists who have created the so-called "World First Formally-Proven OS Kernel".
chongo (Landon Curt Noll)
p.s. What about that other OS instance (that was proven in the late 1970's / early 1980's)? When I left, I was not aware of any successful attack on that other OS. It might be that the lack of a documented successful attack on that other OS was due the to fact that its capabilities was so limited as to be almost useless.
