20 ms·

> This means that it is proved to be bug-free relative to a specification formulated in a mathematical logic But, but, but ... has the specification been prove

> This means that it is proved to be bug-free relative to a specification formulated in a mathematical logic But, but, but ... has the specification been proved to be bug-free? As in does the specification meet eg a set of security constraints?

lmm 6y ago
Perhaps you are a brain in a vat being deceived into thinking that the specification exists. Perhaps any memories you have of reading the specification are false and implanted. Perhaps this very comment doesn't actually exist, you are merely hallucinating the memory of having read it. Nothing can be known with absolute certainty. But a specification is much smaller than an implementation and misunderstandings of specifications are much less common than bugs in code. Don't let perfect be the enemy of good.
- Jweb_Guru 6y ago
  More importantly, a good specification is one that is triple-checked: by inspection by a human, having the program to conform to it, and by having to satisfy a bunch of nontrivial theorems about the spec that a human would expect from programs conforming to the spec. Sel4's integrity, confidentiality, and worst-case-execution-bounds proofs are an example of this... it's quite unlikely for a program to simultaneously provably satisfy a specification, the specification to provably satisfy nontrivial (first order) properties, and for those properties to nonetheless be defined incorrectly. Obviously there can still be holes in your model (for example, not considering certain side channels), but that's a pretty different situation from accidentally proving a different thing than you thought you were.
- MaxBarraclough 6y ago
  Philosophy of that sort offers little insight into correctness in formal software development, just as it offers little insight into the study of mathematics. In practice, bugs can creep in at various stages of a formal development process, but they're much less common that with non-formal software development methodologies, as you say. See page 46 of this case study (giant PDF warning): https://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf https://www.adacore.com/uploads/downloads/Tokeneer_Report.pd...
  - lmm 6y ago
    > Philosophy of that sort offers little insight into correctness in formal software development, just as it offers little insight into the study of mathematics. I disagree. Knowing the limits of what is possible is important, so that we don't waste our time looking for the impossible.
    - exikyut 6y ago
      What if our ability to know/reason about what is possible has a hard limit lower than the limits of what is truly possible?
      - lmm 6y ago
        Such a limit would be worth knowing about. But I see no reason to assume that limit exists in the absence of evidence, particularly as our tools and reasoning are improving all the time.
        MaxBarraclough 6y ago
        We can be pretty sure there is a limit. We're physical creatures in a (roughly) deterministic world, so ultimately we're bound by Rice's theorem just as computers are. Can the human brain in principle be simulated by a (deterministic) algorithm? Seems to me the answer is obviously yes, as we are 'merely' extremely complex machines whose operation is governed by deterministic physical laws. If you agree, you are forced to agree that we are bound by Rice's theorem. Whether it's ever likely to be a practical problem, is another matter. edit: We already know there are mathematically interesting numbers so enormous they cannot be represented in our universe, let alone computed by humans or our machines. That's not really the kind of practical limit we're interested in, but it still shows a limit of a sort. TREE(3) for instance.
        lmm 6y ago
        My perspective on results like Rice's theorem is that they tell us that the Turing machine formalism can express incomprehensible programs. I don't see that as a convincing argument that there are important or useful programs that we cannot comprehend; rather I see it as a demonstration the Turing machine model is broad, and an argument that we should look for stricter models that still admit all the programs we care about (probably based on some form of typed lambda calculus).
panpanna 6y ago
I think this is a very relevant question and I am sad to see that it is being downvoted. Remember that we have had two major flaws in the formally verified tls1.3 so far because the spec was not complete.
sanxiyn 6y ago
The right next sentence is, "And by now it has proofs about further security properties (which show that the specification has the right properties)". In particular, they formalized notions of confidentiality, integrity, and availability, and proved the specification (hence the source code, hence the binary) satisfies these notions. Now you can ask whether these notions were formalized correctly. But that's still a LOT better than asking it for binary/source/specification.
saithound 6y ago
Yes, the seL4 specification comes with proofs of strong integrity and information flow security guarantees, and with integrity and authority confinement proofs. It also comes with a configuration that is proved to be a static separation kernel. The implementation, including the code emitted by gcc, implements this specification, and is guaranteed to be free of buffer overflows, pointer errors, memory leaks, arithmetic overflows, and undefined behavior. [1] https://ts.data61.csiro.au/projects/seL4-verification/ https://ts.data61.csiro.au/projects/seL4-verification/
dathinab 6y ago
1st read other comments then: > has the specification been proved to be bug-free? Yes for SeL4, but no for a bunch of other systems advertised as "having been proven to be correct". Which often sadly only means "implemented as specified" but not "implemented as specified and proven to have the right properties".

lmm 6y ago

Perhaps you are a brain in a vat being deceived into thinking that the specification exists. Perhaps any memories you have of reading the specification are false and implanted. Perhaps this very comment doesn't actually exist, you are merely hallucinating the memory of having read it. Nothing can be known with absolute certainty. But a specification is much smaller than an implementation and misunderstandings of specifications are much less common than bugs in code. Don't let perfect be the enemy of good.

Jweb_Guru 6y ago
More importantly, a good specification is one that is triple-checked: by inspection by a human, having the program to conform to it, and by having to satisfy a bunch of nontrivial theorems about the spec that a human would expect from programs conforming to the spec. Sel4's integrity, confidentiality, and worst-case-execution-bounds proofs are an example of this... it's quite unlikely for a program to simultaneously provably satisfy a specification, the specification to provably satisfy nontrivial (first order) properties, and for those properties to nonetheless be defined incorrectly. Obviously there can still be holes in your model (for example, not considering certain side channels), but that's a pretty different situation from accidentally proving a different thing than you thought you were.
MaxBarraclough 6y ago
Philosophy of that sort offers little insight into correctness in formal software development, just as it offers little insight into the study of mathematics. In practice, bugs can creep in at various stages of a formal development process, but they're much less common that with non-formal software development methodologies, as you say. See page 46 of this case study (giant PDF warning): https://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf https://www.adacore.com/uploads/downloads/Tokeneer_Report.pd...
- lmm 6y ago
  > Philosophy of that sort offers little insight into correctness in formal software development, just as it offers little insight into the study of mathematics. I disagree. Knowing the limits of what is possible is important, so that we don't waste our time looking for the impossible.
  - exikyut 6y ago
    What if our ability to know/reason about what is possible has a hard limit lower than the limits of what is truly possible?
    - lmm 6y ago
      Such a limit would be worth knowing about. But I see no reason to assume that limit exists in the absence of evidence, particularly as our tools and reasoning are improving all the time.
      - MaxBarraclough 6y ago
        We can be pretty sure there is a limit. We're physical creatures in a (roughly) deterministic world, so ultimately we're bound by Rice's theorem just as computers are. Can the human brain in principle be simulated by a (deterministic) algorithm? Seems to me the answer is obviously yes, as we are 'merely' extremely complex machines whose operation is governed by deterministic physical laws. If you agree, you are forced to agree that we are bound by Rice's theorem. Whether it's ever likely to be a practical problem, is another matter. edit: We already know there are mathematically interesting numbers so enormous they cannot be represented in our universe, let alone computed by humans or our machines. That's not really the kind of practical limit we're interested in, but it still shows a limit of a sort. TREE(3) for instance.
        lmm 6y ago
        My perspective on results like Rice's theorem is that they tell us that the Turing machine formalism can express incomprehensible programs. I don't see that as a convincing argument that there are important or useful programs that we cannot comprehend; rather I see it as a demonstration the Turing machine model is broad, and an argument that we should look for stricter models that still admit all the programs we care about (probably based on some form of typed lambda calculus).

panpanna 6y ago

I think this is a very relevant question and I am sad to see that it is being downvoted. Remember that we have had two major flaws in the formally verified tls1.3 so far because the spec was not complete.

sanxiyn 6y ago

The right next sentence is, "And by now it has proofs about further security properties (which show that the specification has the right properties)". In particular, they formalized notions of confidentiality, integrity, and availability, and proved the specification (hence the source code, hence the binary) satisfies these notions. Now you can ask whether these notions were formalized correctly. But that's still a LOT better than asking it for binary/source/specification.

saithound 6y ago

Yes, the seL4 specification comes with proofs of strong integrity and information flow security guarantees, and with integrity and authority confinement proofs. It also comes with a configuration that is proved to be a static separation kernel. The implementation, including the code emitted by gcc, implements this specification, and is guaranteed to be free of buffer overflows, pointer errors, memory leaks, arithmetic overflows, and undefined behavior. [1] https://ts.data61.csiro.au/projects/seL4-verification/ https://ts.data61.csiro.au/projects/seL4-verification/

dathinab 6y ago

1st read other comments then: > has the specification been proved to be bug-free? Yes for SeL4, but no for a bunch of other systems advertised as "having been proven to be correct". Which often sadly only means "implemented as specified" but not "implemented as specified and proven to have the right properties".