Been a while since I posted on /.

I can understand Lord Steve's retirement, considering he's been running on secondhand parts for a while, but Taco?

No one else has abused this meme yet, so I may as well: not letting Taco keep his posting privileges is something that Hitler would do.

EOL.

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:

• 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) /\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.

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:

• Digits of 2^42643801 - 1 with dot separators (instead of commas)
• English name of 2^42643801 - 1 using the American system
• English name of 2^42643801 - 1 using the European system
• English name of 2^42643801 - 1 using the American system with dashes
• English name of 2^42643801 - 1 using the European system with dashes

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. :-)

The difference between the GPL and pretty much all EULAs and ToSes is: the former grants extra rights while the latter takes away rights. If everything else were exactly the same, except the license did not exist, your use of MySpace would be freer, but your use of GPL code would be... nonexistent. It's someone else's copyrighted material, which is simply illegal to insert into your own work without permission. The only reason that people may redistribute GPL code is the GPL itself.

I fully support anyone's right to ignore stupid EULAs and ToSes. I also support their right to ignore the GPL, and not use the code. The hypocrisy is from anyone who thinks they should be allowed the freedoms given to them by one part of the GPL without the requirements laid down by the other part.

Bad analogy. ISPs are in a position of power over its users. Generally there are only a handful of plausible choices for broadband internet in a given location. Wikipedia is just one information-gathering web site out of thousands. If you don't like Wikipedia's conditions, you can put your stuff somewhere else, including many completely free wiki sites. Whereas you can't set up your own independent broadband connection without a huge investment of money and effort.

p.s. Even worse, he's doing it ON THE INTERNET! Just like a CRAIGSLIST call girl!

Hmm... that Elastic Vapor guy is from Toronto, Canada. It seems FOREIGNERS are very happy indeed about this new database.

So, how many days until the 10:00 news is crowing that Obama is spending our tax dollars to give American secrets to other countries?

Antibodies against HIV are extremely hard to get right. For example, Dan Barouch has kept a group of vaccinated monkeys with an SIV/HIV hybrid alive for years... except for one whose virus mutated in just the wrong way. Based on the limited information in the article, it seems like the U Penn study works similarly.

Umm... so what is the bigger problem you are implying? And what exactly can't you agree with? When a lot of 2.4GHz devices are all operating in close proximity (such as apartments in a city) there will be more interference than if those devices are farther apart. It's simple physics.

I know from direct experience that a single 2.4GHz consumer product (such as this one, which BTW does not tell you it uses 2.4GHz video anywhere on or in the box, and only states the much lower frequency of its control channel) can completely swamp WiFi across the width of a suburban house. If there weren't a big yard between us, it would probably knock out my neighbor's WiFi too.