HackMD - Collaborative Markdown Knowledge Base

## Model Checking ### cbmc `簡介:` cbmc 就像編譯器, 會翻譯程式並集結所有 functions, 但他不會產生 binary code, 而是進行其他的模擬。 * A bounded model checker for C and C++ programs * It supports C89, C99, most of C11 and most compiler extensions provided by gcc and Visual Studio, and also SystemC using Scoot * It allows verifying array bounds (buffer overflows), pointer safety, exceptions and user-specified assertions * It can check C and C++ for consistency with other languages * The verification is performed by [unwinding the loops](https://en.wikipedia.org/wiki/Loop_unrolling) in the program and passing the resulting equation to a decision procedure `應用:` * [Applications of CBMC](http://www.cprover.org/cbmc/applications/) * 主要用來除錯及偵測潛在的錯誤 ### cbmc 開源碼測試 `cbmc -h` ``` * * CBMC 5.8 - Copyright (C) 2001-2017 (64-bit version) * * * * Daniel Kroening, Edmund Clarke * * * * Carnegie Mellon University, Computer Science Department * * * * kroening@kroening.com * * * * Protected in part by U.S. patent 7,225,417 * * Usage: Purpose: cbmc [-?] [-h] [--help] show help cbmc file.c ... source file names Analysis options: --show-properties show the properties, but don't run analysis --symex-coverage-report f generate a Cobertura XML coverage report in f --property id only check one specific property --stop-on-fail stop analysis once a failed property is detected --trace give a counterexample trace for failed properties C/C++ frontend options: -I path set include path (C/C++) -D macro define preprocessor macro (C/C++) --preprocess stop after preprocessing --16, --32, --64 set width of int --LP64, --ILP64, --LLP64, --ILP32, --LP32 set width of int, long and pointers --little-endian allow little-endian word-byte conversions --big-endian allow big-endian word-byte conversions --unsigned-char make "char" unsigned by default --mm model set memory model (default: sc) --arch set architecture (default: x86_64) --os set operating system (default: linux) --c89/99/11 set C language standard (default: c99) --cpp98/03/11 set C++ language standard (default: cpp98) --no-arch don't set up an architecture --no-library disable built-in abstract C library --round-to-nearest rounding towards nearest even (default) --round-to-plus-inf rounding towards plus infinity --round-to-minus-inf rounding towards minus infinity --round-to-zero rounding towards zero --function name set main function name Program representations: --show-parse-tree show parse tree --show-symbol-table show symbol table --show-goto-functions show goto program --drop-unused-functions drop functions trivially unreachable from main function Program instrumentation options: --bounds-check enable array bounds checks --pointer-check enable pointer checks (always enabled for Java) --memory-leak-check enable memory leak checks --div-by-zero-check enable division by zero checks --signed-overflow-check enable signed arithmetic over- and underflow checks --unsigned-overflow-check enable arithmetic over- and underflow checks --pointer-overflow-check enable pointer arithmetic over- and underflow checks --conversion-check check whether values can be represented after type cast --undefined-shift-check check shift greater than bit-width --float-overflow-check check floating-point for +/-Inf --nan-check check floating-point for NaN --no-built-in-assertions ignore assertions in built-in library --no-assertions ignore user assertions --no-assumptions ignore user assumptions --error-label label check that label is unreachable --cover CC create test-suite with coverage criterion CC --mm MM memory consistency model for concurrent programs Semantic transformations: --nondet-static add nondeterministic initialization of variables with static lifetime BMC options: --program-only only show program expression --show-loops show the loops in the program --depth nr limit search depth --unwind nr unwind nr times --unwindset L:B,... unwind loop L with a bound of B (use --show-loops to get the loop IDs) --show-vcc show the verification conditions --slice-formula remove assignments unrelated to property --unwinding-assertions generate unwinding assertions --partial-loops permit paths with partial loops --no-pretty-names do not simplify identifiers --graphml-witness filename write the witness in GraphML format to filename Backend options: --object-bits n number of bits used for object addresses --dimacs generate CNF in DIMACS format --beautify beautify the counterexample (greedy heuristic) --localize-faults localize faults (experimental) --smt1 use default SMT1 solver (obsolete) --smt2 use default SMT2 solver (Z3) --boolector use Boolector --mathsat use MathSAT --cvc4 use CVC4 --yices use Yices --z3 use Z3 --refine use refinement procedure (experimental) --refine-strings use string refinement (experimental) --string-non-empty add constraint that strings are non empty (experimental) --string-printable add constraint that strings are printable (experimental) --string-max-length add constraint on the length of strings --string-max-input-length add constraint on the length of input strings --outfile filename output formula to given file --arrays-uf-never never turn arrays into uninterpreted functions --arrays-uf-always always turn arrays into uninterpreted functions Other options: --version show version and exit --xml-ui use XML-formatted output --xml-interface bi-directional XML interface --json-ui use JSON-formatted output --verbosity # verbosity level ``` #### binary_search `$ cbmc --unwind 20 binary_search.c` Output: ``` ** 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 ``` 參考 [Understanding Loop Unwinding](http://www.cprover.org/cprover-manual/cbmc-loops.shtml) * 一般情況, cbmc 自動判斷要執行多少次 iterations * 當 iterations 次數是 data-dependent 的, unwind bound 可能會失敗, 因此要加上 command `--unwind B`, B 為在每個迴圈裡 loop unwindings cbmc 的最大值。 `$ cbmc --unwind 20 binary_search.c` ``` size of program expression: 10135 steps simple slicing removed 10 assignments Generated 22 VCC(s), 19 remaining after simplification Passing problem to propositional reduction converting SSA Running propositional reduction Post-processing Solving with MiniSAT 2.2.1 with simplifier 200202 variables, 764586 clauses SAT checker: instance is UNSATISFIABLE Runtime decision procedure: 1.159s ``` `$ cbmc --unwind 100 binary_search.c` ``` size of program expression: 26935 steps simple slicing removed 10 assignments Generated 22 VCC(s), 19 remaining after simplification Passing problem to propositional reduction converting SSA Running propositional reduction Post-processing Solving with MiniSAT 2.2.1 with simplifier 868336 variables, 4119797 clauses SAT checker: instance is UNSATISFIABLE Runtime decision procedure: 7s ``` #### fft-structure `$ cbmc fft.c` Output: ``` ** Results: [main.assertion.1] assertion !ok: FAILURE ** 1 of 1 failed (1 iteration) VERIFICATION FAILED ``` `$ cbmc --unwind 4 fft.c` ``` ** Results: [main.assertion.1] assertion !ok: SUCCESS ** 0 of 1 failed (1 iteration) ``` `$ cbmc --unwind 5 fft.c` ``` ** Results: [main.assertion.1] assertion !ok: FAILURE ** 0 of 1 failed (1 iteration) ``` 從以上的測試看出, bug 出現在第五個 loop #### logic `$ cbmc logic.c` Output: ``` size of program expression: 28102 steps simple slicing removed 0 assignments Generated 0 VCC(s), 0 remaining after simplification VERIFICATION SUCCESSFUL ``` `$ cbmc --bounds-check --pointer-check logic.c` Output: ``` [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 ``` `$ cbmc logic.c --bounds-check --pointer-check --trace` ``` Violated property: file logic.c line 136 function run_program dereference failure: pointer outside object bounds in STACK[(signed long int)STACKPTR] POINTER_OFFSET(STACK) + (signed long int)STACKPTR >= 0l && OBJECT_SIZE(STACK) >= 1ul + (unsigned long int)POINTER_OFFSET(STACK) + (unsigned long int)(signed long int)STACKPTR || DYNAMIC_OBJECT(STACK) Violated property: file logic.c line 184 function run_program dereference failure: pointer outside object bounds in STACK[(signed long int)STACKPTR] POINTER_OFFSET(STACK) + (signed long int)STACKPTR >= 0l && OBJECT_SIZE(STACK) >= 1ul + (unsigned long int)POINTER_OFFSET(STACK) + (unsigned long int)(signed long int)STACKPTR || DYNAMIC_OBJECT(STACK) Violated property: file logic.c line 305 function main array `STACK' upper bound in STACK[(signed long int)((signed int)STACKPTR - 2)] !((signed long int)(-2 + (signed int)STACKPTR) >= 16l) Violated property: file logic.c line 306 function main array `STACK' upper bound in STACK[(signed long int)((signed int)STACKPTR - 1)] !((signed long int)(-1 + (signed int)STACKPTR) >= 16l) Violated property: file logic.c line 136 function run_program dereference failure: pointer outside object bounds in STACK[(signed long int)STACKPTR] POINTER_OFFSET(STACK) + (signed long int)STACKPTR >= 0l && OBJECT_SIZE(STACK) >= 1ul + (unsigned long int)POINTER_OFFSET(STACK) + (unsigned long int)(signed long int)STACKPTR || DYNAMIC_OBJECT(STACK) Violated property: file logic.c line 148 function run_program dereference failure: dead object in STACK[(signed long int)STACKPTR] !(POINTER_OBJECT(STACK) == POINTER_OBJECT(__CPROVER_dead_object)) Violated property: file logic.c line 77 function run_program dereference failure: dead object in STACK[(signed long int)tmp_post$4] !(POINTER_OBJECT(STACK) == POINTER_OBJECT(__CPROVER_dead_object)) Violated property: file logic.c line 83 function run_program dereference failure: dead object in STACK[(signed long int)STACKPTR] !(POINTER_OBJECT(STACK) == POINTER_OBJECT(__CPROVER_dead_object)) Violated property: file logic.c line 220 function run_program dereference failure: dead object in STACK[(signed long int)STACKPTR] !(POINTER_OBJECT(STACK) == POINTER_OBJECT(__CPROVER_dead_object)) Violated property: file logic.c line 202 function run_program dereference failure: pointer outside object bounds in STACK[(signed long int)STACKPTR] POINTER_OFFSET(STACK) + (signed long int)STACKPTR >= 0l && OBJECT_SIZE(STACK) >= 1ul + (unsigned long int)POINTER_OFFSET(STACK) + (unsigned long int)(signed long int)STACKPTR || DYNAMIC_OBJECT(STACK) Violated property: file logic.c line 211 function run_program dereference failure: pointer outside object bounds in STACK[(signed long int)STACKPTR] POINTER_OFFSET(STACK) + (signed long int)STACKPTR >= 0l && OBJECT_SIZE(STACK) >= 1ul + (unsigned long int)POINTER_OFFSET(STACK) + (unsigned long int)(signed long int)STACKPTR || DYNAMIC_OBJECT(STACK) Violated property: file logic.c line 227 function run_program dereference failure: dead object in *stackptr !(POINTER_OBJECT(stackptr) == POINTER_OBJECT(__CPROVER_dead_object)) ``` ### 自動機理論 (automata theory) `簡介:` * 自動機是一個機器的虛擬模型, 用來計算一個輸入, 並轉移到一連串的狀態。 * 在每個狀態中, 利用 transition function 決定下一個狀態。 * 直到計算過程進到目標狀態, 則接受該輸入, 結束整個計算過程。 * 代表性的自動機: Turing machine `目標:` * 建立一個描述及分析離散系統動態行為的方法。 * 自動機元件包含: inputs, outputs, states `學派:` * Finite-state machine (simplest) * Pushdown automata * Linear-bounded automata * Turing machine (most complex) ### model checking 中局部狀態表示每個主題執行通訊協定的過程，而所有局部狀態構成全域狀態，每個局部狀態的改變由主體的訊息接收、發送來觸發，能否舉出實際案例說明？ ### 是否已編譯 cbmc 並用來分析 C 程式呢？若是，舉出詳細的操作和你的解讀務必詳閱 [CBMC: Bounded Model Checking for C/C++ and Java: A Short Tutorial](http://www.cprover.org/cprover-manual/cbmc.shtml) ### 以 moxiebox 為例，能否使用 cbmc 來找出程式碼實作的缺陷 (或者自己創造) 呢？ ### 在 GitHub 專案中找出使用 model checking 的案例，並且具體說明其作用 (當然要親自實驗) * [PRISM Model Checker](http://www.prismmodelchecker.org/) [Github Link](https://github.com/prismmodelchecker/prism) [PRISM Tutorial](http://www.prismmodelchecker.org/tutorial/die.php) ### 參考資料 * [Understanding Loop Unwinding](http://www.cprover.org/cprover-manual/cbmc-loops.shtml) * [cbmc Github](https://github.com/diffblue/cbmc) * [Stanford University Course - Automata Theory](https://cs.stanford.edu/people/eroberts/courses/soco/projects/2004-05/automata-theory/basics.html) * [自動機理論筆記](http://www.evanlin.com/moocs-coursera-automata-note1/)