Názor ke zprávičce FBI zapletena v backdooru IPSec implementace v OpenBSD od limit_false - Gregory Perry (byvaly NETSEC CTO, ktery zpravu o...
-
limit_false (neregistrovaný)
Gregory Perry (byvaly NETSEC CTO, ktery zpravu o FBI backdooru zverejnil) spekuluje, ze prave tyto backdoory byly duvodem, ze OpenBSD prislo v 2003 o DARPA funding ($2.3M), protoze backdoory nasli ("prava ruka nevi co dela leva").
Je velmi tezke umyslne chyby maskovane jako race condition nebo casovani odhalit, protoze model checking si muze dovolit tak NASA, DARPA nebo firmy vyvijejici software pro letiste. Navic je model checking obecne algoritmicky nevycislitelny problem.
A napr. existuje protokol, ktery je prokazatelne bezpecny, ale nasli se v nem side-channel attacks - protoze model s tim jednoduse nepocital (a dopredu nelze pocitat se vsim - protoze Godelova veta o neuplnosti).
BTW Underhanded C contest: http://underhanded.xcott.com/ (soutez v psani nevinne vypadajiciho kodu, ktery dela neco jineho nez by se zdalo)
