Безопасность программного обеспечения компьютерных систем


Формальные методы доказательства правильности программ и их спецификаций - часть 6


assimilated digits of P; k:=abs(p_short) div n_short; if p_short-k*n_short > n_short div 2 then

k:=k+1; if k>0 then begin if p_short < 0 then addk(k*N,{to} P) else addk(-k*N,{to} P); end; end;{for} right shift P, N by m_shifts; if P < 0 then P:=P+N; write(P); {P - результат}

Рис. 2.1. Псевдокод алгоритма модулярного умножения A*B modulo N

Алгоритм ADDK

carry:=0; for i:=1 to m do begin t:=P[i]+k*N[i]+carry; P[i]:=t mod r; carry:=t div r; end; P[m+1]:=carry; write(P); {P - результат}

Рис.2.2. Псевдокод алгоритма вычисления P+k*N (процедура ADDK)

Вариант B:

p_short>0 (2.1.13)

Из (2.1.9) и (2.1.13) следует P'>N и так как Pi=P'-k*N, то согласно (2.1.7)

Pi=-? *N, если ? 0.5 (2.1.14)

и так как Pi=P'-(k+1)*N, то

Pi=(1-?)*N, если ? > 0.5 (2.1.15)

Во всех случаях (2.1.11), (2.1.12), (2.1.14) и (2.1.15), так как 0 ? < 1, то abs(Pi) < N. Теорема доказана

.

Примечание. Для чего нужна проверка (2.1.7)

"if p_short-k*n_short>n_short DIV 2" ?

Пусть в конце каждой итерации P принимает максимально возможное значение Pi-1=N-1, а N, A и B[i] заведомо тоже велики: N=rn+1-1, A=rn+1-2, B[i]=r-1. Тогда на i-том шаге согласно (2.1.8):

Pi'=(rn+1-2)*r+(rn+1-2)*(r-1)=2*rn+2-rn+1-4*r+2(2.1.16)

(2.1.17)

При достаточно большом m, если не введена проверка (2.1.6), то k < 2*r-1, по условию же 0< k < r -1. И из (2.1.16) и (2.1.17) видно, что P придется представлять m+2 разрядами (что определяется слагаемым 2*rn+2), по условию же m+1. Если же ввести проверку (2.1.7), то даже при ?=0,5 т.е.

Pi-1=(N-1)/2 и с учетом того, что если неравенство (2.1.7) выполняется, то Pi меняет знак на противоположный (сравн. (2.1.11), (2.1.12), (2.1.14) и (2.1.15)), из (2.1.6) и (2.1.7) получим, что 0 k < (1/2)*r-1, что удовлетворяет наложенному на k условию, и для представление P достаточно m+1 разряда.

В алгоритме P используется также известный метод, когда для получения частного от деления двух многоразрядных чисел, используются только старшие цифры этих чисел (см., например, алгоритм D в работе ).Чем больше основание системы счисления r, тем ниже вероятность того, что пробное частное k от деления первых цифр больших чисел не будет соответствовать действительному частному.

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




Начало  Назад  Вперед