「The Challenge of Using C in Safety-Critical Applications」を雑に読む - 低レイヤ強くなりたい組込み屋さんのブログ

The Challenge of Using C in Safety-Critical Applicationsというwhite paperを雑に読んでみます。

このwhite paperは、C言語でsafety-criticalなシステムを作ることが、いかに難しいかを述べています。

white paper内で参照しているコードは、下記のレポジトリで公開されています。

white paper内で静的解析ツールで検出できなかった4つのケースのうち、1つは、PCLintとCoverityでは正しく検出できることがissue #2で報告されています。

Abstract

safety-criticalなシステムにおいて、未定義動作や予期せぬ停止をするようなプログラミング言語 (C言語) が使われ続けています。プログラミング言語の欠陥を埋めるために、MISRA-Cのようなサブセットが定義されていますが、実行時の安全性を保証するには、結局のところ不十分です。

Introduction

safety-criticalなシステムを構築するにあたり、ソフトウェアエラーを開発プロセスの早い段階で検出する戦略が必要です。そのような戦略のうち、設計ドキュメントと定期的なコード検査が、今日のソフトウェア開発プロセスでは一般的ですが、ソフトウェア実装と同様にヒューマンエラーという脆弱性の影響を受けます。静的解析は、危険なコードパターンを自動で検出することで、この問題を緩和します。

Background

safety-criticalシステムでは、C言語があらゆる場所で使われています。これは、性能やフットプリント、コンパイラサポートなど、多くの理由があります。

2010 ISO/IEC 9899:2011の草案では、C言語の200個近い未定義動作について詳述しています。未定義動作を減らすために、CERT CやMISRA-Cのようなサブセットが定義されています。

このwhite paperでは、このようなサブセットがC言語にとって意味のあるものになっているかどうか検証するために、一般的な実行時エラーについて調査します。

Methods

MISRA-C基準とCの静的解析ツールの有効性を評価するため、C言語の4つの危険な動作を選択しています。

複数の可変参照
不変データの修正
曖昧なパターンマッチ
データ競合

その後、MISRA-Cガイドラインといくつかの静的解析ツールを適用し、その有効性を評価します。静的解析ツールには、以下のツールを利用します。

Cppcheck
Flawfinder
Flint++
Frama-C
OCLint
scan-build
splint
Vera++

訳注：全て、OSSの静的解析ツールです。製品使うと、色々問題があるのでしょう。

可変参照

複数の可変参照があると、気づかずに無効な参照を使うリスクが常にあります。 MISRA-Cでは、実行時のNULLポインタチェックを要求しています。静的解析ツールは、NULLポインタの参照外しに対しては、よく機能します。しかし、他のデータ破壊については、あまり検出しません。

MISRA-Cおよび静的解析で検出できない例の、簡略化バージョンです。

typedef struct {
    int32_t x;
    int32_t y;
    int32_t z;
} example_s;

/* Example data. */
example_s a = {
    .x = 1,
    .y = 2,
    .z = 3
};

/* Mutable reference. */
example_s * b = &a;
/* Mutable alias. */
example_s ** c = &b;
/* Reference corrupted. */
*c += 2048;
/* Use after corruption. */
b->y = 4;
b->x = 5;
b->z = 6;

破壊された参照の利用は、未定義動作を引き起こします。大抵の場合、セグメンテーションフォールトになります。

`const`外し

訳注：この例は、PCLintおよびCoverityでは検出できる、という報告がissueにあがっています

基本的には、上述の可変参照のケースと同じです。今回は、constの契約を破ります。

/* Example data. */
example_s a = {
    .x = 1,
    .y = 2,
    .z = 3
};

/* Constant reference to
* example data.
*/
const example_s const * b = &a;
/* Constant alias to reference. */
const example_s * const * c = &b;
/* Cast away const to corrupt
* reference. */
*((example_s **)(c)) += 2048;
/* Use reference after
* corruption. */
int32_t sum = b->x + b->y + b->z;

信頼できないパターンマッチ

C言語では、列挙体の誤使用についての保護機能がありません。 C言語のenumは、定数のintと区別ができないため、下の例では、関係のない値とマッチングしてしまいます。

/* Enumeration intended for use. */
typedef enum {
APPLY_BRAKE = 1,
APPLY_THROTTLE = 2
} action_e;
/* Ambiguous enumeration. */
enum {
SELF_DESTRUCT = 2,
};
/* Example data. */
example_s a = {
    .x = 1,
    .y = 2,
    .z = 3
};
/* Mutable reference. */
example_s * b = &a;
/* Mutable alias. */
example_s ** c = &b;
/* Intended use as an 'action_e'
* enum type.
*/
action_e t = APPLY_THROTTLE;
/* Match on integer instead. */
switch (t)
{
    /* Wrong pattern. */
    case SELF_DESTRUCT: {
        *c += 2048; break;
    }
    default: { break; }
}
/* Use after corruption. */
b->y = 4;
b->x = 5;
b->z = 6;

データ競合

bが共有リソースの場合、b->xへの書き込みは、破壊された参照への書き込みである可能性があります。

/* Arbitrary bound. */
while ((b != NULL) && (b->x < 10))
{
    /* Simulate some amount of
    * work.
    */
    (void)sleep(0);

    /* If another thread has
    * changed the shared resource.
    */
    if (b->a >= 10)
    {
        b += 2048;
    }
    else
    {
        /* Increment potentially
        * corrupted reference.
        */
        b->x += 1;
    }
}

結局のところ、共有の参照を破壊するコードが1箇所あると、C言語では未定義動作に繋がってしまいます。これを、C言語の静的解析で検出することは、困難です。

別のアプローチ

安全性を保証するために、他の言語を調査しました。このwhite paperでは、Rustを選びました。

ここまでのC言語と同様のコードを、Rustで書くとどうなるか、を見ていきます。

安全な参照

下の例はコンパイルできません。Rustの借用と所有権のコンセプトが守ってくれます。所有権を持っていないデータを破壊することはできません。

struct Example {
    x: i32,
    y: i32,
    z: i32,
}
let mut a: Example = Example { x: 1, y: 2, z: 3 };
let mut b: Box<&Example> = Box::new(&mut a);
let _c: Box<&&Example> = Box::new(&mut b);
drop(**c);
//~^ ERROR cannot move out of borrowed content
b.x = 4;
//~^ ERROR cannot assign to `b.x` because it is borrowed
b.y = 5;
//~^ ERROR cannot assign to `b.y` because it is borrowed
b.z = 6;
//~^ ERROR cannot assign to `b.z` because it is borrowed

不変性の保証

下の例はコンパイルエラーになります。不変データを変更しようとするからです。 Rustでは、不変性を簡単には破ることができません。

let mut a: Example = Example { x: 1, y: 2, z: 3 };
let mut b: Box<&Example> = Box::new(&mut a);
let c: Box<&&Example> = Box::new(&mut b);
// Attempt to corrupt referenced data
drop(*(&mut(**c)));
//~^ ERROR cannot borrow immutable `Box` content `*c` as mutable
b.x = 4;
//~^ ERROR cannot assign to field `b.x` of immutable binding
b.y = 5;
//~^ ERROR cannot assign to field `b.y` of immutable binding
b.z = 6;
//~^ ERROR cannot assign to field `b.y` of immutable binding

信頼できるパターンマッチ

下のプログラムはコンパイルエラーになります。 Rustは曖昧なenumを許容していません。また、Rustはデフォルトでは他の型のパターンマッチを許しません。

// Enumeration intended for use.
enum Action {
    ApplyBrake = 1,
    ApplyThrottle = 2,
}
// Second enumeration.
enum Destruct {
    SelfDestruct = 1,
}
let pattern = Action::ApplyThrottle;
match pattern {
    Destruct::SelfDestruct =>
    //~^ ERROR mismatched types
    {
        panic!("Memory corrupted.")
    }
}

データ競合の保護

サンプルコードを2つ示します。 1つは、Cの例を、愚直に実装しようとしたものです。下のコードは、Rustコンパイラによって多くのエラーが報告されます。これはRustのムーブセマンティクスのコンセプトによるものです。

訳注：bはBoxのインスタンスで、複数のスレッド関数にbを渡そうとした、と考えて下さい。ムーブセマンティクスにより、bの利用はエラーになります。

while b.x < 10 {
//~^ ERROR use of moved value: `b.x`
    thread::sleep(time::Duration::from_secs(0));
    if b.x >= 10 {
    //~^ ERROR use of moved value:
    // `b.x`
        drop(b);
        //~^ ERROR use of moved value: `b`
    }
    b.x = b.x + 1;
    //~^ ERROR use of moved value:
    // `*b`
}

次に、スレッド間でデータを共有する場合に、Rustコンパイラが要求することについて見ていきます。

let a: Example =
Example {
    x: 1, y: 2, z: 3
};
let b: Box<&mut Example> = Box::new(&mut a);
//~^ ERROR `a` does not live long enough
for _ in 0..thread_count {
    handles.push(Some(thread::spawn(|| { black_box(b)})));
    //~^ ERROR capture of moved value: `b`
}

spawn()関数は、Rustがライフタイムと呼ぶ制約を持っています。 spawn()の引数（クロージャ）は、「プログラム実行の間中、ライフタイムを持つ必要があります」。ここでは、関数内のローカルデータを参照しているため、spawnしたスレッドが、関数スコープより長く存在した場合、ローカルデータへの参照は無効になります。

次に、可変参照は常に唯一である必要があります。上記例の参照は、ループの1回目で、スレッドにムーブされる必要があります。これまでに見た借用ではなく、所有権を完全に移譲する必要があります。次のイテレーションでは、既に所有権を失っているため、渡せるものが何もありません。

最後に

一通り読んでみました。やはり、強力な型システム、所有権、借用、ライフタイム、による安全性という観点に行きつくのだなぁ、という感想です。