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

Источник: 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)  = )

Вторая теорема 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)  =

Код доказательства этих теорем я почти не буду комментировать - ясно, что по сравнению с, казалось бы, простотой и почти очевидностью доказательств код для проверки машиной должен быть несуразно подробным. Вначале необходимо загрузить модель 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)  = ^(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)  = ^(f3v1_rhsc))``, DISCH_TAC THEN REWRITE_TAC [f3v1, UNDISCH subgoal_eq1, f3f2v_thm]);

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

val ef1vx = prove(``?a c d. ^(f1vx_lhsc) =  ``, 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) =  )``, 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)  = ^(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]);

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

Безльготная IT-жизнь.

SIEMENS: расследование нечистоплотной коммерческой деятельности немецкой компании в части работы с Россией.

Создание системы отчетов для работы финансового директора на основе ERP системы и Seagate Crystal Reports 8.0.

Компьютер и спина.

Сертификационная программа (ISC)2.

Главная » Новости