|
10
|
1 title: GearsOS の Hoare triple を用いた検証
|
|
|
2 author: Masataka Hokama
|
|
|
3 profile: 琉球大学 : 並列信頼研究室
|
|
|
4 lang: Japanese
|
|
|
5
|
|
|
6 <!-- 発表20分、質疑応答5分 -->
|
|
|
7
|
|
11
|
8 ## 研究背景
|
|
|
9 - OS やアプリケーションなどの信頼性は重要な課題
|
|
|
10 - 信頼性を上げるために仕様を検証する必要
|
|
|
11 - 仕様検証の手法として Floyd-Hoare Logic (以下 HoareLogic) がある
|
|
|
12 - 事前条件(PreCondition)が成り立つとき、関数(Command)を実行、それが停止したとき、事後条件(PostCondition)を満たす
|
|
|
13 - 既存の言語ではあまり利用されていない(python の pyrefine ってコードチェッカーくらい...?)
|
|
10
|
14
|
|
11
|
15 ## 背景
|
|
|
16 - 当研究室では 処理の単位を **CodeGear**、データの単位を **DataGear** としてプログラムを記述する手法を提案
|
|
|
17 - CodeGear は Input DataGear を受け取り、処理を行って Output DataGear に書き込む
|
|
|
18 - Gear 間の接続処理はメタ計算として定義
|
|
|
19 - メタ計算部分に検証を埋め込むことで通常処理に手を加えずに検証
|
|
|
20 - 本研究では Gears OS の信頼性を高めるため、 Gears の単位を用いた HoareLogic ベースの検証手法を提案する
|
|
10
|
21
|
|
11
|
22 <p style="text-align:center;"><img src="./pic/cgdg-small.svg" alt="" width="75%" height="75%"/></p>
|
|
10
|
23
|
|
|
24 ## Gears について
|
|
|
25 - **Gears** は当研究室で提案しているプログラム記述手法
|
|
|
26 - 計算の単位を **CodeGear** 、データの単位を **DataGear**
|
|
|
27 - CodeGear は引数として Input の DataGear を受け取り、 Output の DataGear を返す
|
|
|
28 - Output の DataGear は次の CodeGear の Input として接続される
|
|
|
29 <!-- [fig1](file://./fig/cgdg.pdf) -->
|
|
|
30 - CodeGear の接続処理は通常の計算とは異なるメタ計算として定義
|
|
|
31 - メタ計算で信頼性の検証を行う
|
|
|
32
|
|
11
|
33 <!-- {} -->
|
|
|
34 <p style="text-align:center;"><img src="./pic/cgdg.svg" alt="" width="30%" height="30%"/></p>
|
|
|
35
|
|
10
|
36 ## CbC について
|
|
11
|
37 - Gears の単位でプログラミングできる言語として当研究室で開発している **CbC** (Continuation based C) が存在
|
|
|
38 - これは C からループ制御構造と関数呼び出しを取り除き継続を導入したもの
|
|
|
39 - 環境を継続に含めない
|
|
|
40 - 現在の CbC ではメタ計算での検証
|
|
10
|
41 - 将来的には証明も扱えるようにしたいが現段階では未実装
|
|
11
|
42 - そのため Gears の単位を定理証明支援系の言語である **Agda** で記述し、 Agda で証明している
|
|
10
|
43
|
|
|
44 ## Agda
|
|
|
45 - Agda は定理証明支援系の言語
|
|
|
46 - 依存型を持つ関数型言語
|
|
|
47 - 型を明記する必要がある
|
|
|
48 - Agda の文法については次のスライドから軽く説明する
|
|
|
49
|
|
|
50 ## Agda のデータ型
|
|
|
51 - データ型は代数的なデータ構造
|
|
|
52 - **data** キーワードの後に、**名前 : 型**、 where 句
|
|
|
53 - 次の行以降は**コンストラクタ名 : 型**
|
|
11
|
54 - 型は**->**または**→**で繋げる
|
|
|
55 - 例えば、型**PrimComm −> Comm**は**PrimComm** を受け取り**Comm**を返す型
|
|
10
|
56 - 再帰的な定義も可能
|
|
|
57 ```AGDA
|
|
11
|
58 data Comm : Set where
|
|
|
59 Skip : Comm
|
|
|
60 Abort : Comm
|
|
|
61 PComm : PrimComm −> Comm
|
|
|
62 Seq : Comm −> Comm −> Comm
|
|
|
63 If : Cond −> Comm −> Comm −> Comm
|
|
|
64 While : Cond −> Comm −> Comm
|
|
10
|
65 ```
|
|
|
66
|
|
|
67 <!-- - where は宣言した部分に束縛する -->
|
|
|
68
|
|
|
69 ## Agda のレコード型
|
|
|
70 - C 言語での構造体に近い
|
|
11
|
71 - 複数のデータをまとめる
|
|
10
|
72 - 関数内で構築できる
|
|
|
73 - 構築時は**レコード名 {フィールド名 = 値}**
|
|
|
74 - 複数ある場合は **{フィールド1 = 1 ; フィールド2 = 2}**のように **;** を使って列挙
|
|
11
|
75 - (varn,vari の型 **ℕ** は Agda 上の 自然数、 データ型で zero : ℕ と succ : ℕ -> ℕ で定義されてる)
|
|
10
|
76 ```AGDA
|
|
11
|
77 record Env : Set where
|
|
|
78 field
|
|
|
79 varn : ℕ
|
|
|
80 vari : ℕ
|
|
10
|
81 ```
|
|
|
82
|
|
|
83 ## Agda の関数
|
|
|
84 - 関数にも型が必要
|
|
|
85 - 関数は **関数名 = 値**
|
|
|
86 - 関数ではパターンマッチがかける
|
|
|
87 - **_** は任意の引数
|
|
|
88 ```AGDA
|
|
11
|
89 _-_ : ℕ → ℕ → ℕ
|
|
|
90 x - zero = x
|
|
|
91 zero - _ = zero
|
|
|
92 (suc x) - (suc y) = x - y
|
|
10
|
93 ```
|
|
|
94
|
|
|
95 ## Agda での証明
|
|
|
96 - 関数の型に論理式
|
|
|
97 - 関数自体にそれを満たす導出
|
|
|
98 - 完成した関数は証明
|
|
|
99 - **{}** は暗黙的(推論される)
|
|
|
100 - 下のコードは自然数に 0 を足したとき値が変わらないことの証明
|
|
|
101 ```AGDA
|
|
11
|
102 +zero : { y : ℕ } → y + zero ≡ y
|
|
|
103 +zero {zero} = refl
|
|
|
104 +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
|
|
10
|
105 ```
|
|
|
106
|
|
|
107 ## Agda 上での HoareLogic
|
|
|
108 * 現在 Agda での HoareLogic は初期のAgda の実装である Agda1(現在のものはAgda2)で実装されたものと
|
|
|
109 それを Agda2 に書き写したものが存在している。
|
|
|
110 * 今回はAgda2側の HoareLogic で使うコマンド定義の一部と、コマンドの証明に使うルールを借りて説明を行う。
|
|
|
111
|
|
|
112
|
|
|
113 ## Agda での HoareLogic の理解
|
|
|
114 * HoareLogic を用いて次のようなプログラム(while Program)を検証した。
|
|
|
115 ```C
|
|
11
|
116 n = 10;
|
|
|
117 i = 0;
|
|
10
|
118
|
|
11
|
119 while (n>0)
|
|
|
120 {
|
|
|
121 i++;
|
|
|
122 n--;
|
|
|
123 }
|
|
10
|
124 ```
|
|
|
125 * このプログラムは変数iとnをもち、 n>0 の間nの値を減らし、i の値を増やす
|
|
|
126 * n==0のとき停止するため、終了時の変数の結果はi==10、n==0 になるはずである。
|
|
|
127
|
|
|
128 ## HoareLogic
|
|
|
129 * Floyd-Hoare Logic (以下HoareLogic)は部分的な正当性を検証する
|
|
|
130 * プログラムは事前条件(Pre Condition)、事後条件(Post Condition)を持ち、条件がコマンドで更新され、事後条件になる
|
|
|
131 * 事前、事後条件には変数や論理式、コマンドには代入や、繰り返し、条件分岐などがある。
|
|
|
132 * コマンドが正しく成り立つことを保証することで、このコマンドを用いて記述されたプログラムの部分的な正しさを検証する
|
|
|
133
|
|
|
134
|
|
|
135 ## Agda 上での HoareLogic(コマンド定義)
|
|
|
136 * Env は while Program の変数である var n, i
|
|
|
137 * **PrimComm** は代入時に使用される
|
|
|
138 * **Cond** は Condition で Env を受け取って Boolean の値を返す
|
|
11
|
139 ```AGDA
|
|
|
140 record Env : Set where
|
|
|
141 field
|
|
|
142 varn : ℕ
|
|
|
143 vari : ℕ
|
|
10
|
144
|
|
11
|
145 PrimComm : Set
|
|
|
146 PrimComm = Env → Env
|
|
10
|
147
|
|
11
|
148 Cond : Set
|
|
|
149 Cond = (Env → Bool)
|
|
10
|
150 ```
|
|
|
151
|
|
|
152 ## Agda 上での HoareLogic(コマンド定義)
|
|
|
153 * **Comm** は Agda のデータ型で定義した HoareLogic の Command
|
|
|
154 * **Skip** は何も変更しない
|
|
|
155 * **PComm** は変数を代入する
|
|
11
|
156 * **Seq** は Command を実行して次の Command に移す
|
|
10
|
157 * **If** は Cond と2つの Comm を受け取り Cond の状態により実行する Comm を変える
|
|
|
158 * **while** は Cond と Comm を受け取り Cond の中身が真である間 Comm を繰り返す
|
|
|
159 ```AGDA
|
|
11
|
160 data Comm : Set where
|
|
|
161 Skip : Comm
|
|
|
162 Abort : Comm
|
|
|
163 PComm : PrimComm -> Comm
|
|
|
164 Seq : Comm -> Comm -> Comm
|
|
|
165 If : Cond -> Comm -> Comm -> Comm
|
|
|
166 While : Cond -> Comm -> Comm
|
|
10
|
167 ```
|
|
|
168
|
|
|
169 ## Agda 上での HoareLogic(実際のプログラムの記述)
|
|
11
|
170 * Command を使って while Program を記述した。
|
|
|
171 * **$** は **()** の糖衣で行頭から行末までを ( ) で囲う
|
|
|
172 * 見やすさのため改行しているため 3~7 行はまとまっている
|
|
|
173 * Seq は Comm を2つ取って次の Comm に移行する
|
|
10
|
174 ```AGDA
|
|
11
|
175 program : Comm
|
|
|
176 program =
|
|
|
177 Seq ( PComm (λ env → record env {varn = 10}))
|
|
|
178 $ Seq ( PComm (λ env → record env {vari = 0}))
|
|
|
179 $ While (λ env → lt zero (varn env ) )
|
|
|
180 (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
|
|
|
181 $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
|
|
10
|
182 ```
|
|
|
183
|
|
|
184
|
|
|
185 ## Agda 上での HoareLogicの理解
|
|
11
|
186 * 規則は HTProof にまとめられてる
|
|
|
187 * **PrimRule** は **PComm** で行う代入を保証する
|
|
|
188 * 3行目の pr の型 Axiom は PreCondition に PrimComm が適用されると PostCondition になることの記述
|
|
|
189 * **_⇒_** は pre, post の Condition をとって post の Condition が成り立つときに True を返す関数
|
|
|
190 * SkipRule は PreCondition を変更しないことの保証
|
|
|
191 * AbortRule は プログラムが停止するときのルール
|
|
|
192 ```AGDA
|
|
|
193 data HTProof : Cond -> Comm -> Cond -> Set where
|
|
|
194 PrimRule : {bPre : Cond} -> {pcm : PrimComm} -> {bPost : Cond} ->
|
|
|
195 (pr : Axiom bPre pcm bPost) ->
|
|
|
196 HTProof bPre (PComm pcm) bPost
|
|
|
197 SkipRule : (b : Cond) -> HTProof b Skip b
|
|
|
198 AbortRule : (bPre : Cond) -> (bPost : Cond) ->
|
|
|
199 HTProof bPre Abort bPost
|
|
|
200 -- 次のスライドに続く
|
|
|
201 ```
|
|
|
202 ```AGDA
|
|
|
203 Axiom : Cond -> PrimComm -> Cond -> Set
|
|
|
204 Axiom pre comm post = ∀ (env : Env) → (pre env) ⇒ ( post (comm env)) ≡ true
|
|
|
205 ```
|
|
10
|
206
|
|
11
|
207 ## Agda 上での HoareLogicの理解
|
|
|
208 * **SeqRule** は Command を推移させる Seq の保証
|
|
|
209 * **IfRule** は If の Command が正しく動くことを保証
|
|
|
210 ```AGDA
|
|
|
211 -- HTProof の続き
|
|
|
212 SeqRule : {bPre : Cond} -> {cm1 : Comm} -> {bMid : Cond} ->
|
|
|
213 {cm2 : Comm} -> {bPost : Cond} ->
|
|
|
214 HTProof bPre cm1 bMid ->
|
|
|
215 HTProof bMid cm2 bPost ->
|
|
|
216 HTProof bPre (Seq cm1 cm2) bPost
|
|
|
217 IfRule : {cmThen : Comm} -> {cmElse : Comm} ->
|
|
|
218 {bPre : Cond} -> {bPost : Cond} ->
|
|
|
219 {b : Cond} ->
|
|
|
220 HTProof (bPre /\ b) cmThen bPost ->
|
|
|
221 HTProof (bPre /\ neg b) cmElse bPost ->
|
|
|
222 HTProof bPre (If b cmThen cmElse) bPost
|
|
|
223 ```
|
|
10
|
224
|
|
11
|
225 ## Agda 上での HoareLogicの理解
|
|
|
226 * **WeakeningRule** は通常の Condition からループ不変条件(Loop Invaliant)に変換
|
|
|
227 * Tautology は Condition と不変条件が等しく成り立つ
|
|
|
228 * **WhileRule** はループ不変条件が成り立つ間 Comm を繰り返す
|
|
10
|
229 ```AGDA
|
|
11
|
230 -- HTProof の続き
|
|
|
231 WeakeningRule : {bPre : Cond} -> {bPre' : Cond} -> {cm : Comm} ->
|
|
|
232 {bPost' : Cond} -> {bPost : Cond} ->
|
|
|
233 Tautology bPre bPre' ->
|
|
|
234 HTProof bPre' cm bPost' ->
|
|
|
235 Tautology bPost' bPost ->
|
|
|
236 HTProof bPre cm bPost
|
|
|
237 WhileRule : {cm : Comm} -> {bInv : Cond} -> {b : Cond} ->
|
|
|
238 HTProof (bInv /\ b) cm bInv ->
|
|
|
239 HTProof bInv (While b cm) (bInv /\ neg b)
|
|
|
240 ```
|
|
|
241 ```AGDA
|
|
|
242 Tautology : Cond -> Cond -> Set
|
|
|
243 Tautology pre post = ∀ (env : Env) → (pre env) ⇒ (post env) ≡ true
|
|
|
244 ```
|
|
|
245
|
|
|
246 ## Agda 上での HoareLogic(証明)
|
|
|
247 * **proof1** は while Program の証明
|
|
|
248 * HTProof に 初期状態とコマンドで書かれた **program** と終了状態を渡す
|
|
|
249 * lemma1~5は rule それぞれの証明
|
|
|
250 *
|
|
|
251 ```AGDA
|
|
|
252 proof1 : HTProof initCond program termCond
|
|
|
253 proof1 =
|
|
|
254 SeqRule {λ e → true} ( PrimRule empty-case )
|
|
|
255 $ SeqRule {λ e → Equal (varn e) 10} ( PrimRule lemma1 )
|
|
|
256 $ WeakeningRule {λ e → (Equal (varn e) 10) ∧ (Equal (vari e) 0)} lemma2 (
|
|
|
257 WhileRule {_} {λ e → Equal ((varn e) + (vari e)) 10}
|
|
|
258 $ SeqRule (PrimRule {λ e → whileInv e ∧ lt zero (varn e) } lemma3 )
|
|
|
259 $ PrimRule {whileInv'} {_} {whileInv} lemma4 ) lemma5
|
|
|
260
|
|
|
261 initCond : Cond
|
|
|
262 initCond env = true
|
|
|
263
|
|
|
264 termCond : {c10 : ℕ} → Cond
|
|
|
265 termCond {c10} env = Equal (vari env) c10
|
|
|
266 ```
|
|
|
267
|
|
|
268 <!-- program : Comm -->
|
|
|
269 <!-- program = -->
|
|
|
270 <!-- Seq ( PComm (λ env → record env {varn = 10})) -->
|
|
|
271 <!-- $ Seq ( PComm (λ env → record env {vari = 0})) -->
|
|
|
272 <!-- $ While (λ env → lt zero (varn env ) ) -->
|
|
|
273 <!-- (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} )) -->
|
|
|
274 <!-- $ PComm (λ env → record env {varn = ((varn env) - 1)} )) -->
|
|
|
275
|
|
|
276 ## 証明の一部
|
|
|
277 - 基本的な証明方法は Condtition を変化させて次の Condition が成り立つように変形する
|
|
|
278 - impl⇒
|
|
|
279 ```AGDA
|
|
|
280 lemma1 : {c10 : ℕ} → Axiom (stmt1Cond {c10}) (λ env → record { varn = varn env ; vari = 0 }) (stmt2Cond {c10})
|
|
|
281 lemma1 {c10} env = impl⇒ ( λ cond → let open ≡-Reasoning in
|
|
|
282 begin
|
|
|
283 (Equal (varn env) c10 ) ∧ true
|
|
|
284 ≡⟨ ∧true ⟩
|
|
|
285 Equal (varn env) c10
|
|
|
286 ≡⟨ cond ⟩
|
|
|
287 true
|
|
|
288 ∎ )
|
|
10
|
289 ```
|
|
|
290
|
|
|
291
|
|
11
|
292 <!-- lemma2 : {c10 : ℕ} → Tautology stmt2Cond whileInv -->
|
|
|
293
|
|
|
294 <!-- lemma3 : Axiom (λ e → whileInv e ∧ lt zero (varn e)) (λ env → record { varn = varn env ; vari = vari env + 1 }) whileInv' -->
|
|
|
295
|
|
|
296 <!-- lemma4 : {c10 : ℕ} → Axiom whileInv' (λ env → record { varn = varn env - 1 ; vari = vari env }) whileInv -->
|
|
|
297
|
|
|
298 <!-- lemma5 : {c10 : ℕ} → Tautology ((λ e → Equal (varn e + vari e) c10) and (neg (λ z → lt zero (varn z)))) termCond -->
|
|
10
|
299
|
|
|
300 ## Agda での Gears
|
|
|
301 - Agda での CodeGear は通常の関数とは異なり、継続渡し (CPS : Continuation Passing Style) で記述された関数
|
|
|
302 - CPS の関数は引数として継続を受け取って継続に計算結果を渡す
|
|
|
303 - **名前 : 引数 -> (Code : fa -> t) -> t**
|
|
|
304 - **t** は継続
|
|
|
305 - **(Code : fa -> t)** は次の継続先
|
|
|
306 - DataGear は Agda での CodeGear に使われる引数
|
|
11
|
307 ```AGDA
|
|
|
308 _g-_ : {t : Set} → ℕ → ℕ → (Code : ℕ → t) → t
|
|
|
309 x g- zero next = next x
|
|
|
310 zero g- _ = next zero
|
|
|
311 (suc x) g- (suc y) = next (x g- y)
|
|
|
312 ```
|
|
10
|
313
|
|
|
314 ## Gears をベースにした HoareLogic
|
|
|
315 * 次に Gears をベースにした while Program をみる。
|
|
11
|
316 * このプログラムは自然数と継続先を受け取って t を返す
|
|
10
|
317 ```AGDA
|
|
11
|
318 {-# TERMINATING #-}
|
|
|
319 whileLoop : {l : Level} {t : Set l} -> Env -> (Code : Env -> t) -> t
|
|
|
320 whileLoop env next with lt 0 (varn env)
|
|
|
321 whileLoop env next | false = next env
|
|
|
322 whileLoop env next | true =
|
|
|
323 whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next
|
|
10
|
324 ```
|
|
|
325
|
|
|
326 ## Gears と HoareLogic をベースにした証明
|
|
|
327 * ここでは
|
|
|
328 ```AGDA
|
|
11
|
329 proofGears : {c10 : ℕ } → Set
|
|
|
330 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 → conversion1 n p1
|
|
|
331 (λ n1 p2 → whileLoop' n1 p2 (λ n2 → ( vari n2 ≡ c10 ))))
|
|
10
|
332 ```
|
|
|
333
|
|
|
334
|
|
11
|
335 ## まとめと今後の課題
|
|
|
336 - HoareLogic の while を使った例題を作成、証明を行った
|
|
|
337 - Gears を用いた HoareLogic ベースの検証方法を導入した
|
|
|
338 - 証明が引数として渡される記述のため証明とプログラムを一体化できた
|
|
|
339 - 今後の課題
|
|
|
340 - RedBlackTree や SynchronizedQueue などのデータ構造の検証(HoareLogic ベースで)
|
