Cを安全なRustへコンパイルするための形式化された方法

• Cを安全なRustへコンパイルする

• Rust言語の人気は急速に高まっている一方、多くの重要なコードベースは依然としてCで書かれており、手作業で書き換えるのは現実的ではない。したがって、CをRustに自動変換することが魅力的な代替案として浮上している。

• 既存のさまざまな研究では、Rustの複数の機能（例：unsafe）を使ってCの扱う範囲を拡大する方向に進んでいる。しかし、 自動化の可能性は魅力的であるが、unsafeに依存するコードを生成すると、Rustが提供するメモリ安全性の保証が失効し、既存のコードベースをメモリ安全な言語へ移植する主要な利点がなくなる。

• 我々は異なるアプローチを模索し、Cを安全なRustへ翻訳する方法を研究した。つまり、Rustの型システムに準拠して、メモリ安全性を容易に保証できるコードを生成することである。

• 我々の研究は複数の独自の貢献を含む。

  • Cの一部を安全なRustへ型主導で翻訳する
  • Rustのスライスとスライス演算を用いてCのポインタ算術を表現するための「分割木」に基づく新しい静的解析
  • どの借用が可変であるべきかを正確に推論する解析
  • Rustの非所有・所有アロケーションの区別と互換性のあるC構造体型に対するコンパイル戦略

• 我々はこの方法論を既に形式的に検証されたCコードベースに適用した：HACL*暗号ライブラリ、EverParseのバイナリパーサおよびシリアライザ。サポートするCのサブセットで、これら2つのアプリケーションを安全なRustへ翻訳するのに十分であることを示した。

• 評価結果、Rustのエイリアス規則を逸脱するいくつかの部分については、自動化された外科的リライトで十分であり、挿入した戦略的なコピーが性能に与える影響はごくわずかであることを確認した。

• 特にHACL*に対してこのアプローチを適用した結果、現代のあらゆるアルゴリズムを実装する80,000行の検証済み暗号ライブラリが純粋なRustで実装された。これは初めての事例である。

[GN⁺]

Hacker Newsのコメント

• Rust へ移植する際にいくつかの結論に達した

  • C プログラムを Rust に変換すると、Rust の厳格な制約のおかげでバグを素早く発見できる
  • C から Rust への自動変換は、2 つの言語の設計が根本的に異なるため完全に解決できない問題がある
  • 場合によっては C から Rust へのポーティングが不可能なこともあり、これは設計そのものに内在する不安全性のためである
  • ツールの進化により、ポーティングの作業はさらに円滑になるだろう

• 形式的に検証された既存の C コードベースと、一般的なシステム向け C コードベースは異なる

• 研究者たちは 2002 年に安全な C 方言である Cyclone に関する論文を発表し、C から Cyclone へ移植する際に安全性バグを発見した

  • こうした手動・自動変換は、安全な言語の採用を増やし、既存バグを発見する可能性がある

• Rust への単純な変換は安全な部分と不安全な部分を生み出し、手作業は不安全な領域の安全性検証に集中できる

  • 不安全な部分が大きくても、メリットはあり得る

• C の一部だけをコンパイルするアプローチには低い期待しか持てない

  • Rust の所有権モデルが実際の C プログラムと大きく異なるため

• Zig の C 変換機能との比較に対する疑問

  • Zig は新規コードと既存の C コードを混在させた環境をよく生成でき、C コンパイラとしても使える
  • Linux カーネルのメンテナが Zig を C の代替として検討していない理由への疑問

• C2Rust が形式的に正しいコードを生成できるかどうかへの問い

  • Rust コードを生成するソースへのリンクが見当たらない

• C ライブラリが正常に動作しているなら、Rust の不安全性を使って移植する価値があるかもしれない

  • Rust は一般的にライブラリが不足している

• 高い最適化レベルが Rust の速度を大きく向上させなかった点が興味深い

  • O3 最適化レベルで C を Rust に一度でコンパイルした場合に、どれほどうまく機能するか疑問