5 ms·

World's first hack-free software developed

28 points by nreece 16y ago

koretzu46 16y ago
Today there is an interesting situation in that there exist microkernels with an amount of published formal proofs such as the one by NICTA in this thread and, then, that there exist DO-178B avionics certified microkernels and separation kernels (often with very little published artefacts). I think that the current hot field for microkernels is to bring both formal methods and certification together, which is indeed starting to happen for DO-178C see for example https://sites.google.com/site/fmstandardsworkshop/ https://sites.google.com/site/fmstandardsworkshop/ . Holger Disclaimer: not completely unbiased here (e.g. http://www.uni-koblenz.de/~beckert/pub/safecomp2009.pdf http://www.uni-koblenz.de/~beckert/pub/safecomp2009.pdf).
JacobAldridge 16y ago
It's a shame Australian scientists don't have Social Security numbers to embed in this software somewhere, to demonstrate how unhackable it really is. http://www.wired.com/threatlevel/2010/05/lifelock-identity-theft/ http://www.wired.com/threatlevel/2010/05/lifelock-identity-t...
- haribilalic 16y ago
  But they do have Tax File Numbers (http://en.wikipedia.org/wiki/Tax_File_Number http://en.wikipedia.org/wiki/Tax_File_Number) and bank accounts.
  - narcissus 16y ago
    Yeah, the only 'shame' is that even if they embedded their TFNs, what's the worse that could happen? The laws that protect the use of the TFN would essentially make having it useless anyway. 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...
madhouse 16y ago
Sadly, mathematically proving that it does what the spec says does not necessarily mean that it's not vulnerable. The spec can be wrong too. Or the compiler. Or both. Nevertheless, it's very interesting.
- pluies 16y ago
  As Donald Knuth would say: "Beware of bugs in the above code; I have only proved it correct, not tried it."
  - shadowfox 16y ago
    This quote shows up like canon in almost every thread that has anything to do with formally verifiable/verified software :P
- limmeau 16y ago
  On http://ertos.nicta.com.au/research/l4.verified/ http://ertos.nicta.com.au/research/l4.verified/ , they explicitly do not claim that they have proven security properties.
limmeau 16y ago
Earlier discussion: see http://news.ycombinator.com/item?id=760547 http://news.ycombinator.com/item?id=760547
- srean 16y ago
  Very nice discussion there. It surprises me that a non-trivial piece of code written in C can be verified. It might be of interest that BitC http://www.bitc-lang.org/ 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.
sambeau 16y ago
World's first hack-free software 'developed' 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.
- Qz 16y ago
  I'm pretty sure they're using quotes there as actual quotes -- as in, the 'developed' part is a literal quote of something someone said or printed. BBC News does this all the time.
MindTwister 16y ago
Congratulations, OK Labs solved the halting problem: http://www.ibm.com/developerworks/rational/library/nov05/marasco/index.html http://www.ibm.com/developerworks/rational/library/nov05/mar...
- ac 16y ago
  No they didn't. And proving correctness of software isn't the same as solving the halting problem. You're confusing formal verification and static analysis (that doesn't mean that the latter doesn't work). Please, google Curry-Howard Isomorphism and Rice's Theorem, will ya?
- shasta 16y ago
  "Can a program ever be proven correct? No. There may be some very trivial toy programs that under very special conditions can be proven "correct" -- that is, we can mathematically prove that they will never give an incorrect result.5 In the real world of programs, however, the answer is no. At first, one is tempted to believe that it is simply a question of combinatorics. That is, if one considers all the permutations of all the paths through any non-trivial piece of software, one quickly comes to the conclusion that exhaustively testing any piece of software is an impossible task. This is analogous to the NP Complete problem. But, in fact, it is even worse than that. It turns out that proving programs correct is equivalent to solving the Halting Problem. And we know from Turing's work that that is an impossible task." 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.
  - allwein 16y ago
    From the article: "Its unique feature is that it has been mathematically proven to operate correctly, enabling it to separate trusted from untrusted software, protecting critical services from a failure or a malicious attack, say the scientists" 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.
motters 16y ago
In some other realm Gödel is laughing.
- sad_david 16y ago
  I presume you are referring to Gödel's incompleteness theorem, which states that any sufficiently powerful mathematical logic will have theorems that can't ever be proven in it. 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.
- jerf 16y ago
  Godel's theorem doesn't have much to say either way about "hacking". If you've got a bit of information on a system that a user X shouldn't be able to access, if you completely seal off the user X from that information it doesn't matter how many computations they run. They won't be able to get it. Godel's proof does not prove anything about a system's ability to access its external environment, it proves that a sufficiently complicated system can't be sealed from having certain properties on its inside.
  - regularfry 16y ago
    A DOS from a non-terminating process is still a hack.
    - jerf 16y ago
      The process can only fail to terminate if the exterior environment doesn't kill it, and no amount of work in a correctly secured environment will let the process escape that. 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.
zoul 16y ago
How is this hacker news, then? :)
oemera 16y ago
Are they serious? Is this serious? Is such a think like developing "unhackable" software or hardware even possible? I don't think so.
- powrtoch 16y ago
  Software can be proven correct, but if you want to do anything useful with a computer system, you need more than just an OS kernel. Even if the kernel itself is "perfect", that doesn't stop vulnerabilities from appearing in the upper levels. So it's a cool accomplishment, but it's never going to be "like Mac, but totally unhackable!" or anything like that.
spolsky 16y ago
I never understand claims like this. They proved that it implements "the spec" perfectly, but to do that, you need a detailed spec with no abstractions. That means the spec contains just as much information as the code itself, which means the spec is just as complex as the code. Thus, the spec is just as vulnerable to hacks as any other work created by fallible humans. So essentially, proving that the code is a perfect implementation of the spec tells you nothing.
- tbrownaw 16y ago
  > They proved that it implements "the spec" perfectly, but to do that, you need a detailed spec with no abstractions. 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.
  - magic_haze 16y ago
    Why so condescending? Joel made a perfectly valid point, and while _you_ might be thinking of something specific while writing your answer, many of us here don't have that context. I just spent the last few minutes trying to understand the last paragraph, and I'm still confused. 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.
0x0 16y ago
Isn't this what the Microsoft Singularity project have been working on for a long while? I remember reading some post about how they also have proven (verified) the correctness of its operation a while ago, but I can't immediately find a link.
apedley 16y ago
So the chip executes the code to the spec as perfectly as the imperfect human wrote them?
metageek 16y ago
It's worth noting that seL4 is a variant of L4, a very small microkernel. Proving the microkernel secure is interesting, and maybe useful; but a real OS has a lot of other pieces, which may introduce their own insecurities.
pwelch 16y ago
They are kinda asking for it aren't they? I mean its nice in theory but has it not been proven time and again there is no such thing as hack-free?
deleted 16y ago
[deleted]
udoprog 16y ago
Great, cudos. They just seemingly discarded the part about peer-review. Where is the spec and the code? Given that I would believe this claim (which I don't) there has to exist means for independent third parties to verify this. Otherwise it's just a pissing contest in space.
- lsf 16y ago
  Here you go: http://ertos.nicta.com.au/software/seL4/ http://ertos.nicta.com.au/software/seL4/ Contains kernel and spec. Free for non-commercial use.
- limmeau 16y ago
  A peer-reviewed paper on seL4 on an ACM conference: http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.abstract http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEK... (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).
  - udoprog 16y ago
    "The proof assumptions mean that there may be faults remaining in the kernel that could be classified as implementation faults below the level of C. They will not be faults that are properly visible on the level of the C programming language (which is our main claim of correctness), but they could still be serious faults that make the seL4 kernel misbehave." -- http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml 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.
9ec4c12949a4f3 16y ago
Technical Information on the seL4 Brief details: http://ertos.nicta.com.au/research/sel4/tech.pml http://ertos.nicta.com.au/research/sel4/tech.pml Extensive 187pages: https://docs.google.com/viewer?url=http://ertos.nicta.com.au/research/sel4/sel4-refman.pdf https://docs.google.com/viewer?url=http://ertos.nicta.com.au... Paper on it: https://docs.google.com/viewer?url=http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_10.pdf https://docs.google.com/viewer?url=http://ertos.nicta.com.au...
pnathan 16y ago
I spent some time studying this kernel in a graduate class a year or two ago. 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.
acconrad 16y ago
This is the definition of a trolling scientist. I'm willing to bet this will be cracked within 1 year of the software surfacing.
- lsf 16y ago
  How much do you want to bet? 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/ 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 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

28 points by nreece 16y ago

Today there is an interesting situation in that there exist microkernels with an amount of published formal proofs such as the one by NICTA in this thread and, then, that there exist DO-178B avionics certified microkernels and separation kernels (often with very little published artefacts). I think that the current hot field for microkernels is to bring both formal methods and certification together, which is indeed starting to happen for DO-178C see for example https://sites.google.com/site/fmstandardsworkshop/ https://sites.google.com/site/fmstandardsworkshop/ . Holger Disclaimer: not completely unbiased here (e.g. http://www.uni-koblenz.de/~beckert/pub/safecomp2009.pdf http://www.uni-koblenz.de/~beckert/pub/safecomp2009.pdf).

JacobAldridge 16y ago

It's a shame Australian scientists don't have Social Security numbers to embed in this software somewhere, to demonstrate how unhackable it really is. http://www.wired.com/threatlevel/2010/05/lifelock-identity-theft/ http://www.wired.com/threatlevel/2010/05/lifelock-identity-t...

haribilalic 16y ago
But they do have Tax File Numbers (http://en.wikipedia.org/wiki/Tax_File_Number http://en.wikipedia.org/wiki/Tax_File_Number) and bank accounts.
- narcissus 16y ago
  Yeah, the only 'shame' is that even if they embedded their TFNs, what's the worse that could happen? The laws that protect the use of the TFN would essentially make having it useless anyway. 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...

madhouse 16y ago

Sadly, mathematically proving that it does what the spec says does not necessarily mean that it's not vulnerable. The spec can be wrong too. Or the compiler. Or both. Nevertheless, it's very interesting.

pluies 16y ago
As Donald Knuth would say: "Beware of bugs in the above code; I have only proved it correct, not tried it."
- shadowfox 16y ago
  This quote shows up like canon in almost every thread that has anything to do with formally verifiable/verified software :P
limmeau 16y ago
On http://ertos.nicta.com.au/research/l4.verified/ http://ertos.nicta.com.au/research/l4.verified/ , they explicitly do not claim that they have proven security properties.

limmeau 16y ago

Earlier discussion: see http://news.ycombinator.com/item?id=760547 http://news.ycombinator.com/item?id=760547

srean 16y ago
Very nice discussion there. It surprises me that a non-trivial piece of code written in C can be verified. It might be of interest that BitC http://www.bitc-lang.org/ 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.

sambeau 16y ago

World's first hack-free software 'developed' 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.

Qz 16y ago
I'm pretty sure they're using quotes there as actual quotes -- as in, the 'developed' part is a literal quote of something someone said or printed. BBC News does this all the time.

MindTwister 16y ago

Congratulations, OK Labs solved the halting problem: http://www.ibm.com/developerworks/rational/library/nov05/marasco/index.html http://www.ibm.com/developerworks/rational/library/nov05/mar...

ac 16y ago
No they didn't. And proving correctness of software isn't the same as solving the halting problem. You're confusing formal verification and static analysis (that doesn't mean that the latter doesn't work). Please, google Curry-Howard Isomorphism and Rice's Theorem, will ya?
shasta 16y ago
"Can a program ever be proven correct? No. There may be some very trivial toy programs that under very special conditions can be proven "correct" -- that is, we can mathematically prove that they will never give an incorrect result.5 In the real world of programs, however, the answer is no. At first, one is tempted to believe that it is simply a question of combinatorics. That is, if one considers all the permutations of all the paths through any non-trivial piece of software, one quickly comes to the conclusion that exhaustively testing any piece of software is an impossible task. This is analogous to the NP Complete problem. But, in fact, it is even worse than that. It turns out that proving programs correct is equivalent to solving the Halting Problem. And we know from Turing's work that that is an impossible task." 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.
- allwein 16y ago
  From the article: "Its unique feature is that it has been mathematically proven to operate correctly, enabling it to separate trusted from untrusted software, protecting critical services from a failure or a malicious attack, say the scientists" 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.

motters 16y ago

In some other realm Gödel is laughing.

sad_david 16y ago
I presume you are referring to Gödel's incompleteness theorem, which states that any sufficiently powerful mathematical logic will have theorems that can't ever be proven in it. 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.
jerf 16y ago
Godel's theorem doesn't have much to say either way about "hacking". If you've got a bit of information on a system that a user X shouldn't be able to access, if you completely seal off the user X from that information it doesn't matter how many computations they run. They won't be able to get it. Godel's proof does not prove anything about a system's ability to access its external environment, it proves that a sufficiently complicated system can't be sealed from having certain properties on its inside.
- regularfry 16y ago
  A DOS from a non-terminating process is still a hack.
  - jerf 16y ago
    The process can only fail to terminate if the exterior environment doesn't kill it, and no amount of work in a correctly secured environment will let the process escape that. 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.

zoul 16y ago

How is this hacker news, then? :)

oemera 16y ago

Are they serious? Is this serious? Is such a think like developing "unhackable" software or hardware even possible? I don't think so.

powrtoch 16y ago
Software can be proven correct, but if you want to do anything useful with a computer system, you need more than just an OS kernel. Even if the kernel itself is "perfect", that doesn't stop vulnerabilities from appearing in the upper levels. So it's a cool accomplishment, but it's never going to be "like Mac, but totally unhackable!" or anything like that.

spolsky 16y ago

I never understand claims like this. They proved that it implements "the spec" perfectly, but to do that, you need a detailed spec with no abstractions. That means the spec contains just as much information as the code itself, which means the spec is just as complex as the code. Thus, the spec is just as vulnerable to hacks as any other work created by fallible humans. So essentially, proving that the code is a perfect implementation of the spec tells you nothing.

tbrownaw 16y ago
> They proved that it implements "the spec" perfectly, but to do that, you need a detailed spec with no abstractions. 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.
- magic_haze 16y ago
  Why so condescending? Joel made a perfectly valid point, and while _you_ might be thinking of something specific while writing your answer, many of us here don't have that context. I just spent the last few minutes trying to understand the last paragraph, and I'm still confused. 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.

0x0 16y ago

Isn't this what the Microsoft Singularity project have been working on for a long while? I remember reading some post about how they also have proven (verified) the correctness of its operation a while ago, but I can't immediately find a link.

apedley 16y ago

So the chip executes the code to the spec as perfectly as the imperfect human wrote them?

metageek 16y ago

It's worth noting that seL4 is a variant of L4, a very small microkernel. Proving the microkernel secure is interesting, and maybe useful; but a real OS has a lot of other pieces, which may introduce their own insecurities.

pwelch 16y ago

They are kinda asking for it aren't they? I mean its nice in theory but has it not been proven time and again there is no such thing as hack-free?

deleted 16y ago

[deleted]

udoprog 16y ago

Great, cudos. They just seemingly discarded the part about peer-review. Where is the spec and the code? Given that I would believe this claim (which I don't) there has to exist means for independent third parties to verify this. Otherwise it's just a pissing contest in space.

lsf 16y ago
Here you go: http://ertos.nicta.com.au/software/seL4/ http://ertos.nicta.com.au/software/seL4/ Contains kernel and spec. Free for non-commercial use.
limmeau 16y ago
A peer-reviewed paper on seL4 on an ACM conference: http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.abstract http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEK... (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).
- udoprog 16y ago
  "The proof assumptions mean that there may be faults remaining in the kernel that could be classified as implementation faults below the level of C. They will not be faults that are properly visible on the level of the C programming language (which is our main claim of correctness), but they could still be serious faults that make the seL4 kernel misbehave." -- http://ertos.nicta.com.au/research/l4.verified/proof.pml http://ertos.nicta.com.au/research/l4.verified/proof.pml 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.

9ec4c12949a4f3 16y ago

Technical Information on the seL4 Brief details: http://ertos.nicta.com.au/research/sel4/tech.pml http://ertos.nicta.com.au/research/sel4/tech.pml Extensive 187pages: https://docs.google.com/viewer?url=http://ertos.nicta.com.au/research/sel4/sel4-refman.pdf https://docs.google.com/viewer?url=http://ertos.nicta.com.au... Paper on it: https://docs.google.com/viewer?url=http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_10.pdf https://docs.google.com/viewer?url=http://ertos.nicta.com.au...

pnathan 16y ago

I spent some time studying this kernel in a graduate class a year or two ago. 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.

acconrad 16y ago

This is the definition of a trolling scientist. I'm willing to bet this will be cracked within 1 year of the software surfacing.

lsf 16y ago
How much do you want to bet? 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/ 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 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