SALとソースコード解析

マイクロソフト C コンパイラーによるソースコード静的解析

Microsoft Windows SDK に付属の C コンパイラー (cl.exe) ではソースコードの静的解析機能が利用できます。
コンパイラーの起動オプションに /analyze を追加すると、バッファの境界検査や書式文字列とそのパラメーター引数の一致検査などが実行され脆弱性の原因となるソースコード位置を列挙してくれます。
たとえば次のソースコード test.c を解析するには SDK のコマンドラインシェルに cl.exe /analyze /c test.c と入力します。

/* test.c -- for demonstrate /analyze compiler option */
#include <stdio.h>

static char g_buf[10];

char test(size_t i)
{
  if(i >= 10)
    fprintf_s(stderr, "out of range");
  return g_buf[i];
}

この test.c を解析すると次のように警告が出力されます。

warning C6385: Invalid data: accessing 'g_buf', the readable size is 
'10' bytes, but '11' bytes might be read: Lines: 8, 9, 10

関数 test は引数 i の値が境界外の場合にエラーメッセージを出力するものの、 i の値によらず g_buf の i 番目の要素にアクセスするところに問題があることを警告してくれるのです。

なお Visual Studio (IDE) でも、「プロジェクトのプロパティ」を開き「構成プロパティ | C/C++ | コマンドライン」の「追加のオプション」に /analyze を追加することで静的解析機能を利用できます。

コンパイルオプションを設定するだけで利用できるので、ぜひ開発環境の設定に組み込んで開発の一助にしてほしいものです。

マイクロソフト C コンパイラーによる SAL 注釈

マイクロソフト C コンパイラーのソースコード静的解析は SAL (Microsoft Standard Sourecode Annotation Language, SAL Annotations) による注釈 (annotation) にもとづいて実行されています。
バッファの境界検査が主目的ですが、書式文字列とパラメーター引数の一致検査や、戻り値の確認漏れを検出するような注釈もあります。

この SAL 注釈はマイクロソフトの提供する API だけでなく、われわれが開発しているソースコードでも利用できます。注釈をつけたソースコードは実装 (呼び出される側) と使用者 (呼び出す側) との両面からコンパイラーが検査するようになります。ヘッダーファイルの宣言に注釈を入れれば既存実装の動作を変えることなく、高精度な問題検出をコンパイラーが実施してくれるようになるため、 SAL 注釈も積極的に使用していきたいものです。

以下に主な SAL 注釈を例示するのでご利用ください。

_In_z_: 関数が読み取るために受け取る '\0' 文字で終端された文字列。
e.g. void f(_In_z_ const TCHAR* filename);
_In_count_(size): 関数が読み取るために受け取る配列。関数引数で指定された要素数を持つ。
e.g. int sum(_In_count_(nr) const int* array, size_t nr);
_In_bytecount_(size): 関数が読み取るために受け取るバッファ。関数引数で指定されたバイト数を持つ。
e.g. void process(_In_bytecount_(size) const unsigned char* image, size_t size);

_Out_z_cap_(size): 関数が書き込むために受け取るバッファ。関数引数で指定された要素数まで書き込める。関数から制御が戻ったときバッファは '\0' 文字で終端される。
e.g. void getFilename(_Out_z_cap_(length) TCHAR* name, size_t length);
_Out_cap_(size): 関数が書き込むために受け取るバッファ。関数引数で指定された要素数まで書き込める。
e.g. void sort(_Out_cap_(nr) int* result, _In_count_(nr) const int* array, size_t nr);
_Out_cap_c_(size): 関数が書き込むために受け取るバッファ。定数式で指定された要素数まで書き込める。
e.g. void getWorkdir(_Out_cap_c_(MAX_PATH) TCHAR* path);
_Out_bytecap_(size): 関数が書き込むために受け取るバッファ。関数引数で指定されたバイト数まで書き込める。
e.g. void getBinary(_Out_bytecap_(size) unsigned char* value, size_t size, _In_z_ TCHAR* key);
_Deref_out_z_: 関数が確保して返すバッファを受け取るポインター。
e.g. void dupStr(_Deref_out_z_ TCHAR** newStr, _In_z_ const TCHAR* fromStr);

_Inout_z_cap_(size): 関数が読み書きするバッファ。関数引数で指定された要素数まで読み取り、書き込める。 '\0' 文字で終端したものを渡し、結果も終端される。
e.g. void trancate(_Inout_z_cap_ TCHAR* path);

_Ret_z_: 関数の戻り値で '\0' 文字で終端される。
e.g. _Ret_z_ const TCHAR* getName(ID id);
_Printf_format_string_: 関数引数は printf 系関数の書式文字列である。
e.g. void DebugTrace(_Printf_format_string_ const TCHAR* format, ...);
_Scanf_s_format_string_: 関数引数は scanf_s 系関数の書式文字列。
e.g. void readData(_Scanf_s_format_string_ const TCHAR* format, ...);