软件本身是否存在缺陷，因而易受攻击？

Question

任何形式的分析、类型/规则检查都不能阻止它的利用吗？一个经过充分验证的内核(如SEL4 )如何？

Answer 1

根据数学家Kurt G del不完备定理的说法：

第一个不完全性定理指出，其定理可由“有效程序”(例如计算机程序，但可以是任何算法)列出的公理系统不能证明关于自然数关系(算术)的所有真理。对于任何这样的系统，总会有关于自然数的陈述，这些自然数是真的，但在系统中是不可证明的。第二个不完备性定理是第一个定理的推广，它证明了这样一个系统不能证明它本身的一致性。

哥德尔的理论，简单地说，任何足够复杂的系统(非平凡)都不能证明它是没有缺陷的。

软件运行在硬件之上，而硬件也可能出现错误。即使是在硬件级别上遇到错误的正确运行的软件，也将被归类为失败。