1. 自分について
-
セキュリティの勉強をしているおっさんです
-
数学が好きですが、最近ちゃんと時間が取れていません
-
Lean という定理証明支援系の言語を知り、
- プログラムと証明が一体、という発想がやたらカッコいい
- 「型が命題で、値が証明」と言われて、正直よくわからない
-
そこで、セキュリティ文脈で頻出の Bell-LaPadula モデルを
Leanで定義＆証明して勉強しよう、というのがこの記事です
この記事のゴールは以下です。
- Bell-LaPadulaモデルを Lean のコードとして定義する
- read / write 制約を Prop(命題)として表現する
- いわゆる no write down を定理として証明する
2. Leanについて
Leanは
- プログラミング言語
- 定理証明支援系（Theorem Prover）
を同時に満たす言語です。
そして面白いのがこの対応関係です。値が型の証明とかほんとですか？という感じです。
（命題Pを満たすような証明pが存在するならばその命題は真、といったん理解）
- 型 (Type) ＝ 命題 (Proposition)
- 値 (term) ＝ その命題の証明 (Proof)
たとえば
-
P : Propは「Pという命題」 -
p : Pは「Pの証明」
という意味になります。
theorem は
「ある命題（型）の値（証明）を定義する」
という宣言です。
3. Bell-LaPadulaモデルについて
Bell-LaPadula（BLP）は 機密性（Confidentiality） を守るための古典的モデルです。
典型的なセキュリティレベルは次のような順序を持ちます。
$$
\text{Unclassified} \le \text{Confidential} \le \text{Secret} \le \text{TopSecret}
$$
BLPのポイントは次の2つの制約です。（CISSPの試験にでます）
Simple Security Property（no read up）
- 主体（subject）は
自分より高いレベルの対象（object）を読めない - 条件としては
$$
object.level \le subject.level
$$
*-property（スター制約、no write down）
- 主体は
自分より低いレベルに書き込めない - 条件としては
$$
subject.level \le object.level
$$
これをLeanでそのまま「命題」として書いていきます。
4. Leanコードを順に書いていく
4.1 セキュリティレベルの定義
/- Bell-LaPadula model -/
/-- セキュリティレベルをデータ型として定義 -/
inductive Level
| Unclassified
| Confidential
| Secret
| TopSecret
deriving DecidableEq
解説
-
inductiveは列挙型（代数的データ型）です -
Level.Unclassifiedなどの値が作られます -
deriving DecidableEqにより
「レベル同士が等しいかどうか」を判定できるようになる、というオプションです。（実は今回使いません）
4.2 レベルの順序関係 leqを定義
open Level
def leq : Level → Level → Prop
| Unclassified, _ => True
| Confidential, Confidential => True
| Confidential, Secret => True
| Confidential, TopSecret => True
| Secret, Secret => True
| Secret, TopSecret => True
| TopSecret, TopSecret => True
| _, _ => False
解説
def leq : Level → Level → Prop
Level → Level → Prop は 2引数関数で、先ほど定義したlevelデータ型を2つ引数にしてpropを返す、つまり
leq a b は「a ≤ b が成り立つ」という 命題（Prop）を返す、という宣言です。
Prop なので、返り値は True/False（命題としての真偽）になります。
ちょっとdef leq : Level → Level → Prop 引数2つと返値がなんで同じ感じでていぎされてるの？？って感じです。これは
def leq : Level → (Level → Prop) で
leq は levelを引数に 「levelを引数にPropを返す関数」を返す関数
となるので、結果的に2つの引数をとる関数と同等になります。
定義されたleq は 「x ≤ y という命題」を返します。True/False を返しているので計算っぽく見えますが、あくまで「命題」です。
| Unclassified, _ => True
は、パターンマッチで、左が Unclassified なら右が何でも True。
| Confidential, Secret => True
は、Confiental < Secret はTrueであることを表しています。
要は全列挙してTrue/Falseを定義しています。
全列挙しているので本当は順序を定義して推移律を入れたいところです。
4.3 Subject / Object の定義
structure Subject where
id : String
level : Level
structure Object where
id : String
level : Level
解説
-
structureはレコード型です -
s : Subjectに対してs.levelのように参照できます
4.4 アクセス種別
inductive Access
| read
| write
read / write の2種類だけ定義します。
4.5 BLPの性質を命題として定義
def simple_security (s : Subject) (o : Object) : Prop :=
leq o.level s.level
def star_property (s : Subject) (o : Object) : Prop :=
leq s.level o.level
-
simple_security
→ no read up -
star_property
→ no write down
どちらも Propを返す関数です。
単純な定義ですが、個人的にはおお、simple securityが！！とか *-propertyが！！とか興奮気味ですｗ
4.6 アクセス可否の定義
def blp_allowed (s : Subject) (o : Object) (a : Access) : Prop :=
match a with
| .read => simple_security s o
| .write => star_property s o
アクセス種別ごとに
適用される制約を切り替えています。
5. 定理：no write down
5.1 定理の定義
theorem no_write_down :
∀ (s : Subject) (o : Object),
s.level = TopSecret →
o.level = Unclassified →
¬ blp_allowed s o Access.write :=
by
intro s o hs ho h
simp [blp_allowed, star_property, hs, ho] at h
exact h
5.2 証明の読み方
-
¬ Pは Lean ではP → False -
つまり
- write が許可されると仮定して
- 矛盾（False）を導けばよい
simp により
blp_allowedstar_propertyleq TopSecret Unclassified
が展開され、
最終的に False が得られます。
exact h は
「その False を証明として提出する」
という意味です。
地味ですが、write許可がfalseとなるので成功です！！
（地味すぎる）
6. まとめ
- Bell-LaPadulaモデルを Lean で素直に表現できた
- 「no write down」が
定理としてコンパイル可能になった
Leanは最初とっつきにくいですが、
「仕様をコードにしたら、その正しさを証明できる」という感じで興味深いです。
まあ、これは単純すぎてそもそも No Write Down / No Read Up の成立は明確ですが、より複雑な仕様で役に立ちそうです。
Appendix: 全コード（コピペ用）
inductive Level
| Unclassified
| Confidential
| Secret
| TopSecret
deriving DecidableEq
open Level
def leq : Level → Level → Prop
| Unclassified, _ => True
| Confidential, Confidential => True
| Confidential, Secret => True
| Confidential, TopSecret => True
| Secret, Secret => True
| Secret, TopSecret => True
| TopSecret, TopSecret => True
| _, _ => False
structure Subject where
id : String
level : Level
structure Object where
id : String
level : Level
inductive Access
| read
| write
def simple_security (s : Subject) (o : Object) : Prop :=
leq o.level s.level
def star_property (s : Subject) (o : Object) : Prop :=
leq s.level o.level
def blp_allowed (s : Subject) (o : Object) (a : Access) : Prop :=
match a with
| .read => simple_security s o
| .write => star_property s o
theorem no_write_down :
∀ (s : Subject) (o : Object),
s.level = TopSecret →
o.level = Unclassified →
¬ blp_allowed s o Access.write :=
by
intro s o hs ho h
simp [blp_allowed, star_property, hs, ho] at h
exact h