Become a fan of Slashdot on Facebook


Forgot your password?
DEAL: For $25 - Add A Second Phone Number To Your Smartphone for life! Use promo code SLASHDOT25. Also, Slashdot's Facebook page has a chat bot now. Message it for stories and more. Check out the new SourceForge HTML5 internet speed test! ×

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 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) /\oo/\

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.

Comment English name, and other forms of the new Mersenne (Score 1) 89

The link on the GIMPS home page points to where one may obtain the decimal digits of the new Mersenne Prime. Other forms of this prime are available:

The dashed form of the English name is available at assist those who might actually want to read all or part of the +324 Megabyte name. :-)

Comment Let an Apple tech physically disable the camera (Score 4, Informative) 442

You can have the camera/microphone removed from your Apple MacBook. To quote from the Mac OS X Security Configuration for Version 10.5 Leopard Second Edition, Chapter 3 pages 50-51:

''If your environment does not permit the use of the following hardware components, you must physically disable them ...

Only an Apple Certified technician can physically disable these components without voiding the warranty on your computer. A limited number of Apple Certified technicians can remove preapproved components.

After an Apple Certified technician removes the component the technician logs a special note with Apple Care, indicating that the computer has had a component properly removed. Most components removed by Apple technicians can be reinstalled, if needed.

To locate a Certified Apple technician go to:

Also, see your local Apple representative for more information.

Note: If you are in a government organization and need a letter of volatility for Apple products, send your request to''

FYI: A similar action can be taken for hand held devices such as an Apple iPhone.

BTW: You can still use an external camera/microphone for services such as iChat on a MacBook where the built in devices have been removed. When permitted, plugging in an external camera/microphone will temporarily restore such capability. Moreover, by physically removing such external devices when they are not in use, you can better control them. :-)

So buy your MacBook, have a Apple Certified technician remove the offending components, and if needed get a letter of volatility. Q.E.D.

Comment Re:coding at East Camp Vostok Antarctica (Score 1) 1127

You said the laptop drive crashed. Perhaps the altitude combined with the "odd air" as you put it contributed to the drive crash? What was your "non-Windoz laptop" and did that suffer any problems?

I imagine the dry air made static discharge a problem. That must have made working with electronics a challenge.

BTW: Were you working on the lake drilling project or something related to ice-core research or what?

I agree your working conditions may not have been the worst, but from what you said it was one of the more odd coding conditions I've read about.

Slashdot Top Deals

U X e dUdX, e dX, cosine, secant, tangent, sine, 3.14159...