Mercurial > hg > Papers > 2019 > ryokka-sigss
view slide/slide.md @ 12:e8fe28afe61e
fix slide
author | ryokka |
---|---|
date | Tue, 15 Jan 2019 15:56:33 +0900 |
parents | 17b7605a5deb |
children | fde9ee0cc8ae |
line wrap: on
line source
title: GearsOS の Hoare Logic を用いた検証 author: Masataka Hokama profile: 琉球大学 : 並列信頼研究室 lang: Japanese <!-- 発表20分、質疑応答5分 --> ## 研究背景 - OS やアプリケーションなどの信頼性は重要な課題 - 信頼性を上げるために仕様を検証する必要 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある - 事前条件(Pre Condition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(Post Condition)を満たす - 既存の言語ではあまり利用されていない ## 背景 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む <!-- - Gear 間の接続処理はメタ計算として定義 --> <!-- - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 --> - この単位を用いて信頼性の高い OS として GearsOS を開発している - 本発表では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する ## Gears について - **Gears** は当研究室で提案しているプログラム記述手法 - 計算の単位を **CodeGear** 、データの単位を **DataGear** - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す - Output の DataGear は次の CodeGear の Input として接続される <!-- [fig1](file://./fig/cgdg.pdf) --> - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義 - メタ計算で信頼性の検証を行う <p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt="" width="75%" height="75%"/></p> <!-- ![cgdg](./pic/codeGear_dataGear.pdf){} --> <!-- <p style="text-align:center;"><img src="./pic/cgdg.svg" alt="" width="30%" height="30%"/></p> --> ## CbC について - Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在 - これは C からループ制御構造と関数呼び出しを取り除き、代わりに継続を導入したもの - 現在の CbC でもメタ計算での検証は可能 - 将来的には証明も扱えるようにしたいが現段階では未実装 - そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している ## Agda とは - Agda は定理証明支援系の言語 - 依存型を持つ関数型言語 - 型を明記する必要がある - Agda の文法については次のスライドから軽く説明する ## Agda のデータ型 - データ型は代数的なデータ構造 - **data** キーワードの後に、**名前 : 型** - 次の行以降は**コンストラクタ名 : 型** - 型は**->**または**→**で繋げる - 例えば、suc の型**Nat → Nat*は**Nat** を受け取り**Nat**を返す型 - これにより 3 を suc (suc (suc zero)) のように表せる ```AGDA data Nat : Set where zero : Nat suc : Nat → Nat ``` <!-- - where は宣言した部分に束縛する --> ## Agda のレコード型 - C 言語での構造体に近い - 複数のデータをまとめる - 関数内で構築できる - 構築時は**record レコード名 {フィールド名 = 値}** - 複数ある場合は **record Env {varn = 1 ; varn = 2}**のように **;** を使って列挙 ```AGDA record Env : Set where field varn : Nat vari : Nat ``` ## Agda の関数 - 関数にも型が必要(1行目) - 引き算はは自然数を2つ取って結果の自然数を返す - **_** は任意の値、名前で使うと受け取った引数が順番に入る - 関数本体は **関数名 = 値** - 関数ではパターンマッチがかける - ここでは関数名に **_** を使っているため**Nat**の定義にから zero かそれ以外でパターンマッチ ```AGDA _-_ : Nat → Nat → Nat x - zero = x zero - _ = zero (suc x) - (suc y) = x - y ``` ## Agda での証明 - 関数の型に証明すべき論理式 - 関数自体にそれを満たす導出 - 完成した関数は証明 - **{}** は暗黙的(推論される) - 下のコードは Bool型の x と true の and を取ったものは x と等しいことの証明 - **refl** は **x == x** の左右の項が等しいことの証明 ```AGDA ∧true : { x : Bool } → x ∧ true ≡ x ∧true {x} with x ∧true {x} | false = refl ∧true {x} | true = refl ``` ## Agda 上での HoareLogic * Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと それを Agda2 に書き写したものが存在している。 * 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて Agda2上で HoareLogic を構築する ## HoareLogic とは * Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する * プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる * 事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。 * コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証できる ## HoareLogic の理解 - HoareLogic 例として疑似コードを用意した - このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす - n==0 のとき停止するため、終了時の変数の結果は i==10、n==0 になるはずである。 - 次のスライドから Agda 上 HoareLogic を実装し、その上でこの whileProgram の検証を行う ```C n = 10; i = 0; while (n>0) { i++; n--; } ``` ## Agda 上での HoareLogic(条件、変数の定義) - **Env** は while Program で必要な変数をまとめたもの - varn、vari はそれぞれ変数 n、 i - **Cond** は Pre、Post の Condition で Env を受け取って Bool 値(true か false)を返す ```AGDA record Env : Set where field varn : Nat vari : Nat Cond : Set Cond = (Env → Bool) ``` ## Agda 上での HoareLogic(コマンド定義) * **Comm** は Agda のデータ型で定義した HoareLogic のコマンド * **PComm** は変数を代入のコマンド * **Seq** はコマンドの推移、 Command を実行して次の Command に移す * **If** は条件分岐のコマンド * **while** は繰り返しのコマンド * 他にも何もしないコマンドやコマンドの停止などのコマンドもある - **PrimComm** は Env を受け取って Env を返す定義 ```AGDA data Comm : Set where PComm : PrimComm → Comm Seq : Comm → Comm → Comm If : Cond → Comm → Comm → Comm While : Cond → Comm → Comm PrimComm : Set PrimComm = Env → Env ``` ## Agda 上での HoareLogic(実際のプログラムの記述) * 先程定義したコマンドを使って while Program を記述した - 任意の自然数を引数に取る形になっているが**c10 == 10**ということにする * **$** は **()** の糖衣で行頭から行末までを ( ) で囲う * 見やすさのため改行しているが 3~7 行は1行 ```AGDA program : ℕ → Comm program c10 = Seq ( PComm (λ env → record env {varn = c10})) -- n = 10; $ Seq ( PComm (λ env → record env {vari = 0})) -- i = 0; $ While (λ env → lt zero (varn env ) ) -- while (n>0) { (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -- i++; $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -- n--; ``` ## Agda 上での HoareLogic(コマンドの保証)1/3 * 保証の規則は HTProof にまとめられてる * **PrimRule** は **PComm** で行う代入を保証する * 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述 * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す ```AGDA data HTProof : Cond → Comm → Cond → Set where PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} → (pr : Axiom bPre pcm bPost) → HTProof bPre (PComm pcm) bPost -- 次のスライドに続く ``` ```AGDA Axiom : Cond → PrimComm → Cond → Set Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true ``` ## Agda 上での HoareLogic(コマンド保証)2/3 * **SeqRule** は Command を推移させる Seq の保証 * **IfRule** は If の Command が正しく動くことを保証 ```AGDA -- HTProof の続き SeqRule : {bPre : Cond} → {cm1 : Comm} → {bMid : Cond} → {cm2 : Comm} → {bPost : Cond} → HTProof bPre cm1 bMid → HTProof bMid cm2 bPost → HTProof bPre (Seq cm1 cm2) bPost IfRule : {cmThen : Comm} → {cmElse : Comm} → {bPre : Cond} → {bPost : Cond} → {b : Cond} → HTProof (bPre /\ b) cmThen bPost → HTProof (bPre /\ neg b) cmElse bPost → HTProof bPre (If b cmThen cmElse) bPost ``` ## Agda 上での HoareLogic(コマンド保証)3/3 * **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換 * Tautology は Condition と不変条件が等しく成り立つ * **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す ```AGDA -- HTProof の続き WeakeningRule : {bPre : Cond} → {bPre' : Cond} → {cm : Comm} → {bPost' : Cond} → {bPost : Cond} → Tautology bPre bPre' → HTProof bPre' cm bPost' → Tautology bPost' bPost → HTProof bPre cm bPost WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} → HTProof (bInv /\ b) cm bInv → HTProof bInv (While b cm) (bInv /\ neg b) ``` ```AGDA Tautology : Cond → Cond → Set Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true ``` ## Agda 上での HoareLogic(証明) - **proof1** は while Program の証明 - HTProof に 初期状態と先程コマンドで記述した whileProgram である **program** と終了状態を渡す - Condititon は initCond や termCond のようにそれぞれ定義する必要がある - program に近い形で証明を記述できる ```AGDA proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10}) proof1 c10 = SeqRule {λ e → true} ( PrimRule (init-case {c10} )) $ SeqRule {λ e → Equal (varn e) c10} ( PrimRule lemma1 ) $ WeakeningRule {λ e → (Equal (varn e) c10) ∧ (Equal (vari e) 0)} lemma2 ( WhileRule {_} {λ e → Equal ((varn e) + (vari e)) c10} $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 initCond : Cond initCond env = true termCond : {c10 : Nat} → Cond termCond {c10} env = Equal (vari env) c10 ``` <!-- * lemma1~5は rule それぞれの証明 --> <!-- program : Comm --> <!-- program = --> <!-- Seq ( PComm (λ env → record env {varn = 10})) --> <!-- $ Seq ( PComm (λ env → record env {vari = 0})) --> <!-- $ While (λ env → lt zero (varn env ) ) --> <!-- (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) --> <!-- $ PComm (λ env → record env {varn = ((varn env) - 1)} )) --> ## 証明の一部(lemma1) - PComm の証明である lemma1 だけ解説 - lemma1 は n に 10 を代入したあと、 i に 0 を代入するところ - 証明することは**事前条件の n ≡ 10 が成り立つか** - PreCondition が成り立つとき、Command を実行するとPostConditionが成り立つ - Axiom は x ⇒ y ≡ true が成り立てば良かった - **_⇒_** は事後条件が成り立つかどうか - impl⇒ は x ≡ true → y ≡ true の関数(Command)を受け取って x ⇒ y ≡ true を返す関数 - **≡-Reasoning** は Agda での等式変形 ```AGDA lemma1 : {c10 : Nat} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10}) lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in begin (Equal (varn env) c10 ) ∧ true ≡⟨ ∧true ⟩ Equal (varn env) c10 ≡⟨ cond ⟩ true ∎ ) stmt1Cond : {c10 : ℕ} → Cond stmt1Cond {c10} env = Equal (varn env) c10 stmt2Cond : {c10 : ℕ} → Cond stmt2Cond {c10} env = (Equal (varn env) c10) ∧ (Equal (vari env) 0) ``` <!-- lemma2 : {c10 : Nat} → Tautology stmt2Cond whileInv --> <!-- lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' --> <!-- lemma4 : {c10 : Nat} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv --> <!-- lemma5 : {c10 : Nat} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond --> ## Agda での Gears - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 - CPS の関数は引数として継続を受け取って継続に計算結果を渡す - **名前 : 引数 → (Code : fa → t) → t** - **t** は継続 - **(Code : fa → t)** は次の継続先 - DataGear は Agda での CodeGear に使われる引数 ```AGDA _-_ : {t : Set} → Nat → Nat → (Code : Nat → t) → t x - zero = (λ next → next x) zero - _ = (λ next → next zero) (suc x) - (suc y) = (x - y) ``` ## Gears をベースにした HoareLogic と証明(全体) - Gears をベースにした while Program - これは証明でもある - whileループを任意の回数にするため**c10**は引数 - whileTest' の継続に conversion1、その継続に whileLoop' が来て最後の継続に vari が c10 と等しい ```AGDA proofGears : {c10 : Nat } → Set proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` ## Gears と HoareLogic をベースにした証明(whileTest) - ここは代入する Command - 最初の Command なので PreCondition がない - もとの whileProgram では PComm を2回していたがまとめた - proof2は Post Condition が成り立つことの証明 - **_/\\_** は pi1 と pi2 のフィールドをもつレコード型 - 2つのものを引数に取り、両方が同時に成り立つことを示す - Gears での PostCondition は **引数 → (Code : fa → PostCondition → t) → t** ```AGDA whileTest' : {l : Level} {t : Set l} → {c10 : Nat } → (Code : (env : Env) → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t whileTest' {_} {_} {c10} next = next env proof2 where env : Env env = record {vari = 0 ; varn = c10} proof2 : ((vari env) ≡ 0) /\ ((varn env) ≡ c10) <-- PostCondition proof2 = record {pi1 = refl ; pi2 = refl} ``` ## Gears と HoareLogic をベースにした証明(conversion) - conversion は Condition から LoopInvaliant への変換を行う CodeGear - proof4 は LoopInvaliant の証明 - Gears での HoareLogic の完全な記述は **引数 → PreCondition → (Code : fa → PostCondition → t) → t** ```AGDA conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 : Nat } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t conversion1 env {c10} p1 next = next env proof4 where proof4 : varn env + vari env ≡ c10 proof4 = let open ≡-Reasoning in begin varn env + vari env ≡⟨ cong ( λ n → n + vari env ) (pi2 p1 ) ⟩ c10 + vari env ≡⟨ cong ( λ n → c10 + n ) (pi1 p1 ) ⟩ c10 + 0 ≡⟨ +-sym {c10} {0} ⟩ c10 ∎ ``` ## Gears と HoareLogic をベースにした証明(whileLoop) - whileLoop は loopInvaliant が true の間 WhileLoop を回し続けるCodeGear - この CodeGear は Agda がループが終わることが証明できてないため **{-# TERMINATING #-}** で明示 - false になると次の CodeGear へ ```AGDA {-# TERMINATING #-} whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t whileLoop env next with lt 0 (varn env) whileLoop env next | false = next env whileLoop env next | true = whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next ``` ## Gears と HoareLogic をベースにした証明(全体) - 最終状態で返ってくる i の値は c10 と一致する - これにより証明が可能 ```AGDA proofGears : {c10 : Nat } → Set proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 )))) ``` ## まとめと今後の課題 - HoareLogic の while を使った例題を作成、証明を行った - Gears を用いた HoareLogic ベースの検証方法を導入した - 証明が引数として渡される記述のため証明とプログラムを一体化できた - 今後の課題 - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)