Could no amount of formal analysis, type/rule checking prevent it's exploitation? How about a fully verified kernel such as SEL4 ?
1 Answer
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.
answered Nov 19, 2014 at 2:28
-
1AFAIK, 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.– SJuan76Nov 19, 2014 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 Mar 15, 2019 at 19:20