Источник: habrahabr
telomejtel
В своей прошлой статье я описал процесс верификации примитивной функции на Си. Параллельно привел соображения, почему верификация Си кода недостаточна для того, чтоб считать программу безошибочной. В основном эти соображения сводятся к мысли, что написать код - это только часть истории о получении работающей программы. Следующим приближением к тому, чтобы получить действительно безошибочную программу, является верификация ассемблерных кодов, их уже не нужно будет транслировать и поэтому полностью исключится обширное поле для возникновения ошибок. В данной статье я опишу процесс доказательства некоторых свойств уже для ассемблерного кода, который на порядок примитивней, чем даже простейшая функция на Си, о которой говорилось в прошлой статье.
Вот этот код:
0x00: subs r0, r0, #1
0x04: bne 0x0C
0x08: mov r1, #0
0x0C: mov r1, #1
После 3 шагов выполнения этого кода в зависимости от равенства начального значения регистра
r0единице в регистре r1 окажется либо один, либо ноль.
Сначала скажу еще несколько слов о самом ассемблерном коде. В данном случае речь идет не об ассемблере как языке программирования, а о машинных кодах. То есть здесь будет доказано некоторое утверждение о следующей программе в бинарном виде:
0xE2500001
0x1A000000
0xE3A01000
0xE3A01001
Если бы мы говорили об ассемблере, то проблемы доказательств утверждений о коде на высокоуровневых языках программирования остались бы в силе. А именно необходимость не только иметь и доверять имеющейся модели языка программирования, но и доверять компилятору, а в идеале и верифицировать его. Современные ассемблеры предоставляют множество возможностей, например, возможность модульного программирования, а значит становится необходима компоновка. Здесь же стадия компиляции и компоновки отсутствует.
Для доказательств я буду пользоваться средством для интерактивного доказательства теорем HOL (или наgithub'е) и созданной для него моделью ассемблерных инструкции для ARMv4. После того как вы получили последнюю версию HOL, скомпилировали её и модель ARMv4 - можете проделать все доказательства. Код я приведу целиком, чтобы у тех, кому интересно, была возможность полностью повторить все шаги доказательства.
Будет доказано две теоремы. Первая goal_eq1 о том, что если начальное значение регистра r0 равно 1, то через три шага исполнения в регистре r1 будет 0, также как и во всех остальных регистрах общего назначения:
/- ((x :bool[32]) = (1w :bool[32])) ⇒
(STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)
</registers := (r0 =+ x) (λ(n :register). (0w :bool[32]));
psrs :=
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32]));
undefined := F; cp_state := ()/> =
</registers :=
(pc =+ (12w :bool[32])) (λ(n :register). (0w :bool[32]));
psrs :=
(CPSR =+ SET_NZCV (F,T,T,F) (SET_IFMODE F F usr (0w :bool[32])))
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/>)
Вторая теорема
goal_ne1, о том если начальное значение регистра r0 не равно 1, то через три шага исполнения в регистре r1 будет 1:
/- (x :bool[32]) ≠ (1w :bool[32]) ⇒
∃(a :bool) (c :bool) (d :bool).
STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)
</registers := (r0 =+ x) (λ(n :register). (0w :bool[32]));
psrs :=
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32]));
undefined := F; cp_state := ()/> =
</registers :=
(pc =+ (16w :bool[32]))
((r1 =+ (1w :bool[32]))
((r0 =+
(n2w
(MOD_2EXP (32 :num)
(w2n x + (4294967294 :num) + (1 :num))) :
bool[32])) (λ(n :register). (0w :bool[32]))));
psrs :=
(CPSR =+
SET_NZCV (a,F,c,d) (SET_IFMODE F F usr (0w :bool[32])))
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/>
Код доказательства этих теорем я почти не буду комментировать - ясно, что по сравнению с, казалось бы, простотой и почти очевидностью доказательств код для проверки машиной должен быть несуразно подробным.
Вначале необходимо загрузить модель ARMv4, определить основные константы и собственно программу.
FileSys.chDir "/home/path/to/your/HOL/examples/ARM/v4";
load "arm_evalLib";
open arm_evalLib;
val _ = overload_on("sp", ``r13``);
val _ = overload_on("lr", ``r14``);
val _ = overload_on("pc", ``r15``);
fun evaluate_st n state =
let val memory = (rhs o concl) (SIMP_CONV (srw_ss()) [] ``^(state).memory``)
val registers = (rhs o concl) (SIMP_CONV (srw_ss()) [] ``^(state).registers``)
val psrs = (rhs o concl) (SIMP_CONV (srw_ss()) [] ``^(state).psrs``)
in evaluate(n, memory, registers, psrs) end;
fun evaluate_CONV state = evaluate_st 1 state;
val reg_r0_x = set_registers empty_registers `[(r0,x)]`;
val reg_r0_1 = set_registers empty_registers `[(r0,1w)]`;
val psr = set_status_registers empty_psrs
`[(CPSR,SET_NZCV (F,F,F,F) (SET_IFMODE F F usr 0w))]`;
val prog = list_assemble empty_memory
["0x00: subs r0, r0, #1",
"0x04: bne 0x0C",
"0x08: mov r1, #0",
"0x0C: mov r1, #1"];
Теперь доказательство первой из теорем и необходимых лемм. Доказательство происходит так: сначала доказывается, что после одного шага будет некоторое конкретное состояние регистров, затем доказывается, что необходимый бит регистра статуса будет равен 1, затем доказывается теорема про следующие два шага исполнения, и эти два доказательства используются для доказательства целевой теоремы.
val f1vx = evaluate(1,prog,reg_r0_x,psr);
val f1vx_lhsc = (lhs o concl) f1vx;
val f1vx_rhsc = (rhs o concl) f1vx;
val f1v1 = evaluate(1,prog,reg_r0_1,psr);
val f1v1_rhsc = (rhs o concl) f1v1;
val f1v_thm = prove(``(x = 1w) ==> (^(f1vx_lhsc) = ^(f1v1_rhsc))``, SIMP_TAC (srw_ss()) [f1vx, combinTheory.UPDATE_def]);
val f2v1 = evaluate_CONV f1v1_rhsc;
val f2v1_rhsc = (rhs o concl) f2v1;
val f2vx = evaluate_CONV f1vx_rhsc;
val f2vx_lhsc = (lhs o concl) f2vx;
val f2v_thm = prove(``(x = 1w) ==> (^(f2vx_lhsc) = ^(f2v1_rhsc))``, SIMP_TAC (srw_ss()) [f2vx, combinTheory.UPDATE_def]);
val f2v_thm_rhsc = (rhs o concl) (UNDISCH f2v_thm);
val f2f1v_thm = prove(``STATE_ARM_MMU (NO_CP :unit coproc) (2 :num) x = STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) (STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) x)``, REWRITE_TAC [systemTheory.STATE_ARM_MMU_def, numLib.num_CONV ``2``, numLib.num_CONV ``1``]);
val subgoal_eq1 = prove(``(x = 1w) ==> (STATE_ARM_MMU (NO_CP :unit coproc) (2 :num)
</registers :=
(r0 =+ (x :bool[32])) (λ(n :register). (0w :bool[32]));
psrs :=
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/> = ^(f2v1_rhsc))``, REWRITE_TAC [f1vx, f2v_thm, f2f1v_thm]);
val f3v1 = evaluate_CONV f2v_thm_rhsc;
val f3v1_rhsc = (rhs o concl) f3v1;
val f3f2v_thm = prove(``STATE_ARM_MMU (NO_CP :unit coproc) (3 :num) x = STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) (STATE_ARM_MMU (NO_CP :unit coproc) (2 :num) x)``, REWRITE_TAC [systemTheory.STATE_ARM_MMU_def, numLib.num_CONV ``3``, numLib.num_CONV ``1``]);
val goal_eq1 = prove(``(x = 1w) ==> (STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)
</registers :=
(r0 =+ (x :bool[32])) (λ(n :register). (0w :bool[32]));
psrs :=
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/> = ^(f3v1_rhsc))``, DISCH_TAC THEN REWRITE_TAC [f3v1, UNDISCH subgoal_eq1, f3f2v_thm]);
Доказательство второй теоремы несколько сложней, так как там участвует отрицание. Отличия от доказательства первой теоремы в том, что для того чтоб не тянуть за собой символические выражения для значений несущественных битов регистра статуса используются кванторы существования.
val ef1vx = prove(``?a c d. ^(f1vx_lhsc) = </registers :=
(pc =+ (4w :bool[32]))
((r0 =+
(n2w
(MOD_2EXP (32 :num)
(w2n x + (4294967294 :num) + (1 :num))) :bool[32]))
(λ(n :register). (0w :bool[32])));
psrs :=
(CPSR =+
SET_NZCV
(a,
MOD_2EXP (32 :num) (w2n x + (4294967294 :num) + (1 :num)) =
(0 :
num),
c,
d)
(SET_IFMODE F F usr (0w :bool[32])))
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/>``, EXISTS_TAC ``(BIT (31 :num) (MOD_2EXP (32 :num) (w2n (x :bool[32]) + (4294967294 :num) + (1 :num))))`` THEN EXISTS_TAC ``ODD (DIV_2EXP (32 :num) (w2n (x :bool[32]) + (4294967294 :num) + (1 :num)))`` THEN EXISTS_TAC ``word_msb (x :bool[32]) /\ (BIT (31 :num) (MOD_2EXP (32 :num) (w2n x + (4294967294 :num) + (1 :num))) <> word_msb x)`` THEN REWRITE_TAC [f1vx]);
val MODlem1 = prove(``!x. (x MOD 4294967296 = 0) ==> (?k. (x = 4294967296*k))``, RW_TAC arith_ss [] THEN ASSUME_TAC (SPEC ``x :num`` (SIMP_RULE (srw_ss()) [] (SPEC ``4294967296`` arithmeticTheory.DIVISION))) THEN EXISTS_TAC ``x DIV (4294967296 :num)`` THEN RW_TAC arith_ss []);
val CPSRlem1 = prove(``((x :bool[32]) <> 1w) ==> ((MOD_2EXP (32 :num) (w2n x + (4294967294 :num) + (1 :num)) = (0 : num)) = F)``, SIMP_TAC (arith_ss) [arithmeticTheory.MOD_2EXP_def] THEN DISCH_TAC THEN SPOSE_NOT_THEN ASSUME_TAC THEN UNDISCH_TAC ``(x :bool[32]) <> (1w :bool[32])`` THEN RW_TAC bool_ss [] THEN SIMP_TAC arith_ss [MODlem1] THEN ASSUME_TAC (SPEC ``w2n (x :bool[32]) + (4294967295 :num)`` MODlem1) THEN `?(k :num). w2n x + (4294967295 :num) = (4294967296 :num) * k` by (RW_TAC arith_ss []) THEN `(k :num) > 0` by FULL_SIMP_TAC arith_ss [] THEN `?(r :num). w2n (x :bool[32]) = (4294967296 :num) * (r :num) + 1` by EXISTS_TAC ``(k :num) - 1`` THEN ASM_SIMP_TAC arith_ss [] THEN ` w2n (x :bool[32]) = (1 :num)` by ASSUME_TAC (SPEC ``(x :bool[32])`` (INST_TYPE [alpha /-> ``:32``] wordsTheory.w2n_lt)) THEN FULL_SIMP_TAC (arith_ss ++ wordsLib.SIZES_ss) [] THEN PROVE_TAC [wordsTheory.n2w_w2n]);
val subgoal_ne1 = prove(``((x :bool[32]) <> 1w) ==> (?a c d. ^(f1vx_lhsc) = </registers :=
(pc =+ (4w :bool[32]))
((r0 =+
(n2w
(MOD_2EXP (32 :num)
(w2n x + (4294967294 :num) + (1 :num))) :bool[32]))
(λ(n :register). (0w :bool[32])));
psrs :=
(CPSR =+
SET_NZCV
(a,
F,
c,
d)
(SET_IFMODE F F usr (0w :bool[32])))
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/>)``, DISCH_TAC THEN ASSUME_TAC (UNDISCH CPSRlem1) THEN ASSUME_TAC ef1vx THEN FULL_SIMP_TAC pure_ss [] THEN EXISTS_TAC ``a :bool`` THEN EXISTS_TAC ``c :bool`` THEN EXISTS_TAC ``d :bool`` THEN REWRITE_TAC []);
val f3f1v_thm = prove(``STATE_ARM_MMU (NO_CP :unit coproc) (3 :num) x = STATE_ARM_MMU (NO_CP :unit coproc) (2 :num) (STATE_ARM_MMU (NO_CP :unit coproc) (1 :num) x)``, REWRITE_TAC [systemTheory.STATE_ARM_MMU_def, numLib.num_CONV ``3``, numLib.num_CONV ``2``, numLib.num_CONV ``1``]);
val f32vx = evaluate_st 2 (rhs (# 2 (strip_exists (concl (UNDISCH subgoal_ne1)))));
val f32vx_rhsc = (rhs o concl) f32vx;
val goal_ne1 = prove(``((x :bool[32]) <> 1w) ==> (?a c d. (STATE_ARM_MMU (NO_CP :unit coproc) (3 :num)
</registers :=
(r0 =+ (x :bool[32])) (λ(n :register). (0w :bool[32]));
psrs :=
(λ(x :psr).
SET_NZCV (F,F,F,F) (SET_IFMODE F F usr (0w :bool[32])));
memory :=
((0w :bool[30]) /:
[
enc
(SUB AL T (0w :bool[4]) (0w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])) :
arm_instruction);
enc (B NE (0w :bool[24]));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (0w :bool[8])));
enc
(MOV AL F (1w :bool[4])
(Dp_immediate (0w :bool[4]) (1w :bool[8])))
]) (λ(a :bool[30]). (0xE6000010w :bool[32])); undefined := F;
cp_state := ()/> = ^(f32vx_rhsc)))``, DISCH_TAC THEN ASSUME_TAC (UNDISCH subgoal_ne1) THEN FULL_SIMP_TAC pure_ss [f3f1v_thm] THEN EXISTS_TAC ``a :bool`` THEN EXISTS_TAC ``c :bool`` THEN EXISTS_TAC ``d :bool`` THEN REWRITE_TAC [f32vx]);
Доказательства, на мой взгляд, достаточно трудоемкие, особенно если их проводить для чего-то существенного, но те аспиранты, которые делали модель, пишут в своих статьях, что с помощью разработанных ими моделей они верифицировали какие-то нетривиальные вещи. Так что, может быть, подобные доказательства это будущее программ существенных для безопасности.