Continuation Based C の Hoare Logic を用いた仕様記述と検証
琉球大学大学院 : 並列信頼研究室
+外間 政尊
OS の検証技術としての Hoare Logic の問題点
-
+
-
+
OS やアプリケーションの信頼性は重要な課題
+
+ -
+
信頼性を上げるために仕様の検証が必要
+
+ -
+
検証にはモデル検査や定理証明などが存在する
+
+ -
+
また、仕様検証の手法として Hoare Logic がある
+
+-通常の関数でも実行する前に必要な引数があって何らかの出力がある-
+
- Hoare Logic ではコマンドを実行する上で引数が存在するなどの事前に成り立つ条件があり、コマンド実行後に異なる条件が成り立つ +
+ -
+
Hoare Logic では関数が最低限のコマンドで分割されており記述が困難(変数の代入、コマンド実行の遷移等)
+
+
Hoare Logic をベースにした Gears 単位での検証
-
+
- 当研究室では 処理の単位を CodeGear、データの単位を DataGear としてプログラムを記述する手法を提案 +
- CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む +
- CodeGear は継続を用いて次の CodeGear に接続される +
- 定理証明支援機の Agda 上で Gears 単位を用いた検証を行う +
- 本研究では Gears 単位を用いた Hoare Logic ベースの検証手法を提案する +
Agda
Agda は関数型言語
name : type
+ name = value
+関数には型と定義を与える
+型は : で、 値は = で与える
+仮定なしに使えるのは Set のみ
構成要素としては以下の3種類
-
+
- 関数
+
-
+
- 型は(A : Set かつ B : Set のとき) A → B +
- 値は(x : A かつ y : B) λ x → y +
+ - record +
- data +
Agda の record とその例 ∧
導入は２つのものが同時に存在すること
A B
+------------
+ A ∧ B
+除去は名前を区別する必要がある
A ∧ B A ∧ B
+ --------- pi1 --------- pi2
+ A B
+A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B
+Agda ではこのような同時に存在する型を record で書く
record _∧_ (A B : Set) : Set
+ field
+ pi1 : A
+ pi2 : B
+_∧_ は中間記法、変数が入る位置を _ で示せる
+実際の構築は x : A かつ y : B のとき
createAnd : (A : Set) → (B : Set) → A ∧ B
+createAnd x y = record {pi1 = x ; pi2 = y}
+のように記述する
+C 言語での構造体のようなもの
A や B に論理式が入ると２つのものが同時に成り立つ証明ができる
Agda の data とその例 Sum
導入
+一つでも存在すること
A B
+ ----------- p1 ---------- p2
+ A ∨ B A ∨ B
+除去
+A → C か B → C のとき C
A B
+ : :
+ A ∨ B C C
+ ------------------------
+ C
+A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B
+どちらかが成り立つ型を data で書く\
data _∨_ (A B : Set) : Set where
+ p1 : A → A ∨ B
+ p2 : B → A ∨ B
+のように記述できる
+C 言語での union のようなもの
+p1、 p2 は case 文みたいな感じ
Hoare Logic
Hoare Logic はプログラム検証の手法
+事前条件( P )が成り立つとき、コマンド( C )を実行すると事後条件( Q )が成り立つ
これは { P } C { Q } の形で表され、Hoare Triple と呼ばれる
今回は以下のような while program を検証する
n = 10 となっているが検証では n は任意の自然数
n = 10;
+ i = 0;
+
+ while (n>0)
+ {
+ i++;
+ n--;
+ }
+Agda での Hoare Logic
Hoare Logic のプログラムは Command で構成される
Comm 型は data で記述されたコマンドのデータ構造
実際に実行するには解釈して動かす関数が必要
Commを使って while program を構築する
data Comm : Set where
+ Skip : Comm
+ Abort : Comm
+ PComm : PrimComm → Comm
+ Seq : Comm → Comm → Comm
+ If : Cond → Comm → Comm → Comm
+ While : Cond → Comm → Comm
+Hoare Logic での while program
検証する while program の擬似コード
n = 10;
+ i = 0;
+
+ while (n>0)
+ {
+ i++;
+ n--;
+ }
+コマンドで構成した while program
program : ℕ → Comm
+ program c10 =
+ Seq ( PComm (λ env → record env {varn = c10}))
+ $ 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)} ))
+これは Hoare Logic のコマンドで以下のような構文木を記述している
Seq
+ / \
+ PComm Seq
+ (n=c10) / \
+ PComm While
+ (i=0) |
+ Cond
+ (0<n)
+ |
+ Seq
+ / \
+ PComm PComm
+ (i+1) (n-1)
+Hoare Logic での Command に対応する仕様
Command に対応する証明がある
HTProof は Hoare Triple Proof
{P} Q {C} が Cond → Comm → Cond に対応している
data HTProof : Cond → Comm → Cond → Set where
+すべての Command に対応する Proof を載せると長いので
+必要なものだけ
+PrimRule は 代入のときに成り立ってほしいルール
Axiom は Triple を受け取ってすべての Env は事前の Env が正しければ コマンドを実行した後のEnv も正しくなるという命題
PrimRule : {bPre : Cond} → {pcm : PrimComm} → {bPost : Cond} →
+ (pr : Axiom bPre pcm bPost) →
+ HTProof bPre (PComm pcm) bPost
+WekeningRule は 条件を緩める規則
While コマンドなどで条件が厳しいときに同時に成り立つ異なる条件へ変更必要がある
Tautology は２つの Cond 型 bPre、 bPre’ を受け取り、 bPre が成り立つとき、 bPre’が成り立つという命題
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
+SeqRule は Seqcuence が正しい順番で行われることを保証
cm1、cm2 という2つのCommを受け取ってそれらがcm1、cm2の順で実行される
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
+WhileRule は Comm 型の cm と Cond型の bInv、 bが存在するとき、
+事前に
WhileRule : {cm : Comm} → {bInv : Cond} → {b : Cond} →
+ HTProof (bInv and b) cm bInv →
+ HTProof bInv (While b cm) (bInv and neg b)
+検証をするためにはこの HTProof で program と同様の仕様を構成する必要がある
Hoare Logic での 仕様記述
HTProof で記述した仕様
HTProof が コマンドに対応しているのでほとんど同じ形で書けてる
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
+ program : ℕ → Comm
+ program c10 =
+ Seq ( PComm (λ env → record env {varn = c10}))
+ $ 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)} ))
+proof1 は条件がつながるのに必要な条件を lemma で記述している(lemma は長いので省略)
部分正当性は示せている
全体がつながっているが証明にはなっていない
Hoare Logic での健全性の証明
実際に正しく動作すること(健全性)を証明する必要がある
Satisfies は {P} C {Q} を受け取ってそれらが Comm で正しく成り立つ関係を返す
PrimSoundness は HTProof を受け取って Satisfies が成り立つことを Soundness を用いて実際に証明する
PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
+ HTProof bPre cm bPost -> Satisfies bPre cm bPost
+ PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
+Soundness は HTProof に対応した非常に複雑な証明
HTProof を渡すと Ruleに対応した証明を行う
proofOfProgram では 実際に構築した program と proof1 を使って健全性を証明している
proofOfProgram : (c10 : ℕ) → (input output : Env )
+ → initCond input ≡ true
+ → (SemComm (program c10) input output)
+ → termCond {c10} output ≡ true
+ proofOfProgram c10 input output ic sem =
+ PrimSoundness (proof1 c10) input output ic sem
+Continuation based C について
Continuation based C (CbC) は当研究室で開発してるプログラミング言語
CbC では処理の単位を CodeGear 、データの単位を DataGear とする
CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
Output の DataGear は次の CodeGear の Input として接続される
+
+CodeGear の接続処理などのメタ計算は Meta CodeGear として定義
Meta CodeGear で信頼性の検証を行う
Agda での CodeGear、 DataGear の記述
-
+
- Agda での CodeGear は継続渡しで記述された関数 +
whileTest : {t : Set} → (c10 : Nat)
+ → (Code : Env → t) → t
+ whileTest c10 next = next (record {varn = c10
+ ; vari = 0} )
+-
+
- CodeGear の型は継続先を返す関数 +
- (Code : fa → t) は継続先 +
- 引数として継続先の CodeGear を受け取る +
CbC での Hoare Logic
CodeGear、DataGear を用いた Hoare Logic は図のようになる
+
+
+CodeGear が条件を引数として受け、継続先の CodeGear が次の条件を満たす様になる
下のコードは CodeGear、 DataGear を用いた Hoare Logic ベースの記述例である
whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ) → ((env : Envc )
+ → whileTestStateP s1 env → t) → t
+ whileTestPwP c10 next = next (whileTestP c10 ( λ env → env ))
+ record { pi1 = refl ; pi2 = refl }
+CbC での while program
n = 10;
+ i = 0;
+
+ while (n>0)
+ {
+ i++;
+ n--;
+ }
+CbC での while program
whileTestPCall : (c10 : ℕ ) → Envc
+ whileTestPCall c10 = whileTestP' {_} {_} c10 (λ env → loopP' env (λ env → env))
+-
+
- whileTestP’ が n = c10、 i = 0 の代入、 loopP’ が while loop に対応している +
- CbC での Hoare Logic 上でコマンドは CodeGear そのもの
+
-
+
- CodeGear は Hoare Logic のコマンドより自由な記述 +
+
CbC での Hoare Logic 記述
CbC での Hoare Logic 記述では CodeGear が条件を受け取る
whileTestPwP は代入を行う CodeGear
whileTestPwP : {l : Level} {t : Set l} → (c10 : ℕ)
+ → ((env : Envc ) → (vari env ≡ 0) ∧ (varn env ≡ c10 env) → t) → t
+ whileTestPwP c10 next =
+ next (whileTestP c10 ( λ env → env )) (record { pi1 = refl ; pi2 = refl })
+loopPwP’ は while loop をするための条件を持ち、ループをする CodeGear
n と (n ≡ varn env) を受け取り varn でのパターンマッチをしている
suc n の場合はループを抜けるか判断する CodeGear に継続する
更に継続先で loopPwP’ を呼ぶことで再帰的にループする
loopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc )
+ → (n ≡ varn env) → (vari env + varn env ≡ c10 env) →
+ (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t
+ loopPwP' zero env refl refl exit = exit env refl
+ loopPwP' (suc n) env refl refl exit =
+ whileLoopPwP' (suc n) env refl refl
+ (λ env x y → loopPwP' n env x y exit) exit
+whileLoopPwP’ は while loop を抜けるか判断する CodeGear
loopPwP’から呼ばれている
whileLoopPwP' : {l : Level} {t : Set l} → (n : ℕ) → (env : Envc )
+ → (n ≡ varn env) → (vari env + varn env ≡ c10 env)
+ → (next : (env : Envc ) → (pred n ≡ varn env)
+ → (vari env + varn env ≡ c10 env) → t)
+ → (exit : (env : Envc ) → (vari env ≡ c10 env) → t) → t
+ whileLoopPwP' zero env refl refl _ exit = exit env refl
+ whileLoopPwP' (suc n) env refl refl next _ =
+ next (record env {varn = pred (varn env) ; vari = suc (vari env)})
+ refl (+-suc n (vari env))
+conv は whileTestPwP の事後条件から while loop のための loop invaliant に変更する
conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env)
+ → varn env + vari env ≡ c10 env
+ conv e record { pi1 = refl ; pi2 = refl } = +zero
+whileTestPCallwP’ は先程までの Hoare Logic の記述をつなげたもの
継続先の CodeGear に渡す条件が
whileTestPCallwP' : (c : ℕ ) → Set
+ whileTestPCallwP' c = whileTestPwP {_} {_} c (
+ λ env s → loopPwP' (varn env) env refl (conv env s)
+ ( λ env s → vari env ≡ c10 env ) )
+whileTestPCallwP’ では Hoare Logic の条件が接続できた
Hoare Logic をベースにした CbC での while loop
先程条件を接続した whileTestPCallwP’ を型に入れ、実際に実行してみる
whileCallwP : (c : ℕ) → whileTestPCallwP' c
+ whileCallwP c = whileTestPwP {_} {_} c (λ env s →
+ loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!})
+loopPwP’は任意の値を取ってループを行う CodeGear であった
しかし、引数で受け取った任意の自然数で実行するとループが停まらない
任意の自然数回ループする loopPwP’ が停まることを補助する loopHelper を記述した
loopHelper : (n : ℕ) → (env : Envc ) → (eq : varn env ≡ n)
+ → (varn env + vari env ≡ c10 env)
+ → loopPwP' n env (sym eq) seq (λ env₁ x → (vari env₁ ≡ c10 env₁))
+ loopHelper zero env eq refl rewrite eq = refl
+ loopHelper (suc n) env eq refl rewrite eq = loopHelper n
+ (record { c10 = suc (n + vari env) ; varn = n ; vari = suc (vari env) })
+ refl (+-suc n (vari env))
+loopHelper を用いて記述した実行は実際に停止した
helperCallwP : (c : ℕ) → whileTestPCallwP' c
+ helperCallwP c = whileTestPwP {_} {_} c
+ (λ env s → loopHelper c (record { c10 = c ; varn = c ; vari = zero }) refl +zero)
+CbC での Hoare Logic の健全性
implies という data を用いて健全性の証明を行う
implies の型は A と B の条件を受け取る
このとき proof として A → B が存在すれば A implies B が証明できる
data _implies_ (A B : Set ) : Set (succ Zero) where
+ proof : ( A → B ) → A implies B
+代入を行う CodeGear である whileTestP を実行したとき、
+常に真の命題 ⊤ と代入を終えたときの事後条件である
+(vari env ≡ 0) ∧ (varn env ≡ c10 env)
+を implies に入れた型を記述する
whileTestPSem : (c : ℕ) → whileTestP c
+ ( λ env → ⊤ implies (vari env ≡ 0) ∧ (varn env ≡ c10 env) )
+ whileTestPSem c = proof ( λ _ → record { pi1 = refl ; pi2 = refl } )
+証明では proof に( ⊤ → (vari env ≡ 0) ∧ (varn env ≡ c10 env) )であると記述できればよく
+ここでは λ _ → record { pi1 = refl ; pi2 = refl } がこれに対応する
whileTestPSemSound は output ≡ whileTestP c (λ e → e) を受け取ることで whileTestP の実行が終わった結果、つまり停止した CodeGear の実行結果が事後条件を満たしていることを証明している
whileTestPSemSound : (c : ℕ ) (output : Envc ) →
+ output ≡ whileTestP c (λ e → e)
+ → ⊤ implies ((vari output ≡ 0) ∧ (varn output ≡ c))
+ whileTestPSemSound c output refl = whileTestPSem c
+同様に他の CodeGear に対しても健全性の証明が可能
whileConvPSemSound は制約を緩める conversion の健全性の証明
whileConvPSemSound : {l : Level} → (input : Envc) → ((vari input ≡ 0) ∧ (varn input ≡ c)) implies (varn input + vari input ≡ c10 input)
+whileConvPSemSound input = proof λ x → (conversion input x) where
+ conversion : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
+ conversion e record { pi1 = refl ; pi2 = refl } = +zero
+whileLoopPSemSound は ループを行う CodeGear の 健全性の証明
whileLoopPSemSound : {l : Level} → (input output : Envc )
+ → (varn input + vari input ≡ c10 input)
+ → output ≡ loopPP (varn input) input refl
+ → (varn input + vari input ≡ c10 input) implies (vari output ≡ c10 output)
+whileLoopPSemSound {l} input output pre eq = loopPPSem input output eq pre
+loopPPSem を使って証明を行っている
loopPPSem : (input output : Envc ) → output ≡ loopPP (varn input) input refl
+ → (varn input + vari input ≡ c10 input )
+ → (varn input + vari input ≡ c10 input ) implies (vari output ≡ c10 output)
+loopPPSem input output refl s2p = loopPPSemInduct (varn input) input refl refl s2p
+まとめと今後の課題
-
+
- CodeGear、 DataGear を用いた Hoare Logic ベースの仕様記述を導入した +
- Hoare Logic ベースの検証で停止性を含めて検証できた +
- Hoare Logic ベースの検証の健全性を証明できた
+
-
+
- while Program で使用した CodeGear を使って証明できた +
+ - 今後の課題
+
-
+
- BinaryTree の有限ループに対する証明 +
- Hoare Logic で検証されたコードの CbC 変換 +
- 並列実行での検証 +
+