Could no amount of formal analysis, type/rule checking prevent it's exploitation? How about a fully verified kernel such as SEL4 ?


According to mathematician Kurt Gödel's incompleteness theorems:

The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an "effective procedure" (e.g., a computer program, but it could be any sort of algorithm) is capable of proving all truths about the relations of the natural numbers (arithmetic). For any such system, there will always be statements about the natural numbers that are true, but that are unprovable within the system. The second incompleteness theorem, an extension of the first, shows that such a system cannot demonstrate its own consistency.

Gödel's theorums, in simple terms, say that any sufficiently complex system (non-trivial) cannot prove that it is without flaws.

Software runs on top of hardware, which is also likely to have errors. Even correctly functioning software that encounters a bug at the hardware level will then be classified as failing.

| improve this answer | |
  • 1
    AFAIK, Gödel theorems are about systems where you compose all the possible rules/statements (in fact, Wikipedia specifically talks about arithmetic systems, not systems in general). And the result is that you cannot guarante to prove each of the statements as true or false. You could agree that a general programming language would qualify as a Gödel incomplete system, but a concrete program is way more closed and usually predictable. The real issue is that using the tools that calculate formal correction is only done for extreme cases (v.g. power plants) due to the effort they require. – SJuan76 Nov 19 '14 at 8:45
  • The sel4 proofs also make explicit that they assume correctly functioning hardware. That level of abstraction allows the code to be examined as an isolated system and determine whether it can ever reach an inconsistent internal state – Jonathon Anderson Mar 15 '19 at 19:20

Not the answer you're looking for? Browse other questions tagged or ask your own question.