Верификация программ на ARM ассемблере

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

0x00: subs r0, r0, #1 0x04: bne 0x0C 0x08: mov r1, #0 0x0C: mov r1, #1 

После выполнения этого кода в зависимости от равенства начального значения регистра 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]); 

Доказательства, на мой взгляд, достаточно трудоемкие, особенно если их проводить для чего-то существенного, но те аспиранты, которые делали модель, пишут в своих статьях, что с помощью разработанных ими моделей они верифицировали какие-то нетривиальные вещи. Так что, может быть, подобные доказательства это будущее программ существенных для безопасности.