Re: сертификация
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
Reply to: