5 ms·

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 me

by 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.
  - tbrownaw 16y ago
    > 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.
patio11 16y ago
I have no knowledge on whether they correctly implemented the spec or not, but it is virtually certain that it starts with "Assume this code is not actually implemented on atoms and electrons" because as soon as you get physics involved all bets are off. Side channel attacks are some scary voodoo. 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?!
- JoachimSchipper 16y ago
  True, but proving the absence of side-channel attacks is not currently feasible (it's a very active research area, though - feel free to ask if you want to know something). And tptacek has a point: sadly, most devices break well before side-channel attacks are worth considering.
Rusky 16y ago
Why all the skepticism? Of course you can't prove that it works how people imagine it, but the spec can be a lot higher level than the program itself. 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.
wglb 16y ago
One of my favorite papers along this line is http://gcc.gnu.org/wiki/summit2010?action=AttachFile&do=get&target=regehr_gcc_summit_2010.pdf http://gcc.gnu.org/wiki/summit2010?action=AttachFile&do=... (PDF) which talks about a compiler fuzzing technique that found bugs in all kinds of compilers, including 11 bugs in a research compiler that was proved to be correct.

by spolsky 16y ago

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.
- tbrownaw 16y ago
  > 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.

patio11 16y ago

I have no knowledge on whether they correctly implemented the spec or not, but it is virtually certain that it starts with "Assume this code is not actually implemented on atoms and electrons" because as soon as you get physics involved all bets are off. Side channel attacks are some scary voodoo. 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?!

JoachimSchipper 16y ago
True, but proving the absence of side-channel attacks is not currently feasible (it's a very active research area, though - feel free to ask if you want to know something). And tptacek has a point: sadly, most devices break well before side-channel attacks are worth considering.

Rusky 16y ago

Why all the skepticism? Of course you can't prove that it works how people imagine it, but the spec can be a lot higher level than the program itself. 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.

wglb 16y ago

One of my favorite papers along this line is http://gcc.gnu.org/wiki/summit2010?action=AttachFile&do=get&target=regehr_gcc_summit_2010.pdf http://gcc.gnu.org/wiki/summit2010?action=AttachFile&do=... (PDF) which talks about a compiler fuzzing technique that found bugs in all kinds of compilers, including 11 bugs in a research compiler that was proved to be correct.