第24章. 情報流ラベル

この章の目的

この章を読み終える頃には、ある値に「機密」の印を付けて、その値が許されない場所に流れていないことを言語に確認させられるようになります。この章を読み終える頃には、ある値に「機密」の印を付けて、その値が許されない場所に流れていないことを言語に確認させられるようになります。

これは応用的な章で、第6部の最後の章です。ここで扱う機能は普段のプログラムには必要ありません。データを機密に保たなければならないプログラムのためにあります。これは応用的な章で、第6部の最後の章です。ここで扱う機能は普段のプログラムには必要ありません。データを機密に保たなければならないプログラムのためにあります。

ラベルは型に乗る

マスター録音はスタジオの外に出ない約束のものです。プログラムも同じ性質のデータを扱うことがあります — 公の出力に届いてはいけない値です。Keleusmaは型に「ラベル」を持たせることができます。ラベルは値に付く印で、値と一緒に旅をします。ラベルは型のあとに@を付けて書きます。マスター録音はスタジオの外に出ない約束のものです。プログラムも同じ性質のデータを扱うことがあります — 公の出力に届いてはいけない値です。Keleusmaは型に「ラベル」を持たせることができます。ラベルは値に付く印で、値と一緒に旅をします。ラベルは型のあとに@を付けて書きます。

fn main() -> Word@Master {
    classify 42@Master
}

keleusma runで実行します。出力は42です。

Word@Masterは、Masterというラベルを持ったWordです。演算子classify 42@Masterは、ただの値42を取ってMasterラベルを付けます。ラベルの名前はプログラマが選びます。ここではMasterがその一つです。Word@Masterは、Masterというラベルを持ったWordです。演算子classify 42@Masterは、ただの値42を取ってMasterラベルを付けます。ラベルの名前はプログラマが選びます。ここではMasterがその一つです。

ラベルが存在するのは、プログラムが確認されている間だけです。プログラムが走り始めると、ラベルは消えていて、値はただの42になります。ラベルは実行時のコストがゼロです。事前に言語が行う確認のためだけのものです。ラベルが存在するのは、プログラムが確認されている間だけです。プログラムが走り始めると、ラベルは消えていて、値はただの42になります。ラベルは実行時のコストがゼロです。事前に言語が行う確認のためだけのものです。

ラベルは漏えいを防ぐ

ラベルが意味を持つのは、言語がそれを追跡するからです。ラベル付きの値は、そのラベルを受け入れない場所には流れられません。ここでは関数broadcastがただのWordを公の出力に送ります。ラベルが意味を持つのは、言語がそれを追跡するからです。ラベル付きの値は、そのラベルを受け入れない場所には流れられません。ここでは関数broadcastがただのWordを公の出力に送ります。

fn broadcast(x: Word) -> Word {
    x
}

fn main() -> Word {
    let take = classify 42@Master;
    broadcast(take)
}

実行します。結果は無く、こう出ます。

error: compile: type error: argument to `broadcast` expects Word, got Word@Master

値takeはMasterラベルを持っています。broadcastのパラメータはただのWordで、ラベルは無く、つまりMasterラベル付きのデータを受け取れません。takeをbroadcastに渡すと、マスター録音が公の出力に届いてしまいます。言語はそれを「漏えい(leak)」と呼び、プログラムが走る前に却下します。値takeはMasterラベルを持っています。broadcastのパラメータはただのWordで、ラベルは無く、つまりMasterラベル付きのデータを受け取れません。takeをbroadcastに渡すと、マスター録音が公の出力に届いてしまいます。言語はそれを「漏えい(leak)」と呼び、プログラムが走る前に却下します。

declassify: 意図的な解放

ときには機密データを本当に解放するべき場合もあります — 明示的な決定として。declassifyという演算子はラベルを取り除きます。ときには機密データを本当に解放するべき場合もあります — 明示的な決定として。declassifyという演算子はラベルを取り除きます。

fn broadcast(x: Word) -> Word {
    x
}

fn main() -> Word {
    let take = classify 42@Master;
    broadcast(declassify take@Master)
}

実行します。出力は42です。declassify take@MasterがMasterラベルを取り除き、ただのWordにして、broadcastが受け取れるようにしました。実行します。出力は42です。declassify take@MasterがMasterラベルを取り除き、ただのWordにして、broadcastが受け取れるようにしました。

2つの演算子は重みが同じではありません。classifyは制限を加えるだけで、常に安全です。declassifyは制限を取り除くので、プログラムの中で機密データが解放される、唯一の見える場所になります。プログラムを読むレビュー担当者は、declassifyを検索すれば解放の場所すべてを見つけられます。2つの演算子は重みが同じではありません。classifyは制限を加えるだけで、常に安全です。declassifyは制限を取り除くので、プログラムの中で機密データが解放される、唯一の見える場所になります。プログラムを読むレビュー担当者は、declassifyを検索すれば解放の場所すべてを見つけられます。

この章のまとめ

• 型はラベルを持つことができ、T@Labelと書いて値に印を付けます。
• classify expr@Labelはラベルを加え、declassify expr@Labelはラベルを取り除きます。classify expr@Labelはラベルを加え、declassify expr@Labelはラベルを取り除きます。
• 言語はラベル付きの値を追跡し、ラベルを受け入れない場所への流れを、プログラムが走る前に却下します。言語はラベル付きの値を追跡し、ラベルを受け入れない場所への流れを、プログラムが走る前に却下します。
• ラベルはプログラムが走る前に消えて、実行時のコストはゼロです。
• declassifyは機密データが解放される、意図的で見える場所です。

これで第6部は完了です。スクリプト作者が書く言語の全体をひと通り見たことになります。第7部では、書かれたあとのプログラムに何が起こるか — コンパイル、署名、差し替え — に進みます。これで第6部は完了です。スクリプト作者が書く言語の全体をひと通り見たことになります。第7部では、書かれたあとのプログラムに何が起こるか — コンパイル、署名、差し替え — に進みます。