Formalne dowodzenie poprawności
Dającą potencjalnie największe możliwości, ale współcześnie wciąż nieosiągalną metodą weryfikacji bezpieczeństwa programów jest formalne dowodzenie ich poprawności [9]. W teorii, posiadając szczegółowy opis oczekiwanego zachowania aplikacji lub platformy, oraz znając algorytm jej działania, powinno być możliwe wykorzystanie systemów automatycznego dowodzenia twierdzeń do zbadania, czy oczekiwania autora zostaną spełnione przez napisany kod. Temat ten jest obszarem intensywnych prac badawczych, powstały też pewne rozwiązania, których poprawność udowodniono matematycznie. Do przykładów zaliczyć można proste mikrojądro systemu Coyotos, czy Extremely Reliable Operating System. W praktyce jednak, ze względu na stopień skomplikowania typowych programów komercyjnych i zakres ich interakcji z komponentami zewnętrznymi, na trudność sformalizowania specyfikacji oprogramowania, oraz na problem stopu - takie metody, poza bardzo specyficznymi sytuacjami, są nieefektywne.
Strona Glowna