Часто говорят что нет программ без ошибок. Это мнение сильно коробило мои эстетические чувства, поэтому я постарался поразбираться с формальной верификцией программ, ведь она обещает нам максимально возможную гарантию безошибочности при которой утверждение о корректности программы доказывается как математическая теорема. Здесь представлю результаты моего краткого ознакомления с этой темой.
Я написал в заголовке статьи не «верификация программ», а «верификация Си кода», так как по беглом рассмотрении успехов современного программирования в части формальной верификации обнаружил, что ни одна программа не может считаться гарантированно безошибочной. На сегодня существует лишь технология и инфраструктура для верификации Си кода программы, но этот Си код нужно еще оттранслировать в машинные коды, а для этого нужен компилятор и линкер и они тоже должны быть формально корректными. Ну и конечно для правильной работы программы нужна корректная операционная система. По этим направлениям работы ведутся, но окончательно все возникающие проблемы еще не решены.
Существует формальная верифицированная ОС на основе микроядра L4, но верифицирован только Си код, а часть написанная на ассемблере не гарантирована, для того чтобы покрыть и ее нужно иметь формальную модель набора процессорных инструкция, чего еще нет, но работа ведется и в этом направлении. Также существует верифицированный компилятор Compcert, но и для него остаются недоказанными части разбора исходных текстов, генерации непосредственно машинных кодов и линковки. Помимо внутренних проблем каждого из проектов есть еще и проблема совмещения их результатов для получения целиком верифицированной програмной системы. Compcert и l4 verified используют несколько разные подмножества Си и разные инфраструктуры верификации — один основан на Coq, а другой на Isabelle/HOL. Вот небольшая об этом.
Я попытался поизучать Isabelle/HOL и верифицировать примитивную функцию. Вот функция целиком:
void swap(int *a, int *b)
{
int tmp = *a;
*a = *b;
*b = tmp;
}
Я докажу что функция swap действительно меняет местами значения в памяти.
Для того чтобы запустить доказательство у себя вам понадобится Isabelle/HOL версии 2009-1. Здесь можно скачать и посмотреть инструкцию по установке. Также понадобится с-parser от команды l4-verified для того, чтобы парсить Си код и делать из него утверждения доказуемые в Isabelle/HOL. Скачать можно тут, иструкции внутри архива. После того как вы все установили и скомпилировали выполняете в папке YourIsabelleInstalationRoot/Isabelle/bin команду isabelle -emacs -k L4. Далее в начавшейся интерактивной сессии открываете файл swap.thy с приведенным далее доказательством (рядом с файлом swap.thy должен лежать файл swap.c с текстом приведенной выше функции) и запускаете доказательство выбрав логику vcg.
Я не разобрался как записать спецификацию функции отдельно от доказательства поэтому просто сформулировал теорему внутри файла swap.thy. Эту теорему я приведу в самом низу после того как будут доказаны все необходимые леммы. Относительно языка доказательства можно посмотреть туториал здесь, а применяемой модели языка Си статьи отсюда, например эта статья.
Доказательства в 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
