Формальная верификация Си кода

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

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

Существует формальная верифицированная ОС на основе микроядра L4 ^[1], но верифицирован только Си код, а часть написанная на ассемблере не гарантирована, для того чтобы покрыть и ее нужно иметь формальную модель набора процессорных инструкция, чего еще нет, но работа ведется и в этом ^[2] направлении. Также существует верифицированный компилятор Compcert ^[3], но и для него остаются недоказанными части разбора исходных текстов, генерации непосредственно машинных кодов и линковки. Помимо внутренних проблем каждого из проектов есть еще и проблема совмещения их результатов для получения целиком верифицированной програмной системы. Compcert и l4 verified используют несколько разные подмножества Си и разные инфраструктуры верификации — один основан на Coq, а другой на Isabelle/HOL. Вот небольшая об этом ^[4].

Я попытался поизучать Isabelle/HOL и верифицировать примитивную функцию. Вот функция целиком:

void swap(int *a, int *b)
{
	int tmp = *a;
	*a = *b;
	*b = tmp;
}

Я докажу что функция swap действительно меняет местами значения в памяти.

Для того чтобы запустить доказательство у себя вам понадобится Isabelle/HOL версии 2009-1. Здесь ^[5] можно скачать и посмотреть инструкцию по установке. Также понадобится с-parser от команды l4-verified для того, чтобы парсить Си код и делать из него утверждения доказуемые в Isabelle/HOL. Скачать можно тут ^[6], иструкции внутри архива. После того как вы все установили и скомпилировали выполняете в папке YourIsabelleInstalationRoot/Isabelle/bin команду isabelle -emacs -k L4. Далее в начавшейся интерактивной сессии открываете файл swap.thy с приведенным далее доказательством (рядом с файлом swap.thy должен лежать файл swap.c с текстом приведенной выше функции) и запускаете доказательство выбрав логику vcg.

Я не разобрался как записать спецификацию функции отдельно от доказательства поэтому просто сформулировал теорему внутри файла swap.thy. Эту теорему я приведу в самом низу после того как будут доказаны все необходимые леммы. Относительно языка доказательства можно посмотреть туториал здесь ^[7], а применяемой модели языка Си статьи отсюда ^[8], например эта ^[9] статья.

Доказательства в Isabele/HOL проводятся путем применения последовательности тактик, которые изменяют посылки и следствия так, что доказываемое утверждение становится тождеством. Самые распространенные тактики это simp — применяет либо набор зашитых правил логики, либо явно указанных доказанных ранее утверждений для простого переписывания термов. Тактика auto — прувер пытается сам доказать утверждение и оставляет нам для ручного доказательства слишком сложную для него часть. Тактика drule — если какая-нибудь посылка совпадает с посылкой в указанном ранее доказанном утверждении, то она заменяется на следствие этого утверждения. Тактика rule — наоборот, если следствие совпадает со следствием в указанном утверждении то оно заменяется на соответствующую посылку.

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

theory swap
  imports CTranslation
begin

install_C_file "swap.c"

context swap
begin

Затем леммы. Сначала лемма word_uint_proximity и леммы необходимые для ее доказательства. Смыл леммы в том, что если два 32 битных слова находятся близко то разница их числовых представлений может быть хоть и большой но относительно нее выполняются некоторые неравенства:

lemma word_uint_minus_mod: "uint ((a::32 word) - (b::32 word)) = (uint a - uint b) mod 2 ^ 32"
by (simp add: word_sub_wi uint_word_of_int)

lemma word_uint_noteq: "(a::32 word) <noteq> (b::32 word) ==> uint a <noteq> uint b"
by (simp)

lemma word_uint_less: "a < (4::32 word) ==> uint a < 4"
apply (simp add: word_less_def word_le_def, auto)
apply (drule_tac a="a" and b="4" in word_uint_noteq)
by auto

lemma int_less_more_minus: "[| 0 <= (i::int); 0 <= (j::int); i < 4; j < 4 |] ==> -3 <= i-j <and> i - j <= 3"
by auto

lemma int_mod_comp_pos: "[| (a::int) mod 2 ^ 32 = (b::int) mod 2 ^ 32; 0 <= b; b <= 3 |] ==> a <= - (2 ^ 32) + 3 | 0 <= a & a <= 3 | 2 ^ 32 <= a"
apply (rule notnotD)
apply (rule notI)
apply auto
apply (simp add: mod_int_def divmod_int_def negDivAlg.simps posDivAlg.simps)+
done

lemma int_mod_comp_neg: "[| (a::int) mod 2 ^ 32 = (b::int) mod 2 ^ 32; -3 <= b; b < 0 |] ==> a <= - (2 ^ 32) | -3 <= a & a < 0 | 2 ^ 32 - 3 <= a"
apply (rule notnotD)
apply (rule notI)
apply auto
apply (simp add: mod_int_def divmod_int_def negDivAlg.simps posDivAlg.simps)+
done

lemma int_mod_comp_pos_neg: "[| (a::int) mod 2 ^ 32 = (b::int) mod 2 ^ 32; -3 <= b; b <= 3|] ==> a <= - (2 ^ 32) + 3 | -3 <= a & a <= 3 | 2 ^ 32 - 3 <= a"
apply (cases "-3 <= b & b < 0")
apply (drule int_mod_comp_neg, simp+, force)
apply (drule int_mod_comp_pos, simp+, force)
done

lemma int_mod_diff_comp_pos_neg: "[| ((a::int) - (b::int)) mod 2 ^ 32 = (l - k) mod 2 ^ 32; l - k <= 3; -3 <= l - k |] ==> a - b <= - (2 ^ 32) + 3 | -3 <= a - b & a - b <= 3 | 2 ^ 32 - 3 <= a - b"
apply (erule int_mod_comp_pos_neg, auto)
done

lemma word_uint_proximity: "[| (a::32 word) + k = (b::32 word) + l; k < 4; l < 4 |] ==> uint a - uint b <= - (2 ^ 32) + 3 | -3 <= uint a - uint b & uint a - uint b <= 3 | 2 ^ 32 - 3 <= uint a - uint b"
apply (subgoal_tac "a - b = l - k")
defer
apply (drule_tac f="<lambda> x.  x - b - k" and x="a + k" in arg_cong)
apply (simp add: word_sub_def)
apply (thin_tac "a + k = b + l")
apply (drule_tac f="<lambda> x. uint x" in arg_cong)
apply (drule_tac word_uint_less)+
apply (simp only: word_uint_minus_mod)
apply (subgoal_tac "uint l - uint k <= 3 & -3 <= uint l - uint k")
prefer 2 apply (simp add: int_less_more_minus)
apply (elim conjE)
apply (thin_tac "uint ?a < ?b")+
apply (erule int_mod_diff_comp_pos_neg)
by auto

Затем лемма c_guard_eq_or_disjoint и несколько лемм необходимых для ее доказательства. Лемма о том, что если два указателя ненулевые и выравнены (c_guard включает оба утверждения), то они либо равны, либо множества адресов на которые они указываю не пересекаются:

lemma dvd_nat_eq_int: "[| 0 <le> a; n dvd nat a |] ==> int n dvd a"
apply (simp add: dvd_def unat_def)
apply auto
apply (rule_tac x="int k" and P="<lambda> x. a = int n * x" in exI)
apply (drule_tac f="<lambda> x. int x" in arg_cong)
apply (simp only: int_mult)
done

lemma dvd_unat_eq_uint: "[| n dvd unat a |] ==> int n dvd uint a"
apply (rule_tac a="uint a" in dvd_nat_eq_int)
by (auto, simp add: unat_def)

lemma word_ptr_uint_noteq: "a ~= b ==> uint (ptr_val a) ~= uint (ptr_val b)"
by simp

lemma word_of_nat_less: "a < 4 ==> of_nat a < (4::32 word)"
apply (cases "a = 3")
apply auto
apply (cases "a = 2")
apply auto
apply (cases "a = 1")
apply auto
apply (cases "a = 0")
apply auto
done

lemma c_guard_eq_or_disjoint: "[| c_guard (a::32 word ptr); c_guard (b::32 word ptr) |] ==> a = b <or> {ptr_val a..+4} <inter> {ptr_val b..+4} = {}"
apply auto
apply (simp add: intvl_def c_guard_def ptr_aligned_def)
apply clarify
apply (thin_tac "c_null_guard ?x")+
apply (drule dvd_unat_eq_uint)+
apply (simp add: dvd_def)
apply auto
apply (rename_tac da db ka kb)
apply (subgoal_tac "uint (ptr_val a) - uint (ptr_val b) <= - (2 ^ 32) + 3 | -3 <= uint (ptr_val a) - uint (ptr_val b) & uint (ptr_val a) - uint (ptr_val b) <= 3 | 2 ^ 32 - 3 <= uint (ptr_val a) - uint (ptr_val b)")
prefer 2
apply (thin_tac "a ~= b")
apply (thin_tac "uint ?a = ?b")+
apply (drule word_of_nat_less)+
apply (rule word_uint_proximity, assumption+)
apply (thin_tac "?a < 4")+
apply (thin_tac "?a + ?b = ?c + ?d")
apply (drule word_ptr_uint_noteq)
apply auto
apply (subgoal_tac "0 <= ka & ka < 2 ^ 32 div 4")
prefer 2 apply auto[1]
apply (insert uint_ge_0 [of "ptr_val a"], simp)[1]
apply (insert uint_lt [of "ptr_val a"], simp)[1]
apply (subgoal_tac "0 <= kb & kb < 2 ^ 32 div 4")
prefer 2 apply (thin_tac "?a & ?b", auto)[1]
apply (insert uint_ge_0 [of "ptr_val b"], simp)[1]
apply (insert uint_lt [of "ptr_val b"], simp)[1]
apply auto[1]
apply (subgoal_tac "0 <= ka & ka < 2 ^ 32 div 4")
prefer 2 apply auto[1]
apply (insert uint_ge_0 [of "ptr_val a"], simp)[1]
apply (insert uint_lt [of "ptr_val a"], simp)[1]
apply (subgoal_tac "0 <= kb & kb < 2 ^ 32 div 4")
prefer 2 apply (thin_tac "?a & ?b", auto)[1]
apply (insert uint_ge_0 [of "ptr_val b"], simp)[1]
apply (insert uint_lt [of "ptr_val b"], simp)[1]
apply auto[1]
done

Затем лемма h_val_heap_update_disjoint_same о том, что если множества адресов указателей не пересекаются, то значение по первому указателю после того, как по второму указателю что-нибудь записали, не изменится:

lemma h_val_heap_update_disjoint_same: "[| {ptr_val (a::32 word ptr)..+length v} Int {ptr_val (b::32 word ptr)..+4} = {}; v = to_bytes (x::32 word) bs |] ==> h_val (heap_update a (x::32 word) h) b = h_val h b"
apply (drule_tac h="h" in  heap_list_update_disjoint_same)
apply (unfold h_val_def heap_update_def, simp)
apply (rotate_tac 2)
apply (drule_tac f="<lambda> x. from_bytes x" in arg_cong)
apply (simp add: to_bytes_def typ_info_word)
done

Затем сама теорема и одна дополнительная лемма для ее доказательства. Выполнение функции записывается СALL swap(a,b). Предусловия и постусловия записываются в скобках {| |}. Разыменовывание выглядит как h_val (hrs_mem <acute>t_hrs) a, где t_hrs это стандартная переменная для heap'а. Таким образом теорема звучит так: выводимо, что если выполнено предусловие, то после вызова функции будет выполнено постусловие.

lemma word_to_bytes_length: "v = to_bytes (x::32 word) bs ==> length v = 4"
by (simp add: to_bytes_def typ_info_word word_rsplit_def bin_rsplit_def)

theorem "<Gamma> <turnstile> {| c_guard a & a_val = h_val (hrs_mem <acute>t_hrs) a & c_guard b & b_val = h_val (hrs_mem <acute>t_hrs) b |} CALL swap(a,b)
           {| h_val (hrs_mem <acute>t_hrs) a = b_val & h_val (hrs_mem <acute>t_hrs) b = a_val|}"
apply vcg
apply auto
prefer 2 apply (simp add: hrs_mem_def hrs_mem_update_def h_val_heap_update)
apply (simp add: hrs_mem_def hrs_mem_update_def h_val_heap_update)
apply (cases "a = b", simp add: hrs_mem_def hrs_mem_update_def h_val_heap_update)
apply (drule c_guard_eq_or_disjoint)
apply auto
apply (thin_tac "c_guard b")
apply (thin_tac "a ~= b")
apply (subgoal_tac "{ptr_val (b::32 word ptr)..+length (to_bytes (h_val aa a) bs)} Int {ptr_val (a::32 word ptr)..+4} = {}")
prefer 2
apply (auto simp: word_to_bytes_length)[1]
apply (drule_tac a="b" and x="h_val aa a" and h="heap_update a (h_val aa b) aa" in h_val_heap_update_disjoint_same, simp)
apply (simp add: h_val_heap_update)
done

И окончание начатой теории

end

end

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

Автор: telomejtel