要約

  • Dorothy E. Denning は1976年の単著論文で、セキュリティ・クラスを偏順序として扱い、複数入力の影響を受ける結果に必要な最小クラスを最小上界（join）で求めた。
  • 代入や入出力による明示的フローだけでなく、条件分岐が作る暗黙の依存も対象になる。ただし証明は、宣言されたクラスとプログラム表現に現れるフローの内側に限られる。
  • 秘密チャネル、誤分類、実装不具合、根拠のない機密解除は別の統制を要する。格子検査の合格は一つの証拠であり、システム全体の安全判定ではない。

二つの入力から一つの結果を作るとき、その結果にはどの機密度が必要だろうか。Dorothy E. Denning は1976年の “A Lattice Model of Secure Information Flow” で、両方の入力が到達を許される最も低いクラスを求める、と定式化した。それが最小上界、すなわち join である。出力先は、その結合クラスからの情報を受け取れる場所でなければならない。

Denning は A → B を「クラスAの情報がクラスBへ流れることを許される」と定義する。この関係は反射的、推移的、反対称的であり、偏順序になる。「偏」であることは重要だ。二つの部門や案件のクラスは互いに比較不能でもよく、上位に共通の受け皿だけを持てる。join は、その政策のなかで最小の共通到達点を選ぶ。

出力 c が入力 a と b に依存するなら、条件は class(a) join class(b) → class(c) と読める。ここで証明されるのは、c が現実世界で安全だということではない。宣言済みの分類と順序を前提に、二つの入力が c へ影響することを政策が許している、という限定された主張である。

コピーではなく影響を見る

モデルの核心は、情報フローを値のコピーだけでなく「影響」として捉える点にある。b := a は明示的フローである。一方、条件式は値をコピーしなくても暗黙のフローを生む。

論文の例 if a = 0 then b := c では、b が変化したかどうかから a に関する情報が漏れ得る。したがって c から b への代入だけでなく、a から b への制御依存も検査対象になる。転送されたバイトだけを追う設計では、この第二の経路を見落とす。

現在のソフトウェアでも同じ問題がある。アクセス権表は誰がデータを読めるかを示すが、分岐、例外、エラー表示、カウンタ、資源選択、応答時間も情報を運ぶ。Denning の枠組みは、どの入力がどの出力を左右するかを列挙し、入力クラスを結合し、行き先が政策上許されるかを問う。

コンパイル時認証の射程

変数や式にクラスを割り当て、条件式のクラスを影響先へ伝播させれば、実行前に違反を検出できる。後続の “Certification of Programs for Secure Information Flow” は、その認証方法を詳しく展開した。

ここでは著者も区別しなければならない。1976年の格子モデル論文は Dorothy E. Denning の単著である。認証論文は Dorothy E. Denning と Peter J. Denning の共著で、Purdue Technical Report 76-181 を経て1977年に Communications of the ACM に掲載された。後者を Dorothy 一人の成果として扱えば共同研究者を消し、二本を同じ論文として扱えばモデルから認証技法への発展を消してしまう。

認証が与える保証は小さくない。審査者は「下位へ漏らさないはずだ」という意図ではなく、モデル化された変数、演算、制御構造ごとに、導出クラスが出力先へ流れることを許されるか確認できる。ソース変更後に同じ検査を繰り返すことも可能だ。

モデルの外側

同時に、1976年論文は限界を明記している。対象は正規のチャネルと記憶チャネルであり、プロセスがシステム負荷を変えて信号を送るような秘密チャネルは扱わない。プログラム表現に書かれていないフローは認証できない。境界検査の欠落、ダングリング参照、コンパイラ不具合、認証済みソースと異なるバイナリ、ハードウェア故障は、形式上の意味と実行結果を切り離す。

入力となる政策も誤り得る。機密データを公開扱いにすれば、解析は誤った前提のもとで正しくフローを許可してしまう。逆方向の問題もある。Dorothy と Peter Denning の共著 “Data Security” は、上向きのフローだけを許す分類方式が過剰分類を招きやすいと論じる。正当なダウングレードや情報を失わせる変換には役割があるが、誰が何を根拠に許可し、どの情報が除去されたかという別の証拠が必要だ。

時間や資源消費を使う秘密チャネルは、代入として現れない。形式上許された出力でも、安全でない端末、広すぎる受信者、ラベルを捨てる下流へ届けば問題になる。格子はそれらをすべて解決すると主張していない。「モデル適合」を「現実の安全」に言い換える側が境界を越えるのである。

Denning は1999年の講演 “The Limits of Formal Security Models” で、形式的方法が簡略化されたモデルと仮定の内側で結論を与える一方、現実の攻撃はしばしば箱の外へ出ると振り返った。形式手法を弱める主張ではない。合格結果に、何を証明していないかまで添えるための原則である。

一枚の証明を証拠連鎖へ置く

実務で必要なのは「安全」という一語のバッジではなく、次の連鎖である。

  1. クラス、join、許可フローを定義する版管理された政策
  2. データと出力へ付けたラベルの根拠
  3. 明示的依存とモデル化された暗黙依存の解析結果
  4. 審査済みソース、解析器、コンパイラ、バイナリ、配備を結ぶ再現可能な来歴
  5. 機密解除の独立した権限と記録
  6. ラベルと宛先を保つ実行時・端末統制
  7. 静的モデル外の秘密チャネルとサイドチャネルの検査・監視

Bell–LaPadula は多段階セキュリティの隣接する系譜であり、Denning の参考文献にも登場する。しかし、それを彼女自身の依存関係の議論と置き換えてはならない。アクセス制御が主体の操作権限を問うのに対し、この格子モデルは、結果に実際に影響する情報からどのクラスが導かれるかを問う。

この限定こそが論文を古びさせない。万能な証明でも単なる比喩でもなく、一つの問いを検査可能にし、残る問いを隠さないための道具だからだ。

出典