LLVMを拡張してメモリ空間安全性をCで実現するChecked C

Checked CはMicrosoft Researchの主導による、オープンでコラボレーティブなプロジェクトである。C言語を拡張して、バッファオーバーランや領域外メモリアクセス、不正な型キャストといったエラーのない、信頼性の高いプログラムを記述できるようにすることを目標とする。移植を容易にするため、Checked Cコードでは、標準Cで記述されたコードとの共存を可能にしている。

IEEE Cybersecurity Development Conference 2018に間もなく掲載予定の記事に、同言語を開発する研究者たちによるChecked Cの主な機能とメリットが紹介されている。

Checked Cは既存のsafe-Cでの取り組みから多くのアイデアを借用していますが、決定的に違うのは、コントロールと相互運用性、ハイパフォーマンスのバランスを取りながら、インクリメンタルな変換を可能にすることを重視している点です。

この言語では、後方互換性に重点を置くと同時に、静的および動的アクセスを確実に検証するため、チェックポインタの概念を導入している。Checked Cが特に目標としているのは、メモリアクセスの空間的安全の確保である。そのためにポインタは、常にアロケートされたメモリ内のみを参照するようになっている。Checked Cの設計には、次のような3つの重点がある。

• C言語のポインタ表現は保持されているため、Checked CのメモリレイアウトはCと同じである。これにより、既存のCコードベースやライブラリとの相互運用性は容易に実現する。
• ポインタに割り当てられたメモリチャンクのバウンダリを明示的に指定することにより、コンパイル時および実行時のオーバヘッドは最小化されている。
• チェック済み領域(checked region)とバウンダリセーフなインターフェースにより、Checked Cと従来のC言語とのコードの混在が可能である。完全に移植されたコードはチェック済み領域に格納され、すべてのポインタアクセスにメモリ空間違反のないことが保証される。チェック済みコードは、バウンダリセーフなアノテーションを通じることで、コードパラメータや戻り値、関数、レコード型、グローバル変数といった安全でないCコードにアクセスできる。

Checked CではC言語に、_Ptr<T>と_Array_ptr<T>という２つの新しいポインタ型を加えている。前者がデータ参照でのみ使用されるのに対して、後者はポインタ演算をサポートする。いずれのポインタも、参照先の有効性をコンパイラが動的に保証する。以下に示すのは、2つの_Array_ptr<T>を引数として取る関数の定義である。

void append(
  _Array_ptr<char> dst : count(dst_count),
  _Array_ptr<char> src : count(src_count),
  size_t dst_count, size_t src_count)
{
  _Dynamic_check(src_count <= dst_count);
  for (size_t i = 0; i < src_count; i++) {
    if (src[i] == ’＼0’) {
      break;
     }
    dst[i] = src[i];
  }
}

配列を定義する時には、_Checkedキーワードを使って境界チェックを指定することができる。

int buf _Checked[10]

同言語の開発者によると、チェック機能を持ったポインタと配列を使うように既存Cコードを変換する場合には、比較的多くのコード変更が必要になり、ラインの17.5パーセントが影響を受けるという。これを改善するためにチームは、変換を自動化するツールの開発に取り組んでいる。興味深いのは、空間安全性に対する違反がチェック領域外からのものであることを証明可能にするために、部分的な形式化を行っていることだ。この方面での研究がさらに進めば、証明の対象を動的に確保される配列にまで拡張する予定である。

最後に注意すべき点として、予備的に実施されたベンチマークでは、チェックによって平均8.6パーセントの実行時オーバーヘッドが加えられていた。Checked CはLLVMのエクステンションとして実装されており、こちらからダウンロード可能である。