---
# System prepended metadata

title: 形式化驗證與 cbmc

---

# 形式化驗證與 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
```