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 は関数型言語

1
2


    name : type
    name = value

関数には型と定義を与える
型は : で、値は = で与える
仮定なしに使えるのは Set のみ

構成要素としては以下の3種類

関数
- 型は(A : Set かつ B : Set のとき) A → B
- 値は(x : A かつ y : B) λ x → y
record
data

# Agda の record とその例 ∧

導入は２つのものが同時に存在すること

1
2
3


   A   B    
------------ 
   A ∧ B    

除去は名前を区別する必要がある

1
2
3


   A ∧ B           A ∧ B 
 --------- pi1   --------- pi2       
     A               B

A ∧ B が成り立っていれば (pi1 A ∧ B) → A、 (pi2 A ∧ B) → B
Agda ではこのような同時に存在する型を record で書く

1
2
3
4


   record _∧_ (A B : Set) : Set
     field
         pi1 : A
         pi2 : B

_∧_ は中間記法、変数が入る位置を _ で示せる
実際の構築は x : A かつ y : B のとき

1
2


createAnd : (A : Set) → (B : Set) → A ∧ B
createAnd x y = record {pi1 = x ; pi2 = y}

のように記述する
C 言語での構造体のようなもの

A や B に論理式が入ると２つのものが同時に成り立つ証明ができる

# Agda の data とその例 Sum

導入
一つでも存在すること

1
2
3


        A               B
  ----------- p1   ---------- p2
     A ∨ B            A ∨ B  

除去
A → C か B → C のとき C

1
2
3
4
5


               A      B
               :      :
      A ∨ B    C      C    
   ------------------------ 
           C                

A ∨ B が成り立っているとき A → A ∨ B、 B → A ∨ B
どちらかが成り立つ型を data で書く\

1
2
3


    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 は任意の自然数

1
2
3
4
5
6
7
8


    n = 10;
    i = 0;

    while (n>0)
    {
      i++;
      n--;
    }

# Agda での Hoare Logic

Hoare Logic のプログラムは Command で構成される

Comm 型は data で記述されたコマンドのデータ構造

実際に実行するには解釈して動かす関数が必要

Commを使って while program を構築する

1
2
3
4
5
6
7


    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 の擬似コード

1
2
3
4
5
6
7
8


    n = 10;
    i = 0;

    while (n>0)
    {
      i++;
      n--;
    }

コマンドで構成した while program

1
2
3
4
5
6
7


    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 のコマンドで以下のような構文木を記述している

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13


        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 に対応している

1

    data HTProof : Cond → Comm → Cond → Set where

すべての Command に対応する Proof を載せると長いので必要なものだけ

PrimRule は代入のときに成り立ってほしいルール

Axiom は Triple を受け取ってすべての Env は事前の Env が正しければコマンドを実行した後のEnv も正しくなるという命題

1
2
3


      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’が成り立つという命題

1
2
3
4
5
6


      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の順で実行される

1
2
3
4
5


      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が存在するとき、事前に

1
2
3


      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 がコマンドに対応しているのでほとんど同じ形で書けてる

1
2
3
4
5
6
7
8


    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

1
2
3
4
5
6
7


    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 を用いて実際に証明する

1
2
3


    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 を使って健全性を証明している

1
2
3
4
5
6


    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 は継続渡しで記述された関数

1
2
3
4


     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 ベースの記述例である

1
2
3
4


    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 } 

# CbC での while program

1
2
3
4
5
6
7
8


    n = 10;
    i = 0;

    while (n>0)
    {
      i++;
      n--;
    }

CbC での while program

1
2


    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

1
2
3
4


    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’ を呼ぶことで再帰的にループする

1
2
3
4
5
6
7


    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’から呼ばれている

1
2
3
4
5
6
7
8
9


    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 に変更する

1
2
3


    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 に渡す条件が

1
2
3
4


    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’ を型に入れ、実際に実行してみる

1
2
3


    whileCallwP : (c : ℕ) → whileTestPCallwP' c
    whileCallwP c = whileTestPwP {_} {_} c (λ env s →
            loopPwP' (c10 env) env (sym (pi2 s)) (conv env s) {!!})

loopPwP’は任意の値を取ってループを行う CodeGear であった

しかし、引数で受け取った任意の自然数で実行するとループが停まらない

任意の自然数回ループする loopPwP’ が停まることを補助する loopHelper を記述した

1
2
3
4
5
6
7


     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 を用いて記述した実行は実際に停止した

1
2
3


    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 が証明できる

1
2


    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 に入れた型を記述する

1
2
3


    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 の実行結果が事後条件を満たしていることを証明している

1
2
3
4


    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 の健全性の証明

1
2
3
4


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 の健全性の証明

1
2
3
4
5


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 を使って証明を行っている

1
2
3
4


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 変換
- 並列実行での検証

# Comm の実行

Comm で記述した program を解釈して実行する関数 interpet を記述した

interpret は停止性を考慮していないため{-# TERMINATING #-}タグを付けてエラーを回避している

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


{-# TERMINATING #-}
interpret : Env → Comm → Env
interpret env Skip = env
interpret env Abort = env
interpret env (PComm x) = x env
interpret env (Seq comm comm1) = interpret (interpret env comm) comm1
interpret env (If x then else) with x env
... | true = interpret env then
... | false = interpret env else
interpret env (While x comm) with x env
... | true = interpret (interpret env comm) (While x comm)
... | false = env

実行する際は test1 のように interpret に Env と Comm を渡してやる

1
2


test1 : Env
test1 =  interpret ( record { vari = 0  ; varn = 0 } ) (program 10)

実行結果は以下のようになる

1

record { varn = 0 ; vari = 10 }

# Hoare Logic をベースにした Gears 単位での検証