title: GearsOS の Hoare triple を用いた検証 author: Masataka Hokama profile: 琉球大学 : 並列信頼研究室 lang: Japanese ## 研究背景 - OS やアプリケーションなどの信頼性は重要な課題 - 信頼性を上げるために仕様を検証する必要 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある - 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす - 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?) ## 背景 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む - Gear 間の接続処理はメタ計算として定義 - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証 - 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する

## Gears について - **Gears** は当研究室で提案しているプログラム記述手法 - 計算の単位を **CodeGear** 、データの単位を **DataGear** - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す - Output の DataGear は次の CodeGear の Input として接続される - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義 - メタ計算で信頼性の検証を行う

## CbC について - Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在 - これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの - 環境を継続に含めない - 現在の CbC ではメタ計算での検証 - 将来的には証明も扱えるようにしたいが現段階では未実装 - そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している ## Agda - Agda は定理証明支援系の言語 - 依存型を持つ関数型言語 - 型を明記する必要がある - Agda の文法については次のスライドから軽く説明する ## Agda のデータ型 - データ型は代数的なデータ構造 - **data** キーワードの後に、**名前 : 型**、 where 句 - 次の行以降は**コンストラクタ名 : 型** - 型は**->**または**→**で繋げる - 例えば、型**PrimComm −> Comm**は**PrimComm** を受け取り**Comm**を返す型 - 再帰的な定義も可能 ```AGDA data Comm : Set where Skip : Comm Abort : Comm PComm : PrimComm −> Comm Seq : Comm −> Comm −> Comm If : Cond −> Comm −> Comm −> Comm While : Cond −> Comm −> Comm ``` ## Agda のレコード型 - C 言語での構造体に近い - 複数のデータをまとめる - 関数内で構築できる - 構築時は**レコード名 {フィールド名 = 値}** - 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙 - (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる) ```AGDA record Env : Set where field varn : ℕ vari : ℕ ``` ## Agda の関数 - 関数にも型が必要 - 関数は **関数名 = 値** - 関数ではパターンマッチがかける - **_** は任意の引数 ```AGDA _-_ : ℕ → ℕ → ℕ x - zero = x zero - _ = zero (suc x) - (suc y) = x - y ``` ## Agda での証明 - 関数の型に論理式 - 関数自体にそれを満たす導出 - 完成した関数は証明 - **{}** は暗黙的(推論される) - 下のコードは自然数に 0 を足したとき値が変わらないことの証明 ```AGDA +zero : { y : ℕ } → y + zero ≡ y +zero {zero} = refl +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} ) ``` ## Agda 上での HoareLogic * 現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと それを Agda2 に書き写したものが存在している。 * 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。 ## Agda での HoareLogic の理解 * HoareLogic を用いて次のようなプログラム(while Program)を検証した。 ```C n = 10; i = 0; while (n>0) { i++; n--; } ``` * このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす * n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。 ## HoareLogic * Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する * プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる * 事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。 * コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証する ## Agda 上での HoareLogic(コマンド定義) * Env は while Program の変数である var n, i * **PrimComm** は代入時に使用される * **Cond** は Condition で Env を受け取って Boolean の値を返す ```AGDA record Env : Set where field varn : ℕ vari : ℕ PrimComm : Set PrimComm = Env → Env Cond : Set Cond = (Env → Bool) ``` ## Agda 上での HoareLogic(コマンド定義) * **Comm** は Agda のデータ型で定義した HoareLogic の Command * **Skip** は何も変更しない * **PComm** は変数を代入する * **Seq** は Command を実行して次の Command に移す * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す ```AGDA data Comm : Set where Skip : Comm Abort : Comm PComm : PrimComm -> Comm Seq : Comm -> Comm -> Comm If : Cond -> Comm -> Comm -> Comm While : Cond -> Comm -> Comm ``` ## Agda 上での HoareLogic(実際のプログラムの記述) * Command を使って while Program を記述した。 * **$** は **()** の糖衣で行頭から行末までを ( ) で囲う * 見やすさのため改行しているため 3~7 行はまとまっている * Seq は Comm を2つ取って次の Comm に移行する ```AGDA 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)} )) ``` ## Agda 上での HoareLogicの理解 * 規則は HTProof にまとめられてる * **PrimRule** は **PComm** で行う代入を保証する * 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述 * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数 * SkipRule は PreCondition を変更しないことの保証 * AbortRule は プログラムが停止するときのルール ```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 SkipRule : (b : Cond) -> HTProof b Skip b AbortRule : (bPre : Cond) -> (bPost : Cond) -> HTProof bPre Abort bPost -- 次のスライドに続く ``` ```AGDA Axiom : Cond -> PrimComm -> Cond -> Set Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true ``` ## Agda 上での HoareLogicの理解 * **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の理解 * **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 に 初期状態とコマンドで書かれた **program** と終了状態を渡す * lemma1~5は rule それぞれの証明 * ```AGDA proof1 : HTProof initCond program termCond proof1 = SeqRule {λ e → true} ( PrimRule empty-case ) $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 ) $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 ( WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10} $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 ) $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5 initCond : Cond initCond env = true termCond : {c10 : ℕ} → Cond termCond {c10} env = Equal (vari env) c10 ``` ## 証明の一部 - 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する - impl⇒ ```AGDA lemma1 : {c10 : ℕ} → 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 ∎ ) ``` ## Agda での Gears - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数 - CPS の関数は引数として継続を受け取って継続に計算結果を渡す - **名前 : 引数 -> (Code : fa -> t) -> t** - **t** は継続 - **(Code : fa -> t)** は次の継続先 - DataGear は Agda での CodeGear に使われる引数 ```AGDA _g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t x g- zero next = next x zero g- _ = next zero (suc x) g- (suc y) = next (x g- y) ``` ## Gears をベースにした HoareLogic * 次に Gears をベースにした while Program をみる。 * このプログラムは自然数と継続先を受け取って t を返す ```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 をベースにした証明 * ここでは ```AGDA proofGears : {c10 : ℕ } → 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 ベースで)