Методы и технологии обеспечения безопасности программного обеспечения

Методы доказательства правильности программ

Общие положения

К теории верификации.

Традиционные методы анализа ПО включают и методы доказательства правильности программ. Концепция, положенная в основу этого направления, была предложена в 1960;х гг. в работах П. Наура и Р. Флойда, в которых сформулирована идея приписывания точке программы так называемого индуктивного, или промежуточного, утверждения и указана возможность доказательства частичной правильности программы (т.е. соответствия друг другу ее предусловия и постусловия), построенного на установлении согласованности индуктивных утверждений.

Фундаментальный вклад в теорию верификации в середине 1970;х гг. внесли Ч. Хоор, который высказал идеи проведения доказательства частичной правильности программы в виде вывода в некоторой логической системе, и Э. Дейкстра, который ввел понятие «слабейшее предусловие», позволяющее одновременно как соответствие друг другу предусловия и постусловия, так и завершимость.

Методы доказательства правильности программ принесли определенную пользу программированию. Было отмечено, что эти методы указывают способ рассуждения о ходе выполнения программ, дают удобную систему комментирования программ и устанавливают взаимосвязи между конструкциями языков программирования и их семантикой. Если принять более широкое толкование термина «анализ программ», подразумевая доказательство разнообразных свойств программ или доказательство теорем о программах, то ценность методов анализа станет более ясной. В частности, можно исследовать характер изменения выходных значений программы, количество операций при выполнении программы, наличие зацикливаний, незадействованных участков программы. Таким образом, в некоторых частных случаях методы верификации могут применяться и для доказуемого обнаружения программных дефектов.

Формальное доказательство в виде вывода в некоторой логической системе вполне надежно, но сами доказательства оказываются очень длинными и часто необозримыми. Рассмотрим следующий фрагмент программы.

Листинг 6.1. Фрагмент программы.

integer г, dd;

г := a; dd := d;

while dd < г do dd := 2*dd;

while dd Ф d do.

begin dd := dd/2; if dd < r do r:=r-dd;

end.

Должно соблюдаться условие, что целые константы and удовлетворяют отношениям а > d и d > 0.

Рассмотрим последовательность значений, заданную выражениями для.

С помощью обычных математических приемов можно вывести, что.

Кроме того, поскольку d > 0, можно сделать вывод о том, что для любого конечного значения г отношение dd_k > г будет выполняться при некотором конечном значении к; первый цикл завершается при dd = d*2^k. Решая уравнение.

относительно d_; _ _1; получаем.

что позволяет утверждать, что второй цикл тоже завершится. По окончании первого цикла.

и поэтому выполняется соотношение.

Соотношение (6.2) сохраняется при выполнении повторяемого оператора второго заголовка. По завершении повторений (в соответствии с заголовком while dd Ф d do мы получаем.

Отсюда и из соотношения (6.2) следует, что.

Далее доказываем, что после начала работы программы всегда выполняется отношение.

Это следует, например, из того, что возможные значения dd имеют вид (см. формулу (6.1)) d *2‘ при 0 < г < к.

Следующая задача состоит в том, чтобы показать, что после присваивания г начального значения всегда выполняется отношение.

Повторяемый оператор первого заголовка (dd := 2 * dd) сохраняет отношение (6.5), и поэтому весь первый цикл сохраняет отношение (6.5).

Повторяемый оператор из второго цикла состоит из двух операторов:

• • первый dd:= 2/ dd сохраняет инвариантность (6.5);
• • второй тоже сохраняет отношение (6.5), так как он либо не изменяет значение г, либо уменьшает г на текущее dd, а эта операция в силу (6.4) также сохраняет справедливость отношения (6.5).

Таким образом, весь повторяемый оператор второго цикла сохраняет отношение (6.5).

Объединяя отношения (6.3) и (6.5), получаем, что окончательное значение г удовлетворяет условиям 0 r (mod d), т. е. г — наименьший неотрицательный остаток от деления, а на d.

Итак, программа, состоящая всего из нескольких строчек кода, может требовать формального доказательства ее правильности (т.е. доказательства соответствия предусловия и постусловия, а также доказательства завершимости), состоящего из нескольких страниц текста.