Názor ke zprávičce Bezpečnostní audit TrueCryptu bude pokračovat od Lael Ophir - Chyba v kódu a špatný (volitelně záměrně špatný)...

Chyba v kódu a špatný (volitelně záměrně špatný) design jsou dvě různé věci. Když se podíváte na ty stovky ročně bugů v každém browseru, v Adobe Flashi, Adobe Readeru, Javě, všech OS atd., jde typicky o chyby v kódu, o side effecty. Typicky jde o různé variace na téma práce s pamětí, nejčastěji (trestuhodně) buffer overflow. SW průmysl je ve velmi špatném stavu, děravé je prakticky všechno od kernelů až po browsery. Přitom s tímhle si už poradit umíme, vizte projekt Singularity, který jsem linkoval. Samozřejmě u toho zapomeňte na jazyk C, který je z hlediska verifikace noční můrou, a na standardní funkce knihoven typu strcpy(), které jsou nebezpečné už z principu.

Samozřejmě projekt typu Singularity není schopný odhalit, že je špatný návrh aplikace, případně že je návrh špatný záměrně. To ze samotného kódu odhalit ani nelze. Dá se ale verifikovat kód podle strojově čitelné specifikace.

Jinak co se týká problému zastavení, tam to není tak problematické. Ve vámi uvedeném případu můžete v některých variantách říct zcela jistě, že se kód nezastaví (například pokud UserValid() vrací vždy false), a v jiných případech se minimálně dozvíte, že se zastavit nemusí. To pro většinu účelů stačí.