Исследования процесса верификации расчетных программ
В качестве примера работоспособности предложенного метода рассмотрим верификацию программы вычисления функции дискретного возведения в степень:
y= fAM (x) = Ax modulo M.
Выбор данной функции обусловлен тем, что она является одной из основных функций в различных теоретико-числовых конструкциях, например, в схемах электронной цифровой подписи, системах открытого распределения ключей и т.п. Это, в свою очередь, демонстрирует возможность применения предложенного метода при исследовании расчетных программ, решающих конкретные прикладные задачи. Кроме того, очевидно, что данная функция обладает свойством случайной самосводимости, а, исходя из вышеприведенных рассуждений и работы [BLR], рассуждений можно показать, что для данной функции существует (1/288, 1/8)-самотестирующаяся программа.
Для экспериментальных исследований была выбрана программа EXP из библиотеки базовых криптографических функций CRYPTOOLS [КС2], которая реализует функцию дискретного экспоненцирования в степень (размерность переменных и констант не превышает 64 или 128 байтов). Была разработана интегрированная оболочка для проведения верификации, включающая интерфейс с пользователем и программные процедуры, реализующие некоторую совокупность проверочных тестов. Экспериментальные исследования состояли из определения временных характеристик процесса верификации на основе использования ST-пары функций и определения возможности обнаружения предложенным методом преднамеренно внесенных программных ошибок.
Для этого были определены следующие ST-пары функций:
В процессе исследований менялась используемая ST-пара функций и варьировалась размерность параметров A, M и аргумента X. Результаты экспериментов полностью подтвердили приведенные выше временные зависимости (технические результаты исследований автор в данной работе опускает).
Исследование возможности обнаружения предложенным методом преднамеренно внесенных закладок заключалось в написании программы EXPZ.
Спецификация для программ EXP и EXPZ одна и та же, отличие же заключается в том, что программа EXPZ содержит программную закладку деструктивного характера. Преднамеренно внесенная закладка при исследованиях гарантировала сбой работы программы вычисления значения функции y = fAM (x) = Ax modulo M (то есть обеспечивала получение неправильного значения функции) примерно на каждой восьмой части входных значений экспоненты x.
Было проведено свыше 2000 экспериментов [КС2]. Все входные значения, на которых произошел сбой программы, были обнаружены, что в дальнейшем подтвердилось проверочными тестами, основанными на использовании малой теоремы Ферма и теореме Эйлера. Этот факт, в свою очередь, экспериментально показал, что программа, реализующая алгоритм ST, является (1/8,1/288)-самотестирующейся программой.
Таким образом, предложенный метод позволяет в значительной степени сократить время испытания расчетных программ на предмет выявления непреднамеренных и преднамеренных программных дефектов. При этом по результатам испытаний можно получить количественные оценки вероятности наличия программных дефектов в верифицируемой расчетной программе. Однако, разработка формальных методов получения ST-пары функций для заданной расчетной программы, а также разработка методик ее испытания с помощью рассмотренного алгоритма требуют дальнейших теоретических и прикладных исследований.
