Oleksandr Gavenko -> debian-russian@lists.debian.org @ Tue, 27 Apr 2010 09:37:03 +0300:
>> Быстро доказываем, что сертификация существует для кормежки >> сертифицирующих органов и т.д.: >> 1. Баги есть есть всегда >> 2. за 1 год дизассемблируют и найдут дырку где угодно >> 3. 4 года будут делать с информацией что хотят >> >> Или, социальная инженерия решает проблему взлома еще быстрее >> >> Системное ПО без апдейтов - решето, (вспомните недавнюю дырку в bind со >> смешным патчем) >> соответственно вопрос в наполненности абстрактно-конкретных карманов >> и т.д. >> OG> +1 OG> В будущем правда имеется перспектива использования формальных OG> методов для доказательства корректности работы программы. С добрым утром. Век уже как доказано, что эта задача в общем виде алгоритмически неразрешима. То есть для реального доказательства надо либо ОЧЕНЬ специально писать проверяемую программу, либо _придумывать_ доказательство для данной конкретной. Причем во втором случае размер доказательства (и, соответственно, вероятность ошибок уже в нем) растет принципиально быстрее, чем размер самой программы. Даже не экспоненциально, а что-то типа гиперэкспоненты. -- If a `religion' is defined to be a system of ideas that contains unprovable statements, then Godel taught us that mathematics is not only a religion, it is the only religion that can prove itself to be one. -- John Barrow -- To UNSUBSCRIBE, email to debian-russian-requ...@lists.debian.org with a subject of "unsubscribe". Trouble? Contact listmas...@lists.debian.org Archive: http://lists.debian.org/50494...@tigger.lan.cryptocom.ru
