# 形式化驗證與 cbmc ## [cbmc](http://www.cprover.org/cbmc/): Bounded Model Checker for C/C++ programs * 背景知識: [形式化驗證](https://hackmd.io/s/H1xxp3pF0) * Model checking 的具體作法是狀態空間檢索 (state-space search)，原理就是將程式或通訊協定看作一個分散式系統，局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發。 * [使用事件自動機規約的 C 語言有界模型檢測](http://www.jos.org.cn/html/2014/11/4609.htm) - [ ] 定義：事件 * 我們定義程式中「一道敘述的執行完成」為「一個事件的發生」，所產生事件的名稱可以是程式中某個函式的名稱，也可以是我們自定義的名稱 * 事件的參數可以是程式中的表達式，也可以是一個常數 * 將某個事件與一條執行敘述建立關聯 (綁定)，就意味著當程式執行完該敘述之後，程式將產生一個事件傳遞給事件自動機，事件自動機會根據事件流對程式行為進行監控 下方示範對函式 `sum` 綁定事件 `sum(a, b)`，在執行完最後一條敘述`return s` 後，將產生該事件，每當該函式被呼叫執行一次後，都會產生該事件。 ```C int sum(int a, int b) { int s = a + b; return s; } ``` 在這個事件自動機中，自動機變數和事件的參數類型限制在整型 (int)、實數 (real) 和布林值 (bool)。 C 程式中也會保存字元串類型的變數，在綁定事件時，可以進行映射，也就是說，將字串型變數映射到整數型態。事件自動機變數不可以是指標型態，因為指標型態如果指向程式中的變數地址，會導致自動機轉移修改程序的變數，這在監視過程中是不允許的。 - [ ] 自動機 (automata) * 自動機理論 (automata theory) 探討運算的數學模型，包括相關的定義與特性，這些模型在很多電腦科學的應用領域中都扮演相當重要的角色。其中有限自動機 (finite automation)應用於 text processing, compiler 與硬體設計，與上下文無關的文法 (context-free grammar) 則運用於程式語言與人工智慧 * 自動機理論很適合當做運算理論的入門主題，因為運算性的理論與複雜度理論都需要電腦的精確定義，這在自動機理論中經常可以看到實際的例子 * 有限自動機 (finite automata) 可看成是一種模型，用來描述擁有極為有限的記憶體的電腦。在這麼少的記憶體的情況下，這種電腦能有什麼作用呢 ? 其實日常生活中有很多設備都具有類似的功能，例如下圖顯示的自動門，假如有人站在前感應區，則自動門應該開啟，即使行人通過前感應區，來到後感應區，自動門還是要開啟一下，讓行人有足夠的時間離開。 ![](https://i.imgur.com/9vBOj4s.png) * 自動門的作用可用狀態圖 (state diagram) 來表示 * 自動門的狀態有兩種: 開啟 (open) 或是關閉 (closed) * 可能發生的情況則有 4 種，就是前感應區有人 (front)、後感應區有人 (rear)、都有人 (both) 或是都沒人 (neither) * 上圖的狀態圖清楚地顯示出當什麼情況發生時，自動門的狀態會有什麼變化。控制自動門的設備就像是一種有限自動機，只有單一位元(bit)的記憶體。 * 延伸閱讀: [自動機理論](http://prompt.nou.edu.tw/web/sno204/content/w01/01-02-01t.htm) 下圖示範一個描述檔案操作的事件自動機實例，有 3 個狀態: * s~0~ 是初始狀態 * s~1~ 是在打開一個檔案後的狀態 * s~2~ 是接受狀態 當自動機接收到一個 open 事件後，就將 open 中的參數指派到自動機變數`f`。顯然，自動機描述了所有打開一個檔案後，但是程式終止時卻沒有關閉檔案的執行路徑。 在狀態 s~0~ 使用完全事件，好處在於當程式同時打開多個檔案時，可以只用這一個事件自動機進行表達。 ![](https://i.imgur.com/ArEkNku.png) ## 編譯 [cbmc](http://www.cprover.org/cbmc/) * [cbmc](http://www.cprover.org/cbmc/) 發展很快，Ubuntu Linux 內建的版本較舊，最好都從 GitHub 取得最新的程式碼 * 移除過去安裝的 cbmc 套件 (選擇性) ```shell $ sudo apt remove minisat cbmc ``` * 取得必要的套件 ```shell $ sudo apt install ccache doxygen cmake flex bison ``` * 取得 cbmc 原始程式碼並編譯 (注意最後的 `.`，不要漏掉) ```shell $ git clone https://github.com/diffblue/cbmc $ cd cbmc $ cmake -DCMAKE_CXX_FLAGS="-Ofast" . ``` * 上一步預期會看到類似 `Build files have been written to: /home/jserv/cbmc` 的輸出訊息，就可以著手編譯: ```shell $ make -j ``` * 編譯成功後，會在 `bin/` 目錄見到 `cbmc` 一類的執行檔。複製到 `$HOME/.local/bin` 或者其他 `$PATH` 環境變數可找到的目錄 ```shell $ cp -af bin/* ~/.local/bin/ ``` ## 測試案例 * 自 `sidneycadot/cbmc` 取得示範的程式碼 ```shell $ mkdir -p ~/workspace $ cd ~/workspace $ git clone https://github.com/sidneycadot/cbmc cbmc-examples $ cd cbmc-examples ``` - [ ] 示範: binary_search ```shell $ cd binary_search $ cbmc --unwind 20 binary_search.c ``` * 參考輸出: ``` ** Results: [test_bsearch.assertion.1] assertion linear_search_result == binary_search_result: SUCCESS [test_sort.assertion.1] assertion is_sorted(x, size): SUCCESS ** 0 of 2 failed (1 iteration) VERIFICATION SUCCESSFUL ``` - [ ] 示範: fft-structure ```shell $ cd fft-structure $ cbmc fft.c ``` * 參考輸出: ``` ** Results: [main.assertion.1] assertion !ok: FAILURE ** 1 of 1 failed (1 iteration) VERIFICATION FAILED ``` - [ ] 示範: logic (簡易的直譯器/虛擬機器) ```shell $ cd logic $ cbmc logic.c ``` * 參考輸出: ``` size of program expression: 28102 steps simple slicing removed 0 assignments Generated 0 VCC(s), 0 remaining after simplification VERIFICATION SUCCESSFUL ``` 倘若 model checking 的條件更嚴格，像是追加 `--bounds-check --pointer-check` 參數，那 cbmc 會驗證失敗: ```shell $ cbmc --bounds-check --pointer-check logic.c ``` * 參考輸出: ``` [run_program.pointer_dereference.27] dereference failure: deallocated dynamic object in STACK[(signed long int)STACKPTR]: SUCCESS [run_program.pointer_dereference.28] dereference failure: dead object in STACK[(signed long int)STACKPTR]: FAILURE [run_program.pointer_dereference.29] dereference failure: pointer outside dynamic object bounds in STACK[(signed long int)STACKPTR]: SUCCESS [run_program.pointer_dereference.30] dereference failure: pointer outside object bounds in STACK[(signed long int)STACKPTR]: FAILURE [run_program.pointer_dereference.31] dereference failure: pointer outside dynamic object bounds in STACK[(signed long int)((signed int)STACKPTR - 1)]: SUCCESS [run_program.pointer_dereference.32] dereference failure: pointer outside object bounds in STACK[(signed long int)((signed int)STACKPTR - 1)]: FAILURE ... ** 54 of 170 failed (29 iterations) VERIFICATION FAILED ``` :::info 回頭閱讀 `logic.c`，對照上述訊息，思考為什麼 ::: - [ ] 示範: minesweeper ```shell $ cd minesweeper $ cbmc minesweeper.c ``` * 參考輸出: ``` size of program expression: 283 steps simple slicing removed 0 assignments Generated 1 VCC(s), 0 remaining after simplification VERIFICATION SUCCESSFUL ``` * 務必詳閱 [CBMC: Bounded Model Checking for C/C++ and Java: A Short Tutorial](http://www.cprover.org/cprover-manual/cbmc.shtml) ## 以 [moxiebox](https://github.com/sysprog21/moxiebox) 為例，使用 cbmc * 依據 [隔離執行環境的建構與應用](https://hackmd.io/s/Hk9HLRbkf)，做好必要的 [moxiebox](https://github.com/sysprog21/moxiebox) 開發準備 * [moxiebox/runtime/Makefile](https://github.com/sysprog21/moxiebox/blob/master/runtime/Makefile) 有個 `verify` 標的，可透過 cbmc 來驗證由 Ilya O. Levin 開發、獨立於 moxiebox 專案的 [SHA256 實作](https://github.com/sysprog21/moxiebox/blob/master/runtime/sha256.c) * 切換到 `runtime` 目錄，執行 `$ make verify` 命令，參考輸出如下: (需要等待，請保持耐心) ``` ... [_hash.pointer_dereference.53] dereference failure: pointer outside dynamic object bounds in *ctx: SUCCESS [_hash.pointer_dereference.54] dereference failure: pointer outside object bounds in *ctx: SUCCESS [_hash.array_bounds.38] array.hash lower bound in ctx->hash[(signed long int)7]: SUCCESS [_hash.array_bounds.39] array.hash dynamic object upper bound in ctx->hash[(signed long int)7]: SUCCESS [__CPROVER__start.memory-leak.1] dynamically allocated memory never freed in __CPROVER_memory_leak == NULL: SUCCESS ** 0 of 550 failed (1 iteration) VERIFICATION SUCCESSFUL ``` * 通過了 cbmc 以下條件: * --unwind 8 --partial-loops * --bounds-check --pointer-check * --div-by-zero-check * --signed-overflow-check * 修改 `sha256_test.c`，將 Line #35 從原本的 ```C for (size_t i = 0; i < (sizeof(buf) / sizeof(buf[0])); i += 2) { ``` 將「小於」換成「小於等於」，如下： ```C for (size_t i = 0; i <= (sizeof(buf) / sizeof(buf[0])); i += 2) { ``` * 重新執行 `$ make verify`，得到不同的輸出訊息: ``` SAT checker: instance is UNSATISFIABLE Runtime decision procedure: 49.985s ** Results: [main.array_bounds.1] array `buf' upper bound in buf[(signed long int)i]: FAILURE [main.array_bounds.2] array `buf' upper bound in buf[(signed long int)i]: FAILURE [main.array_bounds.3] array `buf' upper bound in buf[(signed long int)i]: FAILURE [main.array_bounds.4] array `buf' upper bound in buf[(signed long int)(i + (unsigned long int)1)]: FAILURE ... ** 16 of 550 failed (6 iterations) VERIFICATION FAILED ```