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


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


Алгоритм модулярного умножения (алгоритм P) приведен на рис.2.1, а на рис.2.2 представлен псевдокод процедуры ADDK.

Так как B[i] [0,...,2 ?/2-1], то проверку "if B[i]<>0" в алгоритме P можно не вводить потому, что вероятность того, что B[i] будет равняться 0 пренебрежимо мала, если значение ? не достаточно малым. Ошибка затем все равно будет алгоритмом обнаружена. Проверка

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

позволяет представлять k числом однократной точности и работать с наи-меньшими абсолютными остатками в каждой итерации. Значение операнда Pi на каждом шаге итерации должно быть ограничено величиной N.

Теорема 2.1. Пусть Pi - частичное произведение P в конце i-той итерации (т.е. в конце i-того цикла FOR алгоритма P). Тогда для любого i (i=[1,...,n]) abs(Pi)N, rm-1 N rm.

Доказательство теоремы 2.1. Доказательство теоремы проведем методом индукции. Если k=abs(p_short) DIV n_short, где DIV - целочисленное деление, то

p_short=(k+?)*n_short, (2.1.6)

где k - целое, 0 k < r-1 и 0 ? < 1.

Проверка "if p_short-k*n_short>n_short DIV 2" есть ни что иное, как проверка

? > 0.5 (2.1.7)

На i-том шаге алгоритм вычисляет:

P'=Pi-1*r+A*B[i] (2.1.8)

Возможны два варианта:

Вариант 1. Если k=0, т.е. n_short>abs(p_short) (см. алгоритм), то суммирование при помощи процедуры ADDK не производится и утверждение теоремы выполняется, т.е. abs(Pi) < N .

Вариант 2. Если k > 0, т.е.

n_short < abs(p_short) (2.1.9)

Здесь также возможны два варианта:

Вариант A:

p_short < 0 (2.1.10)

Из (2.1.9) и (2.1.10) следует P' и так как Pi=-P'+k*N (см. алгоритм), то согласно (2.1.7)

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

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

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

Алгоритм P

m_shifts:=0; while n[m_shifts]=0 do begin shift_left(N and A); m_shifts:=m_shifts+1; end; m:=m_shifts; reset(P); n_short:=N[m]; for i:=n downto 1 do begin shift_left(P);

{сдвиг на 1 элемент влево или
умножение P*r} if b<>0 then addk(A*B[i],{to}P); let p_short represent the 2 high




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