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

 (arxiv.org)
2 ポイント 投稿者 GN⁺ 2024-12-22 | 1件のコメント | WhatsAppで共有
  • Scyllaは既存のCをいったんunsafe Rustへ移してから修正するのではなく、元のCを段階的に構造化し、安全なRustへ直接コンパイルできる経路を提案している
  • 対象は、データ処理、ポインタ演算、構造化された制御フロー、移植可能なコードを含むapplicative Cの部分集合であり、goto、整数-ポインタキャスト、ポインタトリック、ビットフィールド、untagged unionに依存するコードは除外される
  • 変換は、Clang ASTをMini-Cへ落としてからsafe Rustへ移す2段階で、整数昇格・暗黙変換・代入式・前置/後置インクリメントのようなCの微妙な挙動を明示化する
  • 最も厄介なポインタ算術は、Rustのsliceとsplit_at_mut/split_atベースの分割へ置き換え、可変性推論、トレイト導出、Boxとborrowの選択もあわせて処理する
  • Windows SymCrypt、HACL★、bzip2の中核圧縮アルゴリズム、EverParseのCBORパーサ/シリアライザ、Microsoft FrodoKEMの一部を評価し、変換中にbzip2とFrodoKEMのundefined behaviorも発見した

Scyllaが選んだC→Rust移行パス

  • 既存CコードをRustへ移行しようとする動機は、メモリ安全性の問題から出発している
    • GoogleとMicrosoftの研究では、セキュリティ脆弱性の70%が不適切なメモリ処理に関連すると推定している
    • 企業や政府は、安全性が重要なシステムにRustのようなメモリ安全言語を使うことを推奨している
  • Rustは新規コードには明確な利点があるが、すでにテスト・デバッグ済みの産業用Cコード全体を書き直すのは難しい
  • 既存のC→Rust自動変換ツールは、C全体をサポートするために概してunsafe Rustを出力する
    • unchecked pointerやRustのtransmutationのようなC的イディオムを許容する
    • 静的なメモリ安全保証が失われ、安全な言語を使う目的が弱まる
  • 一般的なワークフローは、unsafe Rustの出力物を出発点にして、その後で安全なRustへ反復的にリファクタリングする方式である
    • raw pointerをsafe Rustのborrowへ置き換えたり、低レベル表現からRustの抽象化を復元したりする静的解析が提案されている
    • リファクタリングツールは散在しており、c2rust refactorのサポートも2022年に終了した
  • Scyllaは生成済みのunsafe Rustを修正する代わりに、元のCコード自体を段階的に構造化し、safe Rustへコンパイル可能にする方式を採る

サポートするCの部分集合と除外されるパターン

  • Scyllaの目標は、予測可能な変換と、元のCに近いRustコードの生成である
  • 対象はapplicative Cの部分集合である
    • データを操作・処理するコード
    • ポインタ算術を使うコード
    • 構造化された制御フローを持つコード
    • 移植可能なコード
  • 次のパターンに依存するコードベースはサポートしない
    • goto
    • 整数-ポインタキャストによるオブジェクト表現の利用
    • ポインタトリック
    • ビットフィールド
    • untagged union
  • 開発者は、Scyllaが理解できるようにCソースへターゲットを絞ったリライトとアノテーションを適用できる
    • Rustのborrow checkerと噛み合わないaliasingパターンを書き換えられる
    • tagged unionを高水準ADTへ翻訳すべきだという情報をScyllaへ与えられる

Mini-C: Cの曖昧さを減らす中間言語

  • ScyllaはClangフロントエンドのASTから出発し、まずMini-Cという言語へ変換する
  • Mini-CはCのように分岐、ループ、ポインタ、デリファレンス、アドレス取得を扱うが、“no-surprises”な意味論を持つ
    • すべての整数は固定幅を持つ
    • Cのinteger promotionとinteger conversionは明示的なcastで表現される
    • void *のようなuntyped pointerは許されない
  • Mini-CはCと異なり式言語である
    • 代入は値を返さない
    • e1 = e2 = e3、p[i++]のようなC構文はMini-Cでdesugarされる
    • ループや条件文のテスト式は、Cのintではなくbool型でなければならない
  • Clangのtyped ASTをMini-Cのtyped ASTへ移しながら、Cの暗黙的な挙動を明示化する
    • 条件式はboolへ揃える
    • 配列インデックスはsize_tへ揃える
    • 関数呼び出し引数や代入右辺の暗黙変換を明示的なcastへ変える
    • 算術演算ではC標準のusual arithmetic conversionsを反映する
  • 変換は、Cコードが移植可能であり、Cのデータモデルに依存しないと仮定する
    • たとえばlongが4バイトか8バイトかで動作が変わるコードは想定しない
    • 実装ではconfigure時に対象アーキテクチャのデータモデルを検出し、unsigned intをuint32_tのような固定幅型へ変換する

ADTとタプル合成

  • Mini-CはCより高水準のADT、tuple、pattern matchingを提供する
  • tagged unionはアノテーションによってADTへ翻訳される
    • 対象の形は{ int tag; union { t0 case0; ...; tn caseN }}のような構造である
    • tag値は0からNまでで、tag値はunion caseの順序と一致すると仮定する
  • Scyllaは、アノテーション付きtagged union型をvariant型へ変換する
    • 値の生成時に.tag = iと.casej = eが一致するかを検査する
    • 一致すれば対応するconstructor値へ変換する
    • payloadとtagが合わなければMini-Cへ翻訳しない
  • tagged unionのフィールドアクセスは、現在のtag状態を知っていなければ安全でない
    • if (x.tag == i) { ... x.casei }やswitchのようなパターンを認識する
    • これをmatch x with | Ci v -> ...の形へ変換する
    • それ以外のunion caseへのアクセスはinvalidと見なし、変換エラーにする
  • tupleもアノテーションによって合成できる
    • n個のフィールドを持つstructはn-ary tupleへ変換される
    • フィールドアクセスはtuple field accessへ変わる
    • tupleは構造的に型が決まり、mut-polymorphismの利点を得られる

Mini-Cからsafe Rustへの変換

  • Mini-Cは型アノテーションが完全なCプログラム表現を提供し、その後safe Rustへ変換される
  • 主な難点は3つある
    • Cのポインタ算術の除去
    • 可変性とaliasingの明示化
    • トレイトのようなRust慣用の構造の自動付与
  • ポインタ型の変換は、Rustのポインタ表現の違いのため複雑である
    • RustはBox<T>と&Tを区別する
    • 単一要素へのポインタと複数要素へのポインタも&Tと&[T]のように区別する
    • Rustの配列は値であり、Cのように自動でポインタへdecayしない
  • 基本戦略は、Cのすべてのpointer typeをRustのslice borrow &[T]へコンパイルすることだ
    • スタックポインタとヒープポインタの両方が、基本的にはslice borrowになる
    • 単一要素と複数要素へのポインタも、基本的にはslice borrowになる
    • 可変性は別の段階で自動推論する
  • Scyllaはヒューリスティクスと手動アノテーションによって、一部のポインタをBox<T>へ翻訳する
    • グローバル参照がなくfresh allocationだと判断されるT *create()のような関数は、fn create() -> Box<T>へ翻訳できる
    • この解析はstructやvariant定義の内部まで不動点方式で再帰的に適用される
    • borrowが残るstructはlifetime parameterを持つようになる

Box、slice、array変換の制約

  • Rustではarray、slice borrow、Boxの間に明示的な変換が必要なため、ScyllaのRust変換も型指向で動作する
  • 変換規則は、arrayやboxed sliceをslice borrowへ変えるcoercionを挿入する
    • arrayは&x[..]のような形でslice borrowになる
    • boxed sliceはborrowへ変換できる
  • 逆方向の変換も可能である
    • sliceやarrayをヒープ確保へ昇格させてBox<[T]>へ変えられる
  • この逆方向変換はコピー意味論の差を生むことがある
    • Cではarrayとpointerが同じメモリを指せる
    • RustでBox::new(x)はxのコピーを作ることがある
    • 整数配列のような基本型配列はCopy traitをopt outする方法がないため、Rustが黙ってコピーを行うことがある
  • Scyllaは、このような変換が起きた場合、元の変数を環境から除去して以後の利用を禁止する
    • 元のCプログラムがその変数を使い続けると、変換エラーになる
    • 開発者は変換前にCソースコードを修正し、意図をより明確にする必要がある

ポインタ算術をRustのslice分割へ置き換える

  • Cプログラムは配列を単一のbase pointerだけでアクセスするのではなく、配列をchunkに分割したり、現在位置のポインタを保持しながら走査したりするパターンをよく使う
  • Rustは任意のポインタ算術を許さず、split_at_mutまたはsplit_atでsliceを分割する方式を提供する
    • split_at_mutは元のsliceの所有を手放して2つのsub-sliceを得るprimitiveである
    • mutable dataは一意のownerを持たなければならないというRustのinvariantを保つ
  • Scyllaは、Cのポインタ算術をRustの分割方式へ合わせるためにsplit treeを導入する
    • 各C pointerは1つのsplit treeへマッピングされる
    • split treeはflow-dependentに変化する
    • 特定のプログラム地点で、CのポインタアクセスをどのRust sliceアクセスへ置き換えるべきかを追跡する
  • Cポインタには長さ情報がないため、Scyllaはchunk同士が重ならないと仮定する
    • 重なりを意図しているならRustの型検査を通らず、開発者がCコードを書き直す必要がある
    • 変換は予測可能であるべきなので、backtrackingを避けてforward方式で行う
  • 例では32バイト配列abcdを4つの8バイトlimb領域へ分割する
    • Cではabcd + 0、abcd + 16、abcd + 8、abcd + 24のように、左から右の順ではないポインタ算術を使う
    • Rust変換ではsplit_at_mut呼び出しの履歴をsplit treeとして保持し、正しいsub-sliceをたどる

評価対象と発見されたundefined behavior

  • Scyllaの実装はClangを使って既存Cコードを入力し、safe Rustを出力する
  • 評価対象には、複数の既存Cプロジェクトの一部が含まれる
    • WindowsのSymCryptの一部
    • HACL★暗号ライブラリの一部
    • bzip2圧縮アルゴリズムの中核部分
    • EverParseライブラリのCBORバイナリパーサとシリアライザ
    • MicrosoftのFrodoKEMポスト量子暗号プリミティブ実装
  • これらの事例は、Scyllaのapplicative C部分集合が複数のセキュリティクリティカルなアプリケーションを含みうることを示している
  • 変換過程では、bzip2とFrodoKEMの元のCコードに存在するundefined behaviorも特定し、報告した

関連記事

1件のコメント

 
GN⁺ 2024-12-22
Hacker Newsのコメント

  • この取り組みは「すでに形式検証済みのCコードベース」を対象にしている点が重要
    一般的なシステムCコードは形式検証されていないので、かなり別の話になる

    • それでも完全に信頼できるわけではなさそう。論文の2.2節でも、変換規則が導入する強制が微妙な意味の違いを生む可能性があるとしている
      たとえば、スタック上のC配列を指していたポインタが、RustではBox<[u8]>として、新しいヒープコピーを所有するポインタのように翻訳されることがある。元のコードが、そのポインタが実際の配列を指しているという事実に依存していたなら、翻訳後のコードは黙って誤動作する可能性がある
      私のプロジェクトであるscpptoolの、メモリ安全なC++サブセットへの自動翻訳機能なら、配列を代替型とイテレータへ移して元の意味を保つ形で処理したはず
      OPのプロジェクトは、安全なRustに変えやすいCだけを扱っているのかもしれないが、問題の難しさを考えると成果は尊重に値するし、ある程度の有用性も見える
    • これは注意点がはるかに多く、ほとんど誇大広告に近い
      そもそも彼らは実際のCを翻訳したのではなく、Fで書かれたコードについて、Cコンパイラ側がRustを出力するように変えたもの。複雑な実際のCコードを相手にしたわけではなく、せいぜいおもちゃのコンパイラが吐きそうな制限付きのMini-Cを扱ったにすぎない
      原文でも、元のCプログラムがxにさらに依存していると翻訳がエラーを出し、プログラマにソース修正を求めるとしているが、これはCがすでにRustの借用チェッカーを満たすスタイルで書かれていることを期待しているという意味
      「図4には美しい規則を提示するが、実装は多数の小細工に依存している」という学術界風の表現に見える
      さらに悪いことに、静的に区別できる重なりはコンパイルエラーにし、そうでない場合はRustコードが実行時にパニックする可能性があるという。形式検証済みのCプログラムを「今度はクラッシュするかもしれない」Rustプログラムに変えるのは奇妙
      HACL      を既存の形式検証済みCコードベースと呼ぶのも不正確。HACLはCへコンパイルされるが、Cライブラリではなく、まったく別の言語で書かれている
      正直なタイトルは「F      のサブセットを部分的に安全なRustへコンパイルする、部分的に形式化済み」程度であるべきだった
    • Rust自体は形式検証されているのか？ 知る限りではそうではない
    • 形式検証済みCとは正確には何なのか、そしてなぜもっと多くないのか気になる
    • 核心的な違いが何なのか気になる。コンパイラフラグで準拠を強制できるのか？

  • 2002年に研究者たちは、Cの安全な方言であるCycloneの論文を発表し、CコードをCycloneへ手作業で移植する過程で既存Cコードの安全性バグを発見した
    この種の手動または自動のC変換は、より安全な言語の採用を増やすだけでなく、既存のバグを明らかにする潜在力もある
    [1] https://www.researchgate.net/profile/James-Cheney-2/publicat...

    • Cycloneはもはやサポートされておらず、中心となる研究プロジェクトも終了し、開発者たちも別の仕事へ移っている
      Cycloneの多くのアイデアはRustに取り込まれており、コードは努力すれば動かせるが、現代の64ビットプラットフォームではそのままではビルドできない
      http://cyclone.thelanguage.org

  • C2Rustを第一段階として使い、Cプロジェクトを含むいくつかのプロジェクトをRustへ移植してみて、いくつか結論を得た

    1. CプログラムをRustへ移すと、unsafeが含まれていても、Rustの強い制約、たとえば境界チェックや厳格なシグネチャのおかげで、バグが早く表面化することが多い
    2. 自動C→Rust変換が完全に解決されることはないと思う。Cプログラムの設計はRustと根本的に異なり、安全にするには相当な再設計が必要になる
    3. 場合によっては、正確な意味を保ったままCからRustへ移すことは不可能。安全でないことが設計そのものに内在している可能性があるため
      それでもツールは移植に不可欠であり、ツールが進歩するほどプロセスはより滑らかになるはず
    • 「高速で安全なRust」へ自動変換するのは難しいが、一般的な安全なRustへ自動変換するのはずっと簡単
      メモリを配列で表現し、ポインタをその配列のインデックスとして扱えばよい。そうすれば、チェックなしのポインタ演算やunionのようなCの動作を、借用チェッカーと戦わずに表現でき、意味も保たれる。C→Javaでも昔から似た手法が使われてきた
      もちろん、このような変換の価値は曖昧。実質的にはCをwasmへコンパイルしたのと似ているがより遅く、生成コードが技術的には「安全」だとしても、バッファオーバーフローが不正な状態を作ったり、ダングリングポインタが本来許されるべきでない文脈のデータアクセスを可能にしたりする問題は残る
    • 「安全でないことが設計に内在しうる」という話には原則として同意するし、自分の経験上も強くそう感じるが、議論を具体化する簡単な例があるとよい

  • 著者です。複数のスレッドで出た点をいくつか整理すると役に立ちそうです

    1. これは arxiv に載せた学術論文であって、C→Rust 問題を解決したと主張する新製品発表ではありません。PL 学会に投稿したもので、FOSDEM のようなオープンソースイベントでの発表とは聴衆も期待値も違います
    2. アプローチは単純です。C を安全な Rust に翻訳するという制約から出発し、うまく動作する小さな C の部分集合、スライス分割の推論、エラーを出せる翻訳、中断され得るプログラムなどが必要になる点を検討しています。F* 内に埋め込まれた C という、私たちが持つ対象について評価し、Firefox や Python などの主流ソフトウェアで使われる大規模な C ライブラリに対して、この制約下でかなりスケールすることを示しました。Firefox を自動的に Rust で書き直せると主張しているわけではありません
    3. 研究は本来こう進むものです。設計空間に興味深い点があると見ており、すべての問題を解決すると主張してはいませんが、C→Rust 翻訳分野のさらなる進展を開く可能性のあるアイデアだと考えています。既存のツールがこのアプローチを、部分集合に合うコードには使い、合わない部分は unsafe Rust にフォールバックすることもあり得ます
    4. これが最終版ではありません。実際の C フロントエンドを libclang で作っているところで、生成された Rust が範囲外アクセスを起こさないよう保証する方法も探っています。たとえば Z3 に検証条件を出力するような形を考えています。査読者がさらに作業が必要だと判断すれば、改善して再投稿すればよく、この分野が活発で、他の人がアイデアから助けを得られると判断して論文を採択してくれるなら、なお良いことです

  • 本当に気になるのは、なぜそうすべきなのかという点です
    産業用アプリを C から Rust に本当に変換できる技術なら、既存の C アプリをもっと簡単に堅牢化することもできそうです。静的解析器やテスト生成器のような既存ツールに入れる解析を作ればよいはずです
    同様に、安全なラッパーを生成して、検証済みの C の隣で新しいコードを Rust で書けるようにすることもできるでしょう。新しいコードは Rust の利点を得て、既存コードは安全だと確認され、インターフェースもより安全になります
    完全な翻訳器が理想的ではあるかもしれません。長期的にはコードベースの言語が一つである方がよいからです。しかし既存の C/C++ に対して、誤検知の少ないワンクリックの安全性確保こそ、依然として最も大きな必要性です。Google のコンパイラツールや ForAllSecure の Mayhem のように、C の中の悪い構造を自動修正することも可能かもしれません

    • 一部の C プログラムは安全にできないので、「産業用アプリを Rust に変換する技術なら C アプリをもっと簡単に堅牢化できる」という話は正しくありません
      未定義動作や未規定動作に依存しているからかもしれませんし、適切な安全性チェックを入れると許容可能な入力領域が狭くなりすぎて役に立たなくなるからかもしれません
      安全な言語に翻訳すれば、入力の表現力を保ちながら実行時に正しい動作を静的に保証できるため、このような場合には客観的により優れています
      「現場で実証済みの C」というものも、数多くの致命的脆弱性が示す通り、存在すると見るのは難しいです。実際にあるのは、十分な頻度でかなりうまく動き、有用に見える C にすぎません
      古いコードは運よく安全だと仮定されているだけで、証明されているわけではありません。「証明」には、特にこのような論文の文脈では特定の意味があり、圧倒的多数の C コードは厳密な数学的基準で証明されていません。一方で Rust の型システムは数学的に正しいことが証明されています
      全体翻訳器は、何を諦められるかに依存します。性能、入力領域、出力範囲、コードの可読性などを諦めてよいならある程度可能でしょうが、これらすべての面で健全かつ完全な翻訳器を求め始めると問題が起きます

  • 素朴に Rust へ翻訳すると、安全な部分と unsafe な部分が混ざるのでは？ そうすると手作業では unsafe 領域の安全性だけ確認すればよさそうです。最初から Rust を書くときと似ています
    成果物の 90% が unsafe でないなら、かなり得に見えます

    • 実際その通りです。誰かが OpenJPEG を c2rust で低レベルな unsafe Rust に変換してみたことがあります
      OpenJPEG は特定のテストケースでセグフォールトすることが知られていて、そのテストを Rust 版で走らせると、同じ位置に相当する Rust コードでセグフォールトしました。少なくとも互換性はあったわけです
      しかしそのアプローチは行き止まりです。前進するには、翻訳器が C の一般的なイディオムを認識し、対象言語の自然な形へ引き上げる必要があります。Rust に「コンパイル」すると、安全でない C 風のポインタ操作関数呼び出しだらけのひどい Rust が生成されます
      最大の昇格問題は、ほとんどがポインタに関係しています。この論文の最も有望な成果は、C のポインタ算術を Rust のスライスに置き換える方法を見つけた点です。スライスは C のポインタ算術が行うことの大半を実現でき、いまや誰かがその翻訳を自動化したわけです。翻訳できないポインタ算術は非常に疑って見るべきです
      C で配列を指す生ポインタには、暗黙に長さが付いていると考えると有用です。その長さは C ソースには現れませんが、プログラム状態の関数としてどこかには存在します。定数かもしれませんし、malloc の要求サイズかもしれませんし、関数パラメータかもしれません。保守プログラマが配列長を見つけるのは、通常それほど難しくありません
      これは LLM に向いた問題かもしれません。「このコードを見て、配列 foo の長さが何かを見つけよ」と尋ね、その後、LLM ではない翻訳器に Rust への変換を誘導させる形です。LLM が間違えれば Rust はインデックスエラーを出すか、大きすぎる配列を持つことになりますが、安全でなくはなりません。C の配列サイズ情報のイディオムは十分に定型化されているので、ほとんど当てられるはずです。特に LLM はコメントも読めます
    • 素朴な翻訳では、ほぼすべてが unsafe な Rust コードになるでしょう。参照の代わりに生ポインタを至るところで使うことになるからです
      C コードは Rust のエイリアスモデルや借用チェッカーの制約を念頭に置いて書かれていないため、参照に翻訳するのは難しいです

  • ごく小さな C のサブセットをコンパイルしているだけ。実際には役に立たないほど小さい可能性もある
    この手のアプローチにはあまり期待していない。C コードの静的解析で可能な限界には必ずぶつかるはず。さらに Rust をターゲットに選んだせいで、問題が不必要に難しくなっている。Rust の所有権モデルは、実際の C プログラムの動作方式とあまりに違う

    • Rust の 所有権モデルは C の翻訳に十分近い。より明示的で強い型を持つだけなので、翻訳器が自由度の高い C コードが何をしようとしているのかを把握し、Rust の慣用句にマッピングする必要がある
      たとえば C のバッファには当然長さがあるが、C では長さがポインタに明示的に結び付いていない。そのため翻訳器は、C プログラムが長さをどう追跡しているかを推論し、スライスに変換しなければならない。長さが明示的な変数であっても簡単ではなく、計算されていたり、「末尾の次を指すポインタ」の形で表現が変わっていたりすると、さらに厄介になる
      bool should_free_this_pointer のような C のパターンも Rust の Owned/Borrowed enum に移せるが、どの割り当てがどのブール値と結び付いているのか、借用側のバリアントの本当の安全範囲がどこなのかを推論する必要がある
    • インターフェース言語としては良いかもしれない。バインディングに有用
    • 結局、人々は LLM を投入して、もっともらしく合っているコードを大量に幻覚しても構わないと言い出しそう
      それでも任意の C から慣用的な Rust を作るのは難しい、という点には同意する。いわば「だいたい合っている」程度になるだろう

  • これが Zig の C 変換機能とどう比較されるのか気になる
    Zig は、新しいコードは Zig で、古いコードは C のままにする混在環境を作り、変換や相互運用を行い、C コンパイラの役割まで果たすのに優れているように見える
    Linux カーネルのメンテナが Rust ではなく Zig を C の代替として見ていないのには、非常に良い理由があるのだろう。推測できるほど詳しくないので、もっと詳しい人が説明してくれるとうれしい

    • Rust は「C の代替」というより、C に追加されるツールだ。Torvalds らが価値を認めてカーネルに許可したツールであり、カーネルコードの大部分は引き続き C で書かれるはず
      カーネルメンテナではないが、Rust が Zig より選ばれた大きな理由を二つ推測すると、言語が提供する コンパイル時保証がより優れていて、採用の速度も速いからかもしれない
      業界の主要企業は、API 向けの Rust ネイティブコードや、メンテナンスされる Rust バインディングを提供しようと多くの取り組みをしている。Windows 開発者も自分たちのカーネルの一部を Rust で書き直している。かなり長く続いている流れがあり、止まらないことを願っている
      メンテナたちは、Zig が C に対して十分な利点をもたらさないと感じているのかもしれない。彼らの多くは、まだ Rust にも反対している
    • 私の理解では、ほとんどのカーネルメンテナは C を何かに置き換えようとはしていない
      Zig は Rust より C との相互運用性がはるかに高いが、メモリ安全ではなく、安定化もされていない。C の世界で Zig の採用はかなり増えるだろうが、Rust と直接競合しているとは見なしにくい
      私の地域では誰も Rust を採用しておらず、C++ の人たちは C++ に留まっている。最初は Rust に多少関心があったが、私の知るどの会社にも定着しなかった。Go が若い会社で大きく伸びた一方、伝統的な Java/C# 企業にはあまり入っていけないのと似た理由かもしれない。技術的に筋が通っていても、巨大な変更管理の課題だからだ
      Zig は動的メモリ割り当てを必要としないプログラムの方面で勢いを得ているが、それ以上はあまりない
    • Zig はまだカーネルで検討されるほど成熟していない
      いまも定期的に破壊的変更があり、現在の Zig にとっては良いことだが、Linux のように巨大で長寿命のコードベースには良くない。コンパイラバグも起きる
      Zig の方向性を概ね好んでいる立場で言っている
    • Zig はまだ 1.0 ではなく、後方互換性の保証がまったくない。ほとんどどこでも使われておらず、一部が有望に見えても、まだ価値を証明していない
    • Zig が メモリ安全ではないからかもしれない

  • C2Rust のようなツールがこれを利用して、形式的に正しいコードを生成できるのか気になる
    また、著者たちがどれくらい手作業をしたのか、それとも何かを走らせて Rust コードを生成したのかも気になる。そうだとすれば、Rust を生成するコードがどこにあるのか分からないし、ソースリポジトリへのリンクも見当たらない

    • 論文には、レビュー過程が終わった後、つまり概ね論文が正式に出版された後に、この開発成果物を オープンソースライセンスで公開すると書かれている

  • C ライブラリが動作するなら、つまり問題がないと形式的に証明されたわけではないが、たいていはうまく動くのなら、なぜ unsafe Rust を使って翻訳しないのか気になる
    Rust は全般的にライブラリが不足しているので、価値はあると思う。結局、状況によっては安全でない可能性のある C で書かれた dll/so を使うのと大きくは変わらない