World's first hack-free software developed
hindustantimes.com
hindustantimes.com
No you don't.
> That means the spec contains just as much information as the code itself, which means the spec is just as complex as the code.
No it doesn't.
> Thus, the spec is just as vulnerable to hacks as any other work created by fallible humans.
The spec can be smaller and more accessible than the code.
> So essentially, proving that the code is a perfect implementation of the spec tells you nothing.
It tells you that you can read the spec and know exactly what the code will do. For example it won't BSOD (unless someone was silly enough to put that in the spec).
.
I can have a function "int exp(int a, int b)", and a spec that says it returns "a^b" (or "a b" or however you want to write it), or throws a IntegerOverflowException if that doesn't fit in an int. The actual function contains more information that the spec, such as how exactly it checks for overflow and whether it calls a multiply instruction or does its own repeated addition and whether it does b multiplications or uses certain mathematical tricks to work faster. The proof on the other hand I think does have to be as complex as the function, but at least proofs tend to be written in ways that the computer can help prove them.
I thought it was an accepted axiom that no "perfect" specs can be written in natural language: sure, you can _try_ to with a great deal of effort, but you can never get the same guarantees that a mathematically-based technique can give you. And the separation between the spec and the "proof" bothers me: what is the point of a spec if, after building a product, you can't verify you built it right? I would consider such specs as incomplete.
You have a spec, that says what the code should do. This is independent of the code; there can be many ways to write the code to match a given spec.
You have a proof, that says what the code does do. This is intimately tied to the code, and with the right languages and tools can be the code.
You verify that you built it right, by seeing that they match.
This is abstraction, the basic interface/implementation distinction; the spec is an interface and the code+proof is an implementation.
It's like there is a malicious and perfectly informed mathematician standing over the proof with a pen and a bottle of whiteout and the proof going "Meh, I'm not worried." What is it going to do? Prove that no matter how the malicious mathematician edits the proof it will stay correct?!
And tptacek has a point: sadly, most devices break well before side-channel attacks are worth considering.
You can already prove a lot of things about a large class of programs, depending on the language and tools, like the absence of buffer overruns, etc.
This project has a spec written in Haskell and then a proven 1:1 mapping at a certain level of detail between that spec and the kernel itself. You can prove an awful lot of things that way that do make a kernel like this more trustworthy and stable.
Basically the kernel was implemented in subsets of C and subsets of Haskell, and a 1:1 mapping between C and Haskell was proved. The Haskell code was formally proved to match certain properties in the prover.
One of the key innovations in the seL4 project is a formal treatment of properties regarding memory allocation and usage. That is to say, they were able to write proofs about malloc using only static analysis (just looking at the code, not running it), which was something that's been pretty out-of-reach to that point. Of course, there are limitations to the C code.
So, the seL4 microkernel is provably immune to certain classes of bugs. That's basically the big deal.
If I was looking for a secure kernel, seL4 would be a good starting point to look at, IMO.
Nevertheless, it's very interesting.
"Beware of bugs in the above code; I have only proved it correct, not tried it."
It's a curious use of quotes. I would have expected 'hack-free' to be in quotes.
Putting quotes around 'developed' seems to bring-into-question the whole statement.
It might be of interest that BitC http://www.bitc-lang.org/ is being developed as a flexible system programming language that supports verification.
It seeks to combine the flexibility, safety, and richness
of Standard ML or Haskell with the low-level expressiveness of C....
...it is possible to write a MPEG decoder or SHA-1 hash algorithm
in BitC that is fully safe, but performs competatively with the
C implementation. Today, that can't be done in SML, O'Caml, or Haskell.http://www.wired.com/threatlevel/2010/05/lifelock-identity-t...
Unlike in the US, for example, where the stories seem to imply having someones SSN means that I could essentially steal their identity. I don't know how far you would get trying to do something like that with a TFN only...
(I don't trust the Hindustan Times to get software verification details correct any more than I trust the Badische Zeitung to pick the right operation mode for a block cipher).
This just seems to be a case of someone running their mouth a bit too liberally and Hindustan Time jumping the gun. The actual project, which unfortunately is quite proprietary, has a much better overview of the whole ordeal. I would however like to se how their 1:1 strict C/haskell conversion actually looks (and why they decided against just modifying the something like the ghc :P).
You were right in not trusting the paper.
Contains kernel and spec. Free for non-commercial use.
Security is hard, really hard even, but Hollywood OS is fictional. Barriers are penetrable today because they have holes, not because Godel's theorem guarantees that all security can be penetrated. That's not what it is about.
This doesn't mean that certain particular theorems can't be proven, however. For instance, proving that a particular implementation of a kernel matches a particular specification can keep well away from Gödel.
So it's a cool accomplishment, but it's never going to be "like Mac, but totally unhackable!" or anything like that.
Your link is filled with nonsense, including the conclusion you took away from it here. We're talking about proving properties of a particular program here, not an arbitrary one. Please don't link to that in public again. It's a really terrible article.
He may have been basing his reply on this paragraph. If the OS could successfully answer whether any arbitrary program was trusted or untrusted, that this is equivalent to solving the halting problem.
Of course, the kernel is hackable (just hack the hardware, done). But if you stay with what the claim actually is, not what the press writes about it, we can play.
Download kernel and spec from [http://ertos.nicta.com.au/software/seL4/] stay in the proof assumption space, described here [http://ertos.nicta.com.au/research/l4.verified/proof.pml], and let us know if you can find a deviation from the spec, hacking or otherwise. Take as much time as you like.
If yes, we'll be very interested to hear and I'm sure we can write a paper together that a lot of people want to know about.
I usually don't have much time for trolling, but sometimes it's fun ;-)
Cheers, Gerwin