On 2010.04.27 14:02, Artem Chuprina wrote:
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> методов для доказательства корректности работы программы.
С добрым утром. Век уже как доказано, что эта задача в общем виде
алгоритмически неразрешима.
То есть для реального доказательства надо либо ОЧЕНЬ специально писать
проверяемую программу, либо _придумывать_ доказательство для данной
конкретной. Причем во втором случае размер доказательства (и,
соответственно, вероятность ошибок уже в нем) растет принципиально
быстрее, чем размер самой программы. Даже не экспоненциально, а что-то
типа гиперэкспоненты.
Это и подразумевалось. Доказательства выполняются вручную в
proof assistant.
Сейчас некоторые процессоры имеют доказательство корретности
работы некоторых своих подчастей.
И это понятно почему - если у вас 4 32-битовых регистра
общее число возможных комбинаций - 128-бит - на пределе
обозримых вычислительных возможностей.
Доказательство же позволит избежать полного невозможного
перебора для тестирования.
--
С уважением, Александр Гавенко.
--
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/4bd6da88.9060...@bifit.com.ua
