Want to read Slashdot from your mobile device? Point it at m.slashdot.org and keep reading!

 


Forgot your password?
Close
typodupeerror
Operating Systems

World's First Formally-Proven OS Kernel 517

Posted by Soulskill from the wait-for-it dept.
An anonymous reader writes "Operating systems usually have bugs — the 'blue screen of death,' the Amiga Hand, and so forth are known by almost everyone. NICTA's team of researchers has managed to prove that a particular OS kernel is guaranteed to meet its specification. It is fully, formally verified, and as such it exceeds the Common Criteria's highest level of assurance. The researchers used an executable specification written in Haskell, C code that mapped to Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system." Does it run Linux? "We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well." Further technical details are available from NICTA's website.
Education

Submission + - U.S. Colleges Say Hiring U.S. Students a Bad Deal 1

Submitted by
theodp
theodp writes: "Many U.S. colleges and universities have notices posted on their websites informing U.S. companies that they're tax chumps if they hire students who are U.S. citizens. "In fact, a company may save money by hiring international students because the majority of them are exempt from Social Security (FICA) and Medicare tax requirements," advises the taxpayer-supported University of Pittsburgh (pdf) as it makes the case against hiring its own U.S. students. You'll find identical pitches made by the University of Delaware, the University of Cincinnati, Kansas State University, the University of Southern California, the University of Wisconsin, Iowa State University, and other public colleges and universities. The same messsage is also echoed by private schools, such as John Hopkins University, Brown University, Rollins College and Loyola University Chicago."

Comment Apple profits either way.. (Score 1) 606

by rayver (#25991499) Attached to: Apple Believes Someone Is Behind Psystar
What I don't understand is that Apple is going to win either way. If Psystar wins, they'll still be paying Apple licensing fees for the OSX software. For every clone they sell, Apple makes a small cut. Sure, Apple is going to lose exclusive sales of their already expensive equipment, but it would make them more competitive. They would have to compete separately in the OS market (designing OS's so that PC users can decide whether Windows/Linux/OSX is better, and designing systems so that PC users will think Apple is worth it compared to Dell, Gateway, Acer, IBM, etc.). Apple is only putting up a fight as a barrier to their systems. Since Microsoft allows Windows to be installed on Apple systems, it's only fair that apple allow OSX to be installed on other systems as well. If Microsoft sued Apple for allowing windows to be installed on their systems, there would not be as high of a demand for Apple systems. I truly see this as an unfair competitive advantage that Apple currently holds.

Slashdot Top Deals

Time to take stock. Go home with some office supplies.

Close