情報科学 › Claude Code の中身 › 安全性

外へ出る経路ができる条件

命題 4.2（「安全性」§4）・ ✓公理まで証明済み

情報の流れの模型（定義 4.1）で次が成り立つ。

(a)・(b)・(c) がすべて成り立つならば、あるモデル $M$ と信頼できない入力 $u$ があって、どんな $s$ についても $\mathrm{Ext}(M, t, u, s)$ に $s$ が現れる。
(a) が成り立たなければ、どんな $M$ 、 $t$ 、 $u$ についても、 $\mathrm{Ext}(M, t, u, s)$ は $s$ に依らない。
(b) が成り立たなければ、どんな $M$ 、 $t$ 、 $s$ についても、 $\mathrm{Ext}(M, t, u, s)$ は $u$ に依らない。
(c) が成り立たなければ、 $\mathrm{Ext}(M, t, u, s)$ は常に空である。

本文で読む（証明と前後の説明）→

閉包の状態

✓ 公理まで証明済み

証明が使う定理を前提としてたどると、Rikai の中の証明だけで定義・公理（物理では基本仮定）までつながっています（前提の定理類 3 件、定義なども含めて 4 件）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

前提をたどる証明が使う定理・定義（直接 1 件）

▸ を開くと、その項目の証明が使う前提が出ます。深い先は各項目のページでたどれます。

能力による上界と、その達成✓定理 3.2・安全性
- 判定は規則の集合と呼び出しだけで決まる✓定理 3.4・ツールと権限
  - 設定の階層と規則の合併定義 3.3・ツールと権限
- deny の単調性：規則を足しても安全側にしか動かない✓命題 3.6・ツールと権限

これを使っている定理

証明で明示的に参照している定理は、まだありません。

関連するノック 3 問