形式化驗證與 cbmc

cbmc: Bounded Model Checker for C/C++ programs

背景知識: 形式化驗證
Model checking 的具體作法是狀態空間檢索 (state-space search)，原理就是將程式或通訊協定看作一個分散式系統，局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發。
使用事件自動機規約的 C 語言有界模型檢測

定義：事件

我們定義程式中「一道敘述的執行完成」為「一個事件的發生」，所產生事件的名稱可以是程式中某個函式的名稱，也可以是我們自定義的名稱
事件的參數可以是程式中的表達式，也可以是一個常數
將某個事件與一條執行敘述建立關聯 (綁定)，就意味著當程式執行完該敘述之後，程式將產生一個事件傳遞給事件自動機，事件自動機會根據事件流對程式行為進行監控

下方示範對函式 sum 綁定事件 sum(a, b)，在執行完最後一條敘述return s 後，將產生該事件，每當該函式被呼叫執行一次後，都會產生該事件。

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) 可看成是一種模型，用來描述擁有極為有限的記憶體的電腦。在這麼少的記憶體的情況下，這種電腦能有什麼作用呢 ? 其實日常生活中有很多設備都具有類似的功能，例如下圖顯示的自動門，假如有人站在前感應區，則自動門應該開啟，即使行人通過前感應區，來到後感應區，自動門還是要開啟一下，讓行人有足夠的時間離開。
自動門的作用可用狀態圖 (state diagram) 來表示
- 自動門的狀態有兩種: 開啟 (open) 或是關閉 (closed)
- 可能發生的情況則有 4 種，就是前感應區有人 (front)、後感應區有人 (rear)、都有人 (both) 或是都沒人 (neither)
上圖的狀態圖清楚地顯示出當什麼情況發生時，自動門的狀態會有什麼變化。控制自動門的設備就像是一種有限自動機，只有單一位元(bit)的記憶體。
延伸閱讀: 自動機理論

下圖示範一個描述檔案操作的事件自動機實例，有 3 個狀態:

s₀ 是初始狀態
s₁ 是在打開一個檔案後的狀態
s₂ 是接受狀態

當自動機接收到一個 open 事件後，就將 open 中的參數指派到自動機變數f。顯然，自動機描述了所有打開一個檔案後，但是程式終止時卻沒有關閉檔案的執行路徑。

在狀態 s₀ 使用完全事件，好處在於當程式同時打開多個檔案時，可以只用這一個事件自動機進行表達。

編譯 cbmc

cbmc 發展很快，Ubuntu Linux 內建的版本較舊，最好都從 GitHub 取得最新的程式碼
移除過去安裝的 cbmc 套件 (選擇性)

$ sudo apt remove minisat cbmc

取得必要的套件

$ sudo apt install ccache doxygen cmake flex bison

取得 cbmc 原始程式碼並編譯 (注意最後的 .，不要漏掉)

$ git clone https://github.com/diffblue/cbmc
$ cd cbmc
$ cmake -DCMAKE_CXX_FLAGS="-Ofast" .

上一步預期會看到類似 Build files have been written to: /home/jserv/cbmc 的輸出訊息，就可以著手編譯:

$ make -j

編譯成功後，會在 bin/ 目錄見到 cbmc 一類的執行檔。複製到 $HOME/.local/bin 或者其他 $PATH 環境變數可找到的目錄

$ cp -af bin/* ~/.local/bin/

測試案例

自 sidneycadot/cbmc 取得示範的程式碼

$ mkdir -p ~/workspace
$ cd ~/workspace
$ git clone https://github.com/sidneycadot/cbmc cbmc-examples
$ cd cbmc-examples

示範: binary_search

$ 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

$ cd fft-structure
$ cbmc fft.c

參考輸出:

** Results:
[main.assertion.1] assertion !ok: FAILURE

** 1 of 1 failed (1 iteration)
VERIFICATION FAILED

示範: logic (簡易的直譯器/虛擬機器)

$ 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 會驗證失敗:

$ 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

回頭閱讀 logic.c，對照上述訊息，思考為什麼

示範: minesweeper

$ 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

以 moxiebox 為例，使用 cbmc

依據隔離執行環境的建構與應用，做好必要的 moxiebox 開發準備
moxiebox/runtime/Makefile 有個 verify 標的，可透過 cbmc 來驗證由 Ilya O. Levin 開發、獨立於 moxiebox 專案的 SHA256 實作
切換到 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 從原本的

for (size_t i = 0; i < (sizeof(buf) / sizeof(buf[0])); i += 2) {

將「小於」換成「小於等於」，如下：

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

形式化驗證與 cbmc

cbmc: Bounded Model Checker for C/C++ programs

編譯 cbmc

測試案例

以 moxiebox 為例，使用 cbmc

Read more

留意浮點數運算的陷阱

位元旋轉實作和 Linux 核心案例

圖解傅立葉分析

你所不知道的 C 語言: 浮點數運算