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

в 4:41, , рубрики: верификация, верификация программ, математика, Программирование, формальная верификаци, функциональное программирование, метки: , ,

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

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]);

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

Автор: telomejtel


* - обязательные к заполнению поля


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js