Vlákno názorů ke zprávičce Bezpečnostní audit TrueCryptu bude pokračovat od Pali - "...snad přinese definitivní potvrzení bezpečnosti TrueCryptu." Definitivne to bude...

Deterministicky to rozhodnout nelze, na to přišel Alan Turing už v roce 1936:
http://cs.wikipedia.org/wiki/Probl%C3%A9m_zastaven%C3%AD

O koze a o voze...

Jasne, ze nejde najit *obecny zpusob*. Kdyby to slo, nejsou auditori potreba, protoze by se to pridalo do kompilatoru a bylo by (tedy az na chyby kompilatoru) hotovo.

Jasne, ze metodologicky vzato nelze potvrdit platnost hypotezy. Ale tady se nebavime o hypotezach pri pozorovani, ale o vcelku deterministickem systemu (at uz tomu sami programatori veri nebo ne - ze nerozumim tomu, jak to funguje, neznamena preci, ze to tak nefunguje).

Halting problém taky řeší deterministický systém a říká, že pro známý program a známý vstup neexistuje obecná metoda, která rozhodne, zda program někdy skončí. Security audit je ještě o řád složitější, protože se pro známý program a neznámý (libovolný) vstup snaží dokázat, že program neskončí v nedefinovaném stavu. Tohle exaktně vyřešit neumíme. Jistě, můžete se zeptat nějakého "experta", který se podívá do křišťálové koule a prohlásí daný program za bezpečný, ale nic to nedokazuje, je to tvrzení postavené na dobré víře, které nemáte jak ověřit.

Nie, halting problem hodnoti ci *lubovolny* program vzdy skonci alebo nie. Security audit pre *konkretny* program, hodnoti ci skonci vzdy v definovanom stave.

Vseobecny halting problem nie je mozne riesit algoritmicky. Ale pre nejaku mnozinu problemov (napr. uz LBA) algoritmicky riesitelny je.

Pri security audite sa hodnoti iba jeden program (a nie nekonecne velku mnozninu programov).

Najdu sa aj konkretne priklady programov o ktorych ide rozhodnut ci vzdy skoncia alebo nie. A taktiez teoreticky pre nejake programy ide formalne dokazat ze vzdy skoncia v definovanom stave. Neznamena to ale ze bude nutne existovat vseobecny nejaky postup ako sa k dokazu dopracovat.

Nepotřebujete řešit halting problém. Potřebujete zaručit, že kód nemá vedlejší efekty. Například že konkrétní metoda nezasahuje do jiných dat, než vstupních a výstupních. Tohle a řada jiných věcí se dá ověřit kombinací vhodného jazyka a systematického strojového ověření zdrojáku.
Dá se to dokonce dovést tak daleko, že celý OS může běžet v jednom procesu, protože je formální verifikací ověřeno, že žádný kód nebude lézt kam nemá. Bohužel to stojí nějaký výkon, a vyžaduje to přepsání prakticky veškerého SW, takže si na to ještě počkáme.
http://research.microsoft.com/pubs/69431/osr2007_rethinkingsoftwarestack.pdf

Pokud dokazujete bezpečnost programu, tak musíte dokázat mnohem víc. Program se může chovat zcela bez vedlejších efektů a přesto nebude bezpečný. Systematické ověření zdrojáku vám nepomůže, protože bezpečnostní slabina nemusí být ve zdrojáku rozpoznatelná jako slabina. Abych dal názorný příklad: Můžete mít program šifrující pomocí 3DES. Z programátorského hlediska to bude naprosto v pořádku, nikde nebude docházet k přepisům neočekávané paměti nebo k používání neinicializovaných proměnných apod., ale pokud tvůrce programu dosáhne toho, že jsou všechny tři použité klíče stejné, tak výstup programu sice bude v pořádku z hlediska specifikací (tzn. ani ověřením testových vektorů nic špatného nezjistíte), ale bude snadno prolomitelný (složitost jako DES, ne jako 3DES). No a vy jako bezpečnostní auditor byste potřeboval dokázat, že pro žádnou kombinaci vstupů a vnitřních stavů k tomuto nemůže dojít. A že neexistuje ani žádné jiné myslitelné oslabení algoritmu. A to nedokážete. Dokážete akorát říct, že jste nenašel nic, co by nasvědčovalo této možnosti. Problém je v tom, že na tohle oslabení programátor nepřijde, protože nerozpozná bezpečnostní dopady zdánlivě neškodné operace, a kryptolog, který by to rozpoznat mohl, zase v programu nerozpozná (když to útočník udělá šikovně), že program dělá něco navíc. I když budou program zkoumat programátor a kryptolog společně, budou mít problémy kvůli komunikaci (co jednomu přijde samozřejmé, to nebude říkat tomu druhému, a pravděpodobně tak slabé místo přeskočí).

Já jen doplním, to co už psal _pepak. Když budu mít kód typu:

// authenticate user
do {
    username = GetUsername();
    password = GetPassword();
} while (!UserValid(username, password))
// send money
destinationAccountNumber = GetDestinationAccountNumber();
amountOfMoney = GetAmountOfMoney()
SendMoney(destinationAccountNumber, amountOfMoney);

Tak musím řešit halting problem (skončí ten do while cyklus někdy? skončí jen pro platná data?), ale to je jen malá část problému. Musím navíc ověřit, že všechny funkce dělají to, co mají dělat. Vhodnou volbou jazyka lze omezit chyby typu buffer overflow (za předpokladu, že veříme kompilátoru/virtual machine) a možná i ten halting problem, pokud použiju něco ultimátně funkcionálního, ale jazyk sám o sobě nezaručí, že tam nebudou záměrné nebo náhodné chyby. Když bude ve funkci SendMoney podmínka typu:

if (date() == datumMojiCestyNaBahamy && amountOfMoney >= 1000000) {
    PosliPenizeNaMujUcetNaBahamach(amountOfMoney)
}

Nezjistí to automatický test a je určitá pravděpodobnost (ne 100%), že to objeví auditor. Takových chyb ať už úmyslných nebo neúmyslných tam může být celá řada docela dobře schovaných. Takže ani po auditu kódu nelze nikdy na 100% prohlásit, že je to bezpečné.

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čí.

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čí.