|
23
|
1 \chapter{OSとアプリケーションの信頼性}
|
|
2
|
2
|
|
|
3 コンピューター上では様々なアプリケーションが常時動作している。
|
|
|
4 動作しているアプリケーションは信頼性が保証されていてほしい。
|
|
|
5 信頼性の保証には、 実行してほしい一連の挙動をまとめた仕様と、 それを満たしているかどうかの確認である検証が必要となる。
|
|
|
6 アプリケーション開発では検証に関数や一連の動作をテストを行う方法や、デバッグを通して信頼性を保証する手法が広く使われている。
|
|
|
7
|
|
29
|
8 実際にアプリケーションを動作させるOSは、アプリケーションよりさらに高い信頼性が保証される必要がある。
|
|
2
|
9 OSはCPUやメモリなどの資源管理と、 ユーザーにシステムコールなどのAPIを提供することで抽象化を行っている。
|
|
|
10 OSの信頼性の保証もテストコードを用いて証明することも可能ではあるが、 アプリケーションと比較するとOSのコード量、 処理の量は膨大である。
|
|
|
11 またOSはCPU制御やメモリ制御、 並列・並行処理などを多用する。
|
|
|
12 テストコードを用いて処理を検証する場合、テストコードとして特定の状況を作成する必要がある。
|
|
|
13 実際にOSが動作する中でバグやエラーを発生する条件を、 並列処理の状況などを踏まえてテストコードで表現するのは困難である。
|
|
|
14 非決定的な処理を持つOSの信頼性を保証するには、 テストコード以外の手法を用いる必要がある。
|
|
|
15
|
|
15
|
16
|
|
2
|
17 テストコード以外の方法として、 形式手法的と呼ばれるアプローチがある。
|
|
29
|
18 形式手法の具体的な検証方法の中で、 証明を用いる方法\cite{Yang:2010:SLI:1806596.1806610}\cite{Klein:2009:SFV:1629575.1629596}\cite{Sigurbjarnarson:2016:PVF:3026877.3026879}\cite{Chen:2015:UCH:2815400.2815402}とモデル検査を用いる方法がある。
|
|
30
|
19 証明を用いる方法ではAgda\cite{agda}やCoq\cite{coq}などの定理証明支援系を利用し、 数式的にアルゴリズムを記述する。
|
|
15
|
20 Curry-Howard同型対応則により、型と論理式の命題が対応する。
|
|
|
21 この型を導出するプログラムと実際の証明が対応する。
|
|
30
|
22 証明には特定の型を入力として受け取り、証明したい型を生成する関数を作成する。
|
|
|
23 整合性の確認は、記述した関数を元に定理証明支援系が検証する。
|
|
15
|
24 証明を使う手法の場合、 実際の証明を行うのは定理証明支援系であるため、 定理証明支援系が理解できるプログラムで実装する必要がある。
|
|
|
25 AgdaやCoqの場合はAgda、 Cow自身のプログラムで記述する必要がある。
|
|
|
26 しかしAgdaで証明ができてもAgdaのコードを直接OSのソースコードとしてコンパイルすることはできない。
|
|
|
27 Agda側でCのソースコードを吐き出せれば可能ではあるが、 現状は検証したコードと実際に動作するコードは分離されている。
|
|
30
|
28 検証されたアルゴリズムをもとにCで実装することは可能であるが、 この場合移植時にバグが入る可能性がある。
|
|
15
|
29 検証ができているソースコードそのものを使ってOSを動作させたい。
|
|
|
30
|
|
|
31
|
|
|
32 他の形式手法にモデル検査がある。
|
|
55
|
33 モデル検査はプログラムの可能な実行をすべて数え上げて要求している使用を満たしているかどうかを調べる手法である。
|
|
23
|
34 例えばJavaのソースコードに対してモデル検査をするJavaPathFinderなどがある。
|
|
15
|
35 モデル検査を利用する場合は、実際に動作するコード上で検証を行うことが出来る。
|
|
23
|
36 OSのソースコードそのものをモデル検査すると、実際に検証されたOSが動作可能となる。
|
|
26
|
37 しかしOSの処理は膨大である。
|
|
|
38 すべての存在可能な状態を数え上げるモデル検査では状態爆発が問題となる。
|
|
|
39 状態を有限に制限したり抽象化を行う必要がある。
|
|
23
|
40
|
|
|
41
|
|
|
42 OSのシステムコールは、ユーザーからAPI経由で呼び出され、 いくつかの処理を行う。
|
|
|
43 その処理に着目するとOSは様々な状態を遷移して処理を行っていると考えることができる。
|
|
|
44 OSを巨大な状態遷移マシンと考えると、 OSの処理の特定の状態の遷移まで範囲を絞ることができる。
|
|
|
45 範囲が限られているため、有限時間でモデル検査などで検証することが可能である。
|
|
30
|
46 この為にはOSの処理を証明しやすくする表現で実装する必要がある。\cite{hyperkernel}
|
|
|
47 証明しやすい表現の例として、 状態遷移ベースでの実装がある。
|
|
23
|
48
|
|
|
49
|
|
24
|
50 証明を行う対象の計算は、 その意味が大きく別けられる。
|
|
|
51 OSやプログラムの動作においては本来したい計算がまず存在する。
|
|
|
52 これはプログラマが通常プログラミングするものである。
|
|
28
|
53 これら本来行いたい処理のほかに、 CPU、メモリ、スレッドなどの資源管理なども必要となる。
|
|
|
54 前者の計算をノーマルレベルの計算と呼び、後者をメタレベルの計算と呼ぶ。
|
|
|
55 OSはメタ計算を担当していると言える。
|
|
26
|
56 ユーザーレベルから見ると、データの読み込みなどは資源へのアクセスが必要であるため、システムコールを呼ぶ必要がある。
|
|
32
|
57 システムコールを呼び出すとOSが管理する資源に対して何らかの副作用が発生するメタ計算と言える。
|
|
|
58 副作用は関数型プログラムの見方からするとモナドと言え、 モナドもメタ計算ととらえることができる。
|
|
|
59 OS上で動くプログラムはCPUにより並行実行される。この際の他のプロセスとの干渉もメタレベルの処理である。
|
|
28
|
60 実装のソースコードはノーマルレベルであり検証用のソースコードはメタ計算だと考えると、OSそのものが
|
|
|
61 検証を行ない、システム全体の信頼を高める機能を持つべきだと考える。
|
|
26
|
62 ノーマルレベルの計算を確実に行う為には、メタレベルの計算が重要となる。
|
|
|
63
|
|
|
64
|
|
|
65 プログラムの整合性の検証はメタレベルの計算で行いたい。
|
|
24
|
66 ユーザーが実装したノーマルレベルの計算に対応するメタレベルの計算を、自由にメタレベルの計算で証明したい。
|
|
|
67 またメタレベルで検証ががすでにされたプログラムがあった場合、都度実行ユーザーの環境で検証が行われるとパフォーマンスに問題が発生する。
|
|
|
68 この場合はメタレベルの計算を検証をするもの、しないものと切り替えられる柔軟なAPIが必要となる。
|
|
|
69 メタレベルの計算をノーマルレベルの計算と同等にプログラミングできると、動作するコードに対して様々なアプローチが掛けられる。
|
|
|
70 この為にはノーマルレベル、メタレベル共にプログラミングできる言語と環境が必要となる。
|
|
|
71
|
|
28
|
72 プログラムのノーマルレベルの計算とメタレベルの計算を一貫して行う言語として、 Continuation Based C(CbC)を用いる。
|
|
32
|
73 CbCは基本\texttt{goto文}で\texttt{CodeGaar}というコードの単位を遷移する言語である。通常の関数呼び出しと異なり、スタックあるいは環境と呼ばれる隠れた状態を持たない。
|
|
|
74 このため、計算のための情報は\texttt{CodeGear}の入力にすべてそろっている。
|
|
|
75 そのうちのいくつかはメタ計算、つまり、OSが管理する資源であり、その他はアプリケーションを実行するためのデータ(\texttt{DataGear})である。
|
|
28
|
76 メタ計算とノーマルレベルの区別は入力のどこを扱うかの差に帰着される。
|
|
32
|
77 CbCはCと互換性のあるCの下位言語である。
|
|
28
|
78 CbCは\texttt{GCC}\cite{gcc}\cite{weko_82695_1}あるいは\texttt{LLVM}\cite{llvm}\cite{llvmcbc}上で実装されていて、通常のCのアプリケーションやシステムプログラ厶をそのまま包含できる。
|
|
32
|
79 Cのコンパイルシステムを使える為に、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
|
|
|
80 またCbCの基本文法は簡潔であるため、 Agdaなどの定理証明支援系\cite{agda-ryokka}との相互変換や、 CbC自体でのモデル検査が可能であると考えられる。
|
