Development of automated means for proving programs properties.pdf Для повышения надёжности компьютерных систем актуальна задача автоматической верификации программ. Верификация программы - доказательство её соответствия заданным формальным требованиям [1]. Существуют два основных метода верификации: динамический, при котором программа исследуется в процессе своей работы, и статический, при котором исследование происходит без запуска программы. В данной работе рассматривается статическая верификация. Под программой понимается синтаксически правильная последовательность команд на языке программирования, реализующая некоторую функцию. Для решения задачи верификации необходимы методы, позволяющие определить, обладает ли данная программа некоторым формально заданным свойством. Имеет смысл рассматривать нетривиальное свойство, то есть такое, для которого существуют программы, обладающие им, но не все программы обладают им. В общем случае эта задача неразрешима в силу теоремы Райса - Успенского [2]. Поэтому алгоритм, устанавливающий, обладает ли программа заданным нетривиальным свойством, может не всегда выдавать результат или совершать ошибки первого (второго) рода. Программа преобразует состояние потоков входа и выхода, состояние потока кодируется последовательностью чисел, поэтому за модель программы примем функцию на произведении списков f : N* х N* ^ N* х N*. Для упрощения технических деталей и в силу существования биективного соответствия между N* х N* и N можно принять упрощённую модель программы / : N ^ N. Будем считать 0 Е N специальным значением. В работе исследовано следующее важное свойство безопасности: программа / (х) может выдать секретное сведение s, только если на вход был подан x = k, где k - ключ. В силу принятой модели s, k Е N. Приведём примеры простейших программ (функций), обладающих данным свойством: если x = s иначе. Для доказательства того, что функции обладают заданным свойством, использована система автоматизированного доказательства теорем Coq [3]. Для каждой из возможных функций /(x) построено доказательство соответствующей свойству безопасности теоремы: Vx, s, k Е N \ {0} (/(x) = s ^ x = k). Доказательства для разных функций схожи и строятся по следующей схеме: 1) рассматриваются все x, 0 < x < k, для них выполнение условия /(x) = s проверяется непосредственно; 2) значение /(k) допускается любым; 3) доказывается, что /(x) при x > k не может принять значения s. Шаги 1 и 2 выполняются одинаково для всех функций; в шаге 3 возможны незначительные различия. На основе этого написана новая тактика в системе Coq для доказательства выбранного свойства, автоматически выполняющая шаги 1 и 2 и для некоторых функций шаг 3. Тактика применима к нерекурсивным функциям. Для облегчения трансляции с языка программирования удобнее использовать неупрощённую модель представления программ в виде функций. Для функций на списках подходит такой же метод с модификацией способа реализации шагов. Рассмотрены аналогичные приведённым выше функции на списках, для них также построены доказательства соответствующей теоремы. Наряду с рассмотрением вышеизложенного метода сделано предположение, что поставленную задачу можно решить иным способом. Для формализации программ существует система Л-исчисления [4]. Каждую функцию можно представить в виде терма Л-исчисления, которому можно присвоить тип по определённым правилам. Известен изоморфизм между типизированным Л-исчислением и интуиционистской логикой высказываний, являющийся частным случаем соответствия Карри - Говарда [5]. Таким образом, если сформулировать некое свойство программ в виде импликации в интуиционистской логике и представить исследуемую программу в виде терма типизированного Л-исчисления, можно проверить, соответствует ли полученный терм доказательству требуемого свойства, и в случае соответствия утверждать, что программа обладает данным свойством. Реализация этого метода - возможная тема для дальнейших исследований.

Скачать электронную версию публикации