静的保証（2/2）

これで、静的プログラム解析における課題について、非形式的な理解が得られました。 あるいは、ポインター解析がなぜ難しいのかについて、いくつか直感を得られただけかもしれません。 そして厄介なことに、ポインターは私たちのシステムプログラミングに欠かせない存在です。 高性能なソフトウェアを書くには、参照渡しのセマンティクスが必須です。

ここから Rust におけるトレードオフが始まります。 まず、生ポインターを捨て、代わりに参照に頼らなければなりません（これについては後述します）。 次に、参照を使うときには常に従わなければならないルールがあります。

しかし、本当に昔ながらのポインターが必要な場合はどうなるのでしょうか？

抽象化は、「その前提が、それが存在するコンテキストと一致している」場合に有用です¹。 ポインターは、メモリとの相互作用を容易にする抽象化です。

プログラムを安全な Rust の制約内で表現できない場合²でも、unsafe キーワードを使ってそのプログラムを書くことができます。 このキーワードが示すとおり、限定されたスコープについて、コンパイラによって強制される特定の安全性保証を放棄することになります。 unsafe ブロックの内部では、自らの責任で生ポインターを使用できます。 正しさの証明責任は、プログラマーであるあなたの肩に完全にかかっています。

そのような「オプトアウト」メカニズムがあることは、解析を完全に中止するよりも優れています。 実際、unsafe により、既存の C コードとのシームレスな統合が可能になります。 その相互運用性が、Rust の実世界での利用の多くを可能にしています。

unsafe は弱点ではないのでしょうか？保証をすべて失うのではないでしょうか？

正確にはそうではありません。 Rust の型システムの形式的検証に関する研究は、unsafe が存在していてもセキュリティ上の主張を維持できることを示しています³。

形式手法を使わなくても、安全な抽象化はunsafe な操作の上に構築できます⁴。 どのように呼び出されても安全性の不変条件を維持するインターフェイスを、注意深く設計できます。 内部で unsafe を使っているにもかかわらずです。 ただし、そのような設計の正しさをコンパイラが自動的に検証することはできません。 第13章では、unsafety と unsoundness の違いについて説明します。

しかし、もっと単純な見方を考えてみましょう。使用する unsafe が少なければ少ないほど、メモリ関連のバグについて監査しなければならないコード全体は少なくなります。

コードベースが safe と unsafe で 50/50 に分かれている場合でさえ、セキュリティレビュー、デバッグ時間、パッチのデプロイにかかるコストを大幅に節約できます。これは、後者の unsafe な半分が、安全な Rust と相互運用する C や C++ である場合でも当てはまります。

Rust の静的戦略

以下は、私たちのお気に入りの小さな厄介者である C の incr 関数を、Rust で書き直したものです。

fn incr(a: &mut isize, b: &isize) {
    *a += *b;
}

C 版を一つひとつ分解したので、この関数が何をするかはすでにご存じでしょう。 少し時間を取って、上のコードを確認してください。 構文について、いくつか推測できますか？

関数の本体はまったく同じです。 * は依然として逆参照演算子です。 += は同じ省略記法です。 isize は符号付き整数を表すキーワードで、C の int と同じようなものです。

しかし、Rust と C の incr 関数には 2 つの違いがあります。 1 つ目は細かな点です。戻り値の型がありません。 void が暗黙に指定されます。Rust では、関数が実際に値を返す場合にのみ、明示的な戻り値の型注釈が必要だからです。

2 つ目の違い、つまりポインターを使わなくなったという事実のほうが、はるかに重要です。 関数シグネチャを見ると、次のようになります。

• & は参照です。これはポインターに似ていますが、任意の値にはなれません。Rust は、それが初期化済み変数の有効なアドレスであることを保証します。

  • 前のセクションで述べたメモリモデルの問題を修正したことになります。逆参照演算子 * を使うとき、クラッシュしたり不正なデータを読み取ったりするリスクはありません。

• &mut は「可変参照」を意味します。この関数は、a が指す変数に書き込む能力を得ます。b についてはそうではありません。b は取るに足らない「不変参照」（単なる &）だからです。Rust は今や、任意のデータ片について、任意の時点で可変参照は 1 つだけ存在することを保証します。

  • 任意の時点で可変参照が 1 つしか存在できないなら、b が a と同じデータ片を参照することはできません。2 つのパラメーターは、決してエイリアスしないことが保証されています。

Rust について今述べたことの重大さを振り返る価値があります。 強力な静的保証の世界全体が開かれたのです。

前のセクションでは、incr 関数について議論しながら、判定不能なエイリアシングが過大近似を強いること、クラッシュの可能性、任意メモリの読み取りなど、悲哀に浸っていました。

その関数を Rust に移植すると、それをコンパイルする（実行可能プログラムを作成する）という行為だけで、このプログラムが期待どおりに 2 つの異なる整数を加算することを実際に証明します。つまり、計算機科学者たちは、Rust の型システム（それらの保証の源です^{5 6}）の形式的検証⁷について初期の研究を行っています。

Rust が適している場面で Rust を活用することで、高いレベルの保証を得られます。 少なくともメモリ安全性に関してはそうです。 それでも、incr のビジネスロジック（incr がインクリメントしている値の大局的な意味や、それらをインクリメントすることに意味があるかどうか）については何も保証していません。 木を見て森を見失わないようにしましょう。

C++ にも参照があるのではないですか？

はい。 しかし、その参照はメモリ安全ではありません。

C++ の参照は任意の値に設定できないため、生ポインターよりも正しく使いやすいものです。 しかし、それでも可変エイリアスを許します。 それは検証と並行コードの両方にとって問題です。

また、有効性も強制しません。 C++ では、すでに「存在しなくなった」オブジェクト、つまり解放済みのオブジェクトへの参照を誤って使用することがあります。これはバグであり、潜在的には脆弱性です。Rust はこれを防ぎます。

私たちの主張を検証する

セキュリティが要件であるときには、「信頼せよ、されど検証せよ」という考え方を採用するとよいでしょう。 では、Rust の解析が実際にどのように働くかを見てみましょう。 次の有効なプログラムを考えてください。

fn incr(a: &mut isize, b: &isize) {
    *a += *b;
}

fn main() {
    // 整数
    let mut val = 40;
    let step = 2;

    // 整数への参照
    let a = &mut val;
    let b = &step;

    println!("Before incr: a == {}, b == {}", a, b);
    incr(a, b);
    println!("After incr: a == {}, b == {}", a, b);
}

前のセクションの最初の図の組を思い出してください。そこでは、エイリアシングも無効なポインターもありませんでした。 このプログラムは次のように出力します。

Before incr: a == 40, b == 2
After incr: a == 42, b == 2

呼び出しの後、私たちはその2つ目の「良い」図に到達しました。

この関数は期待どおりに動作します。 フォーマット指定子 {} が、整数そのものを出力するために逆参照を行ってくれる点に注目してください。

Rust の参照では、無効なポインタを生成する方法はありません。 そのため、それは試すことすらできません。 では、参照にエイリアスを作ろうとして、前のセクションで見た問題のあるエイリアシング図を作り出そうとするとどうなるでしょうか？

fn incr(a: &mut isize, b: &isize) {
    *a += *b;
}

fn main() {
     // 整数
    let mut val = 40;
    let step = 2;

    // 整数 `val` へのエイリアス参照
    let a = &mut val;
    let b = a;

    println!("Before incr: a == {}, b == {}", a, b);
    incr(a, b);
    println!("After incr: a == {}, b == {}", a, b);
}

このプログラムは実行されることはありません。代わりに、コンパイル時エラーが発生します。

error[E0382]: borrow of moved value: `a`
  --> src/main.rs:16:10
   |
11 |     let a = &mut val;
   |         - move occurs because `a` has type `&mut isize`, which does not implement the `Copy` trait
12 |     let b = a;
   |             - value moved here
...
16 |     incr(a, b);
   |          ^ value borrowed here after move

For more information about this error, try `rustc --explain E0382

このエラーはおそらく混乱を招くでしょう。 コンパイラは、一意な可変参照を複製することはできないと指摘しています。 それは、特に並行プログラムでは潜在的に危険なエイリアスになります。 このエラーは、第3章で「所有権」と「トレイト」を扱った後で、より理解しやすくなるでしょう。

話がうますぎるのでは？

ここまでで、Rust のコンパイラが可変エイリアシングを素早く効果的に検出する様子を見てきました。 Rust が C のようなメモリ制御を提供するなら、コンパイラ内部の解析も、これまで説明した points-to 解析と同じ根本的な障害に突き当たるはずではないでしょうか？

意外かもしれませんが、答えはノーです。 ここには、互いに関連する3つの要因があります。

• 型システムによるサポート: Rust の内部解析器は、言語そのものとの直接的な統合という土台、つまり型システムの上に構築されています。この型システムは「アフィン型」⁸の一種を実装しており、任意の型キャストを許可しません。

  • 弱い型付けの言語（C など）に対して静的解析を行っても、これに匹敵する共同設計上の利点はありません。Rust コンパイラは、C 系のコンパイラや解析ツールでは証明できない性質を、設計上証明できます。

• 実行時サポート: Rust のメモリ安全性の保証がすべてコンパイル時に強制されるわけではありません。一部のチェックは実行時に行う必要があるため、Rust コンパイラはその目的のために追加のコードを挿入します。それらのチェックが失敗すると、Rust プログラムは終了する可能性があります。

  • メモリが破壊されたり悪用されたりしたプログラムが激しく死ぬよりは、正常な終了のほうが望ましいものの、理想的ではありません。この本の後半では、実行時の「パニック」に対する堅牢性テストを扱います。

• 強い制約: 安全な Rust プログラムは、一連の特別なルールに従わなければなりません。mut キーワードには規定があります。型システムの機能であるこれらの制約により、一部のアルゴリズムは Rust で表現しにくくなります。少なくとも、捉え直しなしには難しいのです。

  • これらの制約の中で最も悪名高いものは、参照は共有（&T）または可変（&mut T）のどちらかにはなれるが、両方にはなれない、というものです。これは特定の種類のデータ構造にとって障害になります。この本の前半では、その解決策を探っていきます。

そもそも型システムとは？

型システムは静的解析の一般的な形態であり、特定の種類の実行時エラーを排除できます。 この話題についての短い補足は、付録の 基礎: 型システム セクションを参照してください。

まとめ

Rust のコンパイラは、メモリ安全性の性質を検証するためのファーストパーティの静的解析を提供します。 これは、Rust プログラムをビルドするたびに得られる、無料で即時の、そして大きな保証価値の追加です。

高価な製品（たとえば複雑なコード解析ツール）や、スケールしにくい専門家プロセス（たとえば熟練したセキュリティエンジニアによるベストエフォートのコードレビュー）に頼る必要はありません。 それは［ほとんどの場合］「ただ動く」のです。 保証は反復可能なデフォルトになります。

これらの保証は主に、「所有権」という新しい概念を導入する Rust の型システムの産物です。 その仕組みはメモリモデルとエイリアシングの複雑さを克服し、特定の正しさの概念を証明できるようにします。 所有権がどのように機能するかについては、第3章で詳しく掘り下げます。

動的解析に進み、最初の Rust プログラムを書き始めましょう。

形式検証のための基礎

Rust の型システムは、形式検証研究に重要な意味を持ちます。 具体的には、共有された可変状態が存在しないため、この言語は一階述語論理⁹を使う検証技法に適しています。

一階述語論理は、学部課程の離散数学の授業で教えられます。 そうした授業は、コンピュータサイエンスのカリキュラムでは一般的です。 これは、実務エンジニアが Rust の演繹的検証ツールを使うために、分離論理（より新しく高度なトピック）を学ぶ必要がないかもしれない、ということを意味します。

第11章では、演繹的検証の初期プロトタイプを試します。 Rust の検証は、活発な学術研究の領域です。

1. 文脈の中のソフトウェア、Zach Tellman とともに。Zach Tellman、Adam Gordon Bell（2019）。 ↩

2. Memory Mapped Input/Output（MMIO）は、遠く離れた、一見ランダムなメモリ領域に大量のマジックバイトを書き込む必要がある文脈です。意外かもしれませんが、それはハードウェア周辺機器を制御する主要な方法の1つです。「データシート」（製造元が書いた公式のハードウェアマニュアル）には、どの特定のメモリアドレスにどのマジックバイトを書き込むべきかが記されています。これは、まさに生ポインタが必要で、危険など知ったことか、という類のものです！¹⁰。 ↩

3. Rust プログラミング言語の理解と進化（博士論文）。Ralf Jung（2020）。 ↩

4. Rust の Unsafe が機能する理由。jam1garner（2020）。 ↩

5. Pin における不健全性。comex（2019）。Rust コンパイラは人間によって書かれ、保守されていることを忘れないでください。ここにリンクした Pin の問題のように、時にはバグもあります。繰り返しますが、絶対的なセキュリティなど存在しません。Rust の型システムの形式検証は、頻繁に変更されるコンパイラのコードベース全体にバグがないことの検証を意味するわけではありません！ ↩

6. totally_safe_transmuteの行ごとの解説. William Woodruff (2021). このブログ記事では、transmutation（ある型のビットを別の型として再解釈すること）のための型破りなトリックを詳しく説明しています。このトリックでは、プログラムがOS機能を使って、Rustコンパイラが想定しておらず、想定しようもない方法で、実行時に自身のコードを変更します。そのため、コンパイラにとっては「安全」ですが、実際には極めて安全ではありません。これはRustの安全性保証が破られているという意味ではなく、型システムがプログラムの実行環境のあらゆる側面をモデル化できるわけではない、というだけです。また、そうすべきでもありません。現実世界のほとんどのプログラムは、実行時にメモリ上の自身の表現を書き換えたりしません。 ↩

7. コンピュータ科学者がプログラミング言語 Rust の安全性主張を証明。Saarland University（2021）。Rust の形式検証は、現在の成功と継続中の取り組みの両方を伴う研究課題であることに注意してください。 ↩

8. アフィン型システム. Wikipedia (Accessed 2022). ↩

9. RustHorn: CHCベースのRustプログラム検証. Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi (2020). ↩

10. tock-registers. Tock Project Developers (2021). このプロジェクトは、カスタマイズ可能な型の形で安全なMMIO抽象化を提供します。生ポインタの代替として確認する価値があります。 ↩