Coscup 形式化驗證演講補充

# Coscup 形式化驗證演講補充 [演講資料](https://github.com/KevinKu/Formal-verification-of-simple-C-code) ## 相關領域簡介只說定理證明相關的目前自己是分成兩類 1. proof checker的實作與優化 ``` 這邊就要比較多的數理邏輯的理論了而各個定理證明器使用的理論都不一樣 ``` 舉常見的Coq與Isabelle/HOL為例子 ``` Coq使用數學直覺主義的邏輯 ``` 而 ``` Isabelle/HOL基於Meta Logic ``` 來源: Coq : Bertot Y, Casteran P. Interactive theorem proving and program development. Coq’Art: The Calculus of Inductive Constructions, Series: Texts in Theoretical Computer Science. An EATCS Series, 2004 Isabelle/HOL : [Old Introduction to Isabelle](http://isabelle.in.tum.de/doc/intro.pdf)第二頁 2. proof checker使用與驗證 ``` 基本上就是定理證明器語法的學習需要點數理邏輯的東西 , 原則以看懂proof checker的message為主另外就是驗證的公理理論 , 建模與證明的技巧了 ``` 基本入門就是符號邏輯 ## 形式化方法的限制不管是model checking還是定理證明基本有的限制 ``` model與Implementation的差異 ``` 基本做不到model與Implementation沒有差異所以這之間的gap考量就很重要了通常以C code建模的話要考慮的點就是:編譯器 , 硬體與 OS環境(可有可無) ### 編譯器 ``` 編譯器有可能改掉建模使用理論的公理/rule ``` ### 硬體 ``` 指令的語義 , 硬體行為的影響(i.e:亂序執行) ``` ### OS環境 ``` 使用的API , OS一些特性 ``` (從個人角度看 , 從組語model才是比較好的) 從驗證使用的公理化理論來看例如Hoare Logic 要考慮的是語義(semantics)與rule/公理以一段c++ code為例子 ``` b = 72; ``` 如果考慮 b是class的object的話 =的語義 , 就不是單純的assign 因為C++有operator overloading 所以=的語義不是單純的assign 而是要看實作這變成Hoare Logic的公理無法使用而要另外定義從這邊可以看出公理/rule應該是一些公認的事實所以用定理證明的形式化驗證可以說 ``` 基於一些基本的事實用嚴密的邏輯推理驗證系統的性質 (proof checker檢查推理正不正確) ``` 補充跟限制有關的資料內容來自[連結](http://cs4161.web.cse.unsw.edu.au/week01A_anim.pdf)第70頁 ``` 1. OS and H/W issues reduced by using different systems 2. runtime/compiler bugs reduced by using different compilers 3. faulty implementation reduced by having the right prover architecture 4. inconsistent logic reduced by implementing and analysing it 5. wrong theorem reduced by expressive/intuitive logics ``` 這五點指的是如何使驗證model就是驗證implementation 這性質更為穩健的方法 1 , 2　點上面提過 3是指使用正確的實作的proof checker 4是指避免使用自相矛盾的公理系統 5自然就是把邏輯學好拉 ## Vcg與hoare logic 整段解釋的code [連結](https://github.com/KevinKu/Formal-verification-of-simple-C-code/blob/master/hoare_logic_test.thy) ``` theory hoare_logic_test imports "~~/src/HOL/Hoare/Separation" begin lemma "VARS x {P} SKIP {P}" apply vcg done lemma "VARS x {x=5} x:=7 {x=5}" apply vcg apply auto sorry lemma "VARS x {P} SKIP;SKIP {P}" apply vcg done lemma "VARS x {P} IF R THEN SKIP ELSE SKIP FI {Q}" apply vcg sorry lemma "VARS x {P} WHILE S INV{I} DO SKIP OD {Q}" apply vcg sorry end ``` vcg是verification condition generator 的縮寫實際上這method的目的很簡單 , 就是把command去掉利用command的rule與公理 , 去掉command 最終得到一串邏輯敘述來看前面code內的lemma就可以看到vcg的作用 ### SKIP ``` lemma "VARS x {P} SKIP {P}" apply vcg done ``` "apply vcg" proof state ``` proof (prove) goal: No subgoals! ``` 可以如此是由於SKIP的公理與Precondition strengthening推導出來最終是p推到p 所以就自動推理完畢 , 沒有目標要證了 ### assignment ``` lemma "VARS x {x=5} x:=7 {x=5}" apply vcg apply auto sorry ``` "apply vcg" proof state ``` proof (prove) goal (1 subgoal): 1. ⋀x. x = 5 ⟹ 7 = 5 ``` 實際上就是投影片內提到的要證這三元組是True 證 ``` P ⇒ Q[y/x] ``` 這邊P是x=5 Q原本是x=5 Q[y/x]經過代換後 , 變成7=5 ### sequence ``` lemma "VARS x {P} SKIP;SKIP {P}" apply vcg done ``` "apply vcg" prood state ``` proof (prove) goal: No subgoals! ``` 自動推理推掉了中間過程是: P推到P P再推到P 根據sequence的rule , 加上SKIP的公理 ### IF ``` lemma "VARS x {P} IF R THEN SKIP ELSE SKIP FI {Q}" apply vcg sorry ``` "apply vcg" proof state ``` proof (prove) goal (1 subgoal): 1. ⋀x. P ⟹ (R ⟶ Q) ∧ (¬ R ⟶ Q) ``` 跟投影片關於IF的rule比對看看有點出入 ⟹這個符號可以是 " ⟹ ", 也可以是 " , " 比較投影片的rule 應該會得到兩個前提 ``` { P ∧ R }SKIP{ Q }與{ P ∧ ~R }SKIP{ Q } ``` 由SKIP的公理與Precondition strengthening 會有 ``` P ∧ R ⟶ Q 與 P ∧ ~R ⟶ Q ``` 與是∧ 整個整理後就有proof state的subgoal ### WHILE ``` lemma "VARS x {P} WHILE S INV{I} DO SKIP OD {Q}" apply vcg sorry ``` "apply vcg" proof state ``` proof (prove) goal (3 subgoals): 1. ⋀x. P ⟹ I 2. ⋀x. I ∧ S ⟹ I 3. ⋀x. I ∧ ¬ S ⟹ Q ``` 這很明顯是投影片驗證WHILE的內容了補充一點 , 這三個條件是部份正確性的證明完全正確性還需要證明終止 ## Demo.c的model 前置斷言與後置斷言和循環不變式下一節說明這節說明模型怎麼建 VARS使用說明 ### f() C code: ``` unsigned int max = 0; if(max < 82) { max = 82; } if(max < 43) { max = 43; } ``` model: ``` lemma "VARS max::nat {} max:=0; IF max < 82 THEN max := 82 ELSE SKIP FI; IF max < 43 THEN max := 43 ELSE SKIP FI {}" ``` VARS的使用是這樣的 ``` VARS 程式變數 {前置斷言}command{後置斷言} ``` 每個部份空格隔開這段c code會出現的變數就是max 所以有max::nat 這" ::nat "的意思是 ``` max的type為nat nat是自然數的意思 ``` 這裡我用自然數來表示max的性質原始的code是無符號的整數 nat可以表示數值 , 但並沒有完整敘述變數的性質無符號整數是有範圍 , 而任意的自然數並沒有但是這邊要證的性質 , 不需要有範圍這個性質所以type是自然數不影響要驗證的性質接下來的command ``` max:=0; IF max < 82 THEN max := 82 ELSE SKIP FI; IF max < 43 THEN max := 43 ELSE SKIP FI ``` 就是根據C code的semantics對應的翻譯過去應該很明顯 , 就不細說了 ### g() C code: ``` unsigned int max = 0; unsigned int a[3] ; a[0] = 45; a[1] = 36; a[2] = 12; unsigned int i = 0; while(i < 3) { if(max < a[i]) { max = a[i]; } i = i+1; } ``` model: ``` lemma "VARS (max::nat) (a::nat list) (i::nat) {} max:=0; a[0]:=45; a[1]:=36; a[2]:=12; i :=0 ; WHILE i < 3 INV{} DO IF max < (a!i) THEN max:=(a!i) ELSE SKIP FI; i:=i+1 OD {}" ``` 這邊特別說明(a::nat list) Hoare Logic library有提供array的抽象type就是" 'a list " 'a是type變數某種意義上任何type的符號都可以(i.e : int,nat,nat set...) list定義在list.thy 它的符號表示跟array類似這邊出現" a!i " 所以來說明a!i是甚麼 i是list的index 一個list表示是[e1 e2 e3....] en 皆為符號 , 有不同的type a!i 就代表list內某個ei的意思 ## 驗證性質的形式化表示把完整的model code貼上來 ### f() [Try_.thy](https://github.com/KevinKu/Formal-verification-of-simple-C-code/blob/master/Try_.thy) ``` lemma "VARS max::nat { True } max:=0; IF max < 82 THEN max := 82 ELSE SKIP FI; IF max < 43 THEN max := 43 ELSE SKIP FI {max = 82}" ``` 看Goal ``` prove that the variable max equals 82. ``` 要驗證run完這段code , max是82 max是82用形式表示 , 就是max=82 而執行完是放在Hoare triple的後置斷言部份至於前置斷言 , 由於max是 local variable 所以前置斷言只要是True的邏輯敘述都行這邊簡單起見 , 就用True了 ### g() ``` lemma "VARS (max::nat) (a::nat list) (i::nat) {length a = 3} max:=0; a[0]:=45; a[1]:=36; a[2]:=12; i :=0 ; WHILE i < 3 INV{if i = 0 then max = 0 else (∀j<i. a!j≤max)} DO IF max < (a!i) THEN max:=(a!i) ELSE SKIP FI; i:=i+1 OD {∀j<i. max≥(a!j)}" ``` 看Goal ``` prove that the variable max is bigger than element of array a or equals some element of array a. ``` 要驗證run完整段code max會大於等於array中的元素 array中的元素就是任一個array中的元素所以形式的表示是 ``` "∀j. a!j" ``` 但是array是有固定大小的所以以這個例子是 ``` "∀j<3. a!j" ``` max要大於等於所以整個就是 ``` "∀j<3. a!j ≤ max " ``` 不過剛好 , 跳出while loop時 , i會是3 實際上還是寫3比較好所以後置斷言 , 就是 ``` ∀j<i. max≥(a!j) ``` 前置斷言 , a在code宣告為3個int的array 所以length a = 3是在assign command前是True的事實由於有assign的command 所以前置斷言選用這個事實接下來是INV內的邏輯敘述怎麼給了由於循環不變式(loop invariant)要求while command前也是對的 while command後也是對的(while loop執行完) 這邊比較麻煩看後置斷言這後置斷言在while command不會是True 所以得hack一下在while command前 max=0這是可以肯定為True 所以使用if _ then _ else _ 這語法糖來造loop invariant if P then Q else R 實際上就是 ``` (P ⟶ Q) ∧ (~P ⟶ R) ``` 而max=0是True就是i=0是True的情況因此 loop invariant就是 ``` if i = 0 then max = 0 else (∀j<i. a!j≤max) ``` ## 證明 [answer.thy](https://github.com/KevinKu/Formal-verification-of-simple-C-code/blob/master/answer.thy) ### f() ``` lemma "VARS max::nat { True } max:=0; IF max < 82 THEN max := 82 ELSE SKIP FI; IF max < 43 THEN max := 43 ELSE SKIP FI {max = 82}" apply vcg apply simp done ``` 先說Isabelle/HOL 內建自動推理寫證明腳本的指令(apply xxx) 會做自動推理所以需要知道的是 , subgoal出現甚麼形式要用哪種證明策略來使用 apply vcg幾乎是起手式來看一下apply vcg後的subgoal ``` proof (prove) goal (1 subgoal): 1. ⋀max. True ⟹ (0 < 82 ⟶ (82 < 43 ⟶ 43 = 82) ∧ (¬ 82 < 43 ⟶ 82 = 82)) ∧ (¬ 0 < 82 ⟶ (0 < 43 ⟶ 43 = 82) ∧ (¬ 0 < 43 ⟶ 0 = 82)) ``` 看起來都是logic相關的符號所以嘗試simp "apply simp" proof state ``` proof (prove) goal: No subgoals! ``` 自動推理完了沒有還要證的subgoal 下done表示證畢 "done" proof state ``` theorem {True} max := 0; IF max < 82 THEN max := 82 ELSE SKIP FI; IF max < 43 THEN max := 43 ELSE SKIP FI {max = 82} ``` ### g() ``` lemma "VARS (max::nat) (a::nat list) (i::nat) {length a = 3} max:=0; a[0]:=45; a[1]:=36; a[2]:=12; i :=0 ; WHILE i < 3 INV{if i = 0 then max = 0 else (∀j<i. a!j≤max)} DO IF max < (a!i) THEN max:=(a!i) ELSE SKIP FI; i:=i+1 OD {∀j<i. max≥(a!j)}" apply vcg apply simp apply simp apply (rule conjI) apply (rule impI) apply rule apply (rule impI) apply (erule less_SucE) apply auto apply (erule less_SucE) apply auto done ``` 這邊的rule , 基本上就是符號邏輯的東西特別來講使用erule less_SucE的情況挑第一個說明就可以 , 因為第二次使用是類似的 "apply (rule impI)"第二次使用的 proof state ``` proof (prove) goal (3 subgoals): 1. ⋀max a i j. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ max < a ! i ⟹ j < Suc i ⟹ a ! j ≤ a ! i 2. ⋀max a i. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ ¬ max < a ! i ⟶ (∀j<Suc i. a ! j ≤ max) 3. ⋀max a i. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ ¬ i < 3 ⟹ ∀j<i. a ! j ≤ max ``` 看第一個subgoal(apply 預設作用在第一個subgoal) ``` 1. ⋀max a i j. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ max < a ! i ⟹ j < Suc i ⟹ a ! j ≤ a ! i ``` 這邊分析一下 j < Suc i 就是 j < i+1 那代表要討論 j=i 與 j<i 的情況 ``` j=i ``` a!j ≤ a!i 就是 a!i ≤ a!i 這一定對 ``` j<i ``` 由 a ! j ≤ max 與 max < a ! i 可以得到 a!j ≤ a!i 的結論所以問題就是 , Suc i 要用甚麼策略拆開? 剛好less_SucE這erule就是合適的來看一下這erule的內容 (在[Nat.thy](https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/Nat.html)裡面) ``` lemma less_SucE: assumes major: "m < Suc n" and less: "m < n ⟹ P" and eq: "m = n ⟹ P" shows P apply (rule major [THEN lessE]) apply (rule eq) apply blast apply (rule less) apply blast done ``` 恩簡單說這可以把 (j < Suc i) ⟹ P 拆成兩個subgoal j < i ⟹ P 和 j = i ⟹ P 所以來看下一行 "apply (erule less_ScuE)" 的proof state ``` proof (prove) goal (4 subgoals): 1. ⋀max a i j. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ max < a ! i ⟹ j < i ⟹ a ! j ≤ a ! i 2. ⋀max a i j. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ max < a ! i ⟹ j = i ⟹ a ! j ≤ a ! i 3. ⋀max a i. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ ¬ max < a ! i ⟶ (∀j<Suc i. a ! j ≤ max) 4. ⋀max a i. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ ¬ i < 3 ⟹ ∀j<i. a ! j ≤ max ``` 看第一個和第二個 ``` 1. ⋀max a i j. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ max < a ! i ⟹ j < i ⟹ a ! j ≤ a ! i 2. ⋀max a i j. (if i = 0 then max = 0 else ∀j<i. a ! j ≤ max) ∧ i < 3 ⟹ max < a ! i ⟹ j = i ⟹ a ! j ≤ a ! i ``` j < i 與 j = i 的情況變成subgoal了剩下就嘗試auto或simp把subgoal證完 ###### tags: `formal verification`