Oleksandr Gavenko -> debian-russian@lists.debian.org @ Tue, 27 Apr 2010
15:37:28 +0300:
>> >> Быстро доказываем, что сертификация существует для кормежки
>> >> сертифицирующих органов и т.д.:
>> >> 1. Баги есть есть всегда
>> >> 2. за 1 год дизассемблируют и найдут дырку где угодно
>> >> 3. 4 года будут делать с информацией что хотят
>> >>
>> >> Или, социальная инженерия решает проблему взлома еще быстрее
>> >>
>> >> Системное ПО без апдейтов - решето, (вспомните недавнюю дырку в bind
>> со
>> >> смешным патчем)
>> >> соответственно вопрос в наполненности абстрактно-конкретных карманов
>> >> и т.д.
>> >>
>> OG> +1
>>
>> OG> В будущем правда имеется перспектива использования формальных
>> OG> методов для доказательства корректности работы программы.
>>
>> С добрым утром. Век уже как доказано, что эта задача в общем виде
>> алгоритмически неразрешима.
>>
>> То есть для реального доказательства надо либо ОЧЕНЬ специально писать
>> проверяемую программу, либо _придумывать_ доказательство для данной
>> конкретной. Причем во втором случае размер доказательства (и,
>> соответственно, вероятность ошибок уже в нем) растет принципиально
>> быстрее, чем размер самой программы. Даже не экспоненциально, а что-то
>> типа гиперэкспоненты.
>>
OG> Это и подразумевалось. Доказательства выполняются вручную в
OG> proof assistant.
OG> Сейчас некоторые процессоры имеют доказательство корретности
OG> работы некоторых своих подчастей.
От то-то и оно, что _некоторые_ процессоры и _некоторых_ подчастей. По
сравнению с кодом хотя бы libc там доказывать-то нечего... И все равно
полного доказательства про весь процессор нету. Да и в том, что есть,
еще надо доказать отсутствие ошибок :-)
OG> Доказательство же позволит избежать полного невозможного
OG> перебора для тестирования.
Нивапрос. Если его удастся, во-первых, построить, а во-вторых,
проверить.
Тесты ту же вероятность обычно дают дешевле.
Я еще могу понять, если требуется вероятность, которую тесты дать не
способны в принципе. Но доказательство с такой вероятностью практически
тоже возможно только для очень простой программы.
--
If it's there and you can see it---it's real
If it's not there and you can see it---it's virtual
If it's there and you can't see it---it's transparent
If it's not there and you can't see it---you erased it!
IBM poster explaining virtual memory, circa 1978
--
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/20095...@tigger.lan.cryptocom.ru
