# Program Verification ## work# 曾顯恩 --- ## Program ---- ### 大家對寫程式的想像是什麼？ ---- ### 對於 debug 呢？ ---- ### 我們寫的程式會在哪裡運作？ ---- [](https://stackoverflow.com/questions/8021774/how-do-i-add-a-system-call-utility-in-xv6/13205101) ---- [](https://store.google.com/us/category/nest_thermostats) ---- ### 我們寫出來的 bug 會出現在哪裡？ ----  https://zeroday.hitcon.org/vulnerability ----  [Nest Thermostat Glitch Leaves Users in the Cold](https://www.nytimes.com/2016/01/14/fashion/nest-thermostat-glitch-battery-dies-software-freeze.html) ---- - 編譯器 - 交通運輸 - 醫療設備 - ... --- ## 如何達成軟體的正確性 ---- ### 寫測試 ---- [](ada-judge.csie.ntu.edu.tw) ---- [](https://www.csie.ntu.edu.tw/~pjcheng/course/sp2021/) ---- [](https://docs.google.com/presentation/d/1rCR6nvem14BLKR7c8MTH-CKWZ_Z0RkbYWQK93R4N4Tc/edit?usp=sharing) ---- The first moral of the story is that program testing can be used very effectively to show the presence of bugs but never to show their absence. -- <cite>Edsger W. Dijkstra</cite> [On the reliability of programs](https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html) --- ### 不然要怎樣？ 難道有辦法可以保證程式是對的嗎？ ---- #### 什麼是對的？ ---- 制定精確的規格 :arrow_right: 證明程式符合規格 ---- Program verification is a systematic approach to proving the correctness of programs. Correctness means that the programs enjoy certain desirable properties. [Apt, K. R., de Boer, F. S., & Olderog, E.-R. (2009). Verification of Sequential and Concurrent Programs](https://doi.org/10.1007/978-1-84882-745-5) ---- [Wiki - Formal verification](https://en.wikipedia.org/wiki/Formal_verification) --- ## 制定規格 ---- 作業的 spec 算是規格嗎？ 是，但它可以用來證明嗎？ ---- ## 邏輯 ---- ### 語法 有今天 workshop 今天有 workshop ---- $\phi ∶∶= p \mid (¬\phi) \mid (\phi \land \phi) \mid (\phi \lor \phi) \mid (\phi \implies \phi)$ ---- ### 語義 | $p$ | $q$ | $p\implies q$ | |:---:|:---:|:-------------:| | 0 | 0 | 1 | | 0 | 1 | 1 | | 1 | 0 | 0 | | 1 | 1 | 1 | ---- ### 推論規則 modus ponens $\phi$ 成立且 $\phi \implies \psi$ 成立可以推得 $\psi$ 成立 ---- - soundness：推論出來的語義上都是真的 - completeness：語義上是真的都推論的出來 --- ## 模型驗證 [Paul Gastin - Basics of Verification](http://www.lsv.fr/~gastin/Verif/Verif-M1-20-handout.pdf) ---- - 模型 - 狀態 - 行動 - 轉移關係 - 規定 檢驗模型是否符合規定 ---- 優點：驗證過程自動化 缺點：不適合處理狀態數太多的複雜系統（？ ----  ----  ----  --- ### NuSMV [An open source model checker](https://nusmv.fbk.eu) ---- 這個例子來自[王柏堯老師的投影片](https://homepage.iis.sinica.edu.tw/~bywang/courses/comp-logic/chapter-3-2.pdf) ---- #### 安裝 - [下載](https://nusmv.fbk.eu/NuSMV/download/getting_bin-v2.html) - 解壓縮 - 執行 [ferryperson.smv](https://gist.github.com/titusjgr/09816a3366331bfb4d8e2cd0b7e28758) ``` NuSMV-2.6.0-Linux/bin/NuSMV ferryperson.smv ``` ---- #### 工作站上的指令： ``` mkdir nusmv cd nusmv wget https://nusmv.fbk.eu/distrib/NuSMV-2.6.0-linux64.tar.gz tar xf NuSMV-2.6.0-linux64.tar.gz wget https://gist.githubusercontent.com/titusjgr/09816a3366331bfb4d8e2cd0b7e28758/raw/8834e9681b36bdb2b6b41b85977ed8937b6f44b5/ferryperson.smv NuSMV-2.6.0-Linux/bin/NuSMV ferryperson.smv ``` ---- ### Demo 我們想要的：直到所有東東渡到對岸為止，不會發生慘案 我們說的：不可能直到所有東東渡到對岸為止，都不會發生慘案吧？ 然後 NuSMV 就找到一個「不可能直到所有東東渡到對岸為止，都不會發生慘案吧？」的反例 --- ## 演繹驗證 ---- Proof Obligations ---- ### [Proof Assistants](https://en.wikipedia.org/wiki/Proof_assistant) 互動式的證明數學定理 Coq, HOL, Isabelle, Lean, ... ----  ---- [CompCert - Formally verified compiler](https://compcert.org/) used Coq in its verification ---- ### [Automated Theorem Proving](https://en.wikipedia.org/wiki/Automated_theorem_proving) 自動證明 ---- - [z3](https://github.com/Z3Prover/z3): Satisfiability modulo theory - [Gappa](https://gappa.gitlabpages.inria.fr/): 數值運算 ---- Coq、z3、Gappa 都可以作為 [Frama C](https://frama-c.com/) 的後端 用來證明 C 程式的正確性 ---- ### Program Derivation The proper way of doing it is the other way round; given the specification, one designs the correctness proof and, as that design progresses, derives the program to which the proof is applicable, a method known as “designing proof and program hand in hand”. -- <cite>Edsger W. Dijkstra</cite> [Introducing a course on program design and presentation](https://www.cs.utexas.edu/users/EWD/transcriptions/EWD11xx/EWD1157.html) --- ## 相關連結 - [王柏堯老師的計算邏輯簡介](https://homepage.iis.sinica.edu.tw/~bywang/courses/comp-logic/) - [蔡益坤老師的軟體規格與驗證](http://im.ntu.edu.tw/~tsay/dokuwiki/doku.php?id=courses:ssv2021:main) - [NuSMV tutorial](https://nusmv.fbk.eu/NuSMV/tutorial/index.html) - [Software Foundations](https://softwarefoundations.cis.upenn.edu/) - [The complete correctness of sorting](https://www.twanvl.nl/blog/agda/sorting) - [Z3 Playground](https://jfmc.github.io/z3-play/) - [穆信成老師的命令程式設計](https://scmu.github.io/plip/) --- ## 素材來源 - https://www.irasutoya.com - https://hololive.hololivepro.com ---- ###### tags: `Math` `logic` `學術部`