Nessuna quantità di analisi formale, tipo / controllo delle regole potrebbe impedire il suo sfruttamento? Che ne dici di un kernel completamente verificato come SEL4?
Secondo il matematico Kurt i teoremi di incompletezza di Gödel :
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.
I teoremi di Gödel, in termini semplici, affermano che qualsiasi sistema sufficientemente complesso (non banale) non può dimostrare che sia privo di difetti.
Il software gira su hardware, probabilmente anche con errori. Anche i software funzionanti correttamente che incontrano un bug a livello di hardware saranno classificati come non funzionanti.
Leggi altre domande sui tag debugging vulnerabilities verification