日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

C 言語における無効なスタック領域へのポインタを検出する静的解析
矢杉 和義

五十嵐 淳

C 言語は，柔軟な低レベルメモリ処理能力を持つがゆえに，無効なメモリへのアクセスを行うバグが容易に混入する．本研究は，C 言語において起こりうるメモリアクセス違反のうち，寿命が尽きて無効になったスタック領域へのポインタへのアクセスに焦点を当て，C 言語のソースコード中に，無効なスタック領域へのポインタを生じさせうる
ようなコードが存在するかどうかを検査する静的解析手法を提案する．本解析は，関数定義に現れる各式の値を，その値が含むポインタの指す領域で分類し，return 文がその関数の局所変数を指すポインタを返さないことを検査す
る．特に，関数呼び出し式の値が指す領域を，その関数の定義を用いず実引数の情報のみから推論するので，関数定義ごとに独立に解析できる特徴がある．本研究はさらに，C 言語のサブセットとその上での本解析を形式化し，本解析により検証されたプログラムは実行しても無効なポインタが生じないことを証明する．

値に対する不変条件が少ないために，精度の高い静1 はじめに的解析が困難である．そのため，先行研究 [8, 10] でC 言語は，速い実行速度と低レベルメモリ処理には，アノテーションを追加するなどの言語の拡張を行おける柔軟な表現力をもつために，今もなおシステム

うことで，解析できる情報を増やして解析の精度を高プログラミング言語として幅広く用いられている．一

めるものある．

方，C 言語にはバグを軽減する機能が殆どないため，

本研究では，C 言語に対する，ローカル変数の寿

C 言語による脆弱性被害は繰り返されている．その命に関するバグを検出する静的解析手法を提案する．

ため，C 言語プログラムからバグを検出する研究が本解析手法には次のような特徴がある：

求められている．

言語を拡張しない C 言語のプログラムなら通常

C 言語プログラムからバグを検出する手法の 1 つ

すでに備わっている関数宣言の情報を活用するこに静的解析がある．静的解析は，プログラムを実行すとで，アノテーションなどによる言語の拡張をすることなくそのソースコードを解析することで，プロることなく解析する．

グラム中に含まれるバグを検出する手法である．静的

intra-procedural な解析 関数呼び出し式の解

解析はプログラムの実行以前に行うので，十分な時析を，呼び出す関数の定義に依存せず，その関数

間と計算資源を用いて解析することができるが，プの宣言の情報のみを用いて行うため，プログラム

ログラムには実行時にしか決定できない情報も存在

中の各関数定義を独立に解析できる．

するので，偽陽性の発生は避けがたい．特に，型付け

線形時間アルゴリズム 本解析は型検査の拡張にが弱く，柔軟な低レベルメモリ処理が可能な C 言語

よって実現される．型検査アルゴリズムはソース

は，ソースコード上の記述から保証できる，実行時のコードのサイズに対して線形時間のアルゴリズ

Static analysis of the C language to detect pointers
pointing to an invalid stack area.
Kazuyoshi Yasugi, Atsushi Igarashi, 京都大学大学院情報学研究科, Graduate School of Informatics, Kyoto
University.

ムなため，本解析も線形時間で実行できる．

int * f ( void ) {int x = 0;
return & x ;}Listing 1

無効なスタック領域へのポインタを返す関数

1. 1 論文の構成
2 節では，まず無効なスタック領域へのポインタとその問題点について説明する．3 節では，本研究が提int * f1 ( int * x ) {return x ;}int * f2 ( int *) {return NULL ;}int * g1 ( void ) {int x = 0;
return f1 (& x );}int * g2 ( void ) {int x = 0;
return f2 (& x );}案する静的解析手法について詳しく述べる．4 節では，C 言語のサブセット言語 Csub を定義し，CsubListing 2関数呼び出しを介してポインタを返す関数

上での本解析を形式化する．5 節では，Csub 上における本解析の健全性について論じる．

2 無効なスタック領域へのポインタ
C 言語では，関数を呼び出すたびに，その関数内で用いられるローカル変数を格納するためのスタックフ
レームが割り当てられる．このスタックフレームは，関数実行の終了とともに解放されるため，このスタックフレーム内のアドレスを指すポインタを呼び出し

int * f ( int * x ) {if ( x ) {x = f ( NULL );}return x ;}int * g ( void ) {int x = 0;
return f (& x );}Listing 3

本解析を通らない関数

元に返すと，無効なメモリ領域を指すポインタが生じる．このポインタのことを，ここでは無効なスタッ
ク領域へのポインタと呼ぶ．

つまり，f1 は Listing 1 と同様に無効なスタック
領域へのポインタを返す関数である．

Listing 1 は，無効なスタック領域へのポインタを• f2 はヌルポインタを返す定数関数なので，g2 の返す関数を表している．x のアドレスは f の実行の終戻り値はヌルポインタである．よって，無効なポ了とともに解放されるため，f の戻り値 &x は無効な

インタは生じない．

スタック領域へのポインタとなる．無効なスタック領

f1 や f2 の実装が g1 や g2 と異なる翻訳単位にある域へのポインタに対する間接参照は未定義動作であ場合，g1 や g2 の翻訳単位からは f1 や f2 の実際のり [7]，このポインタの悪用は深刻なセキュリティ脆

関数定義がわからないため，f1 や f2 の呼び出しが安

弱性につながる．したがって，Listing 1 のような無全かどうかを判定できない．

効なスタック領域へのポインタを生み出す関数定義を，事前に検出する必要がある．

3 静的解析手法のアイデア

Listing 1 のような単純な例では，無効なスタック

2 節で言及したように，無効なスタック領域へのポ

領域へのポインタの発生を容易に検出できるが，関数インタの存在を検査する際には，関数呼び出しの実際

呼び出しを介すと，問題は本質的に困難になる．

の挙動が呼び出し元からはわからないことが問題と

Listing 2 は関数呼び出しを介しているために解析なる．そこで，本研究が提案する解析手法は，呼び出が困難な問題の例である．f1 は int* 型の引数をそす関数に対しても同じ解析を適用することを仮定すのまま返す恒等関数であり，f2 は引数によらずにヌることで，この問題を緩和するものである．

ルポインタを返す定数関数である．

• f1 は恒等関数なので，g1 の戻り値は &x である．

例えば，Listing 3 の g の解析について考える．gが呼び出している f が本解析を通ると仮定する．このとき，本解析の性質から，f が返すポインタ x は，f や f がさらに呼び出しうる関数のローカル変数のア
ドレスではないと結論できる．つまり，そのポインタ
は，引数やグローバル変数から到達可能なアドレス，
またはヌルポインタのいずれかに限られる．したがっ

int * f ( void ) {int x = 0;
int * y = NULL ;int ** z = & y ;y = &x;return * z ;}て，g において，f の引数に渡すポインタ &x が指している領域を把握していれば，その戻り値が指す領域

Listing 4型システムの不変条件を壊す代入の可能性を限定することができる．さらに，f の停止性も仮定すれば，たとえ f が再帰呼び出しを含んで印の両方の情報をもつ．ポインタを含まない型に対いても，f の戻り値が指す領域を推論できる．この g

応する印付き型は，もとの型と同じとする．そして，の場合，f に渡しているポインタは g のローカル変数

印付き型の上にも，印の半順序から自然に従う半順序のアドレスなので，f の戻り値，ひいては g の戻り値を導入しておく．

が g のローカル変数のアドレスの可能性がある．し

本解析における印付き型の型システムは，文の任意たがって，本解析は g を危険な関数であると判断すの実行時点において，各変数の印付き型とその値が次る．実際には g は無効なスタック領域へのポインタを生じさせない †1 ので，Listing 3 は偽陽性の例になっの不変条件を保つように設計されている：ている．

• i 以上の印をもつポインタは，有効なアドレスを指すポインタであるか，またはヌルポインタである．

3. 1 静的解析手法の詳細• o 印をもつポインタは，その時点の関数のスコー

本解析は，通常の C 言語の型システムを拡張した，

プにおける自動記憶域期間をもつ領域を指さな

flow-sensitive な型システムを用いた型検査によりプ

い．特に，呼び出し元の関数のスコープにおけるログラムの解析を行う．

自動記憶域期間をもつ領域を指してもよい．

まず，メモリ領域の種類を，未定義な領域，現在の• g 印をもつポインタは，自動記憶域期間をもつ関数のスコープにおける自動記憶域期間をもつ領域，

領域を指さない．特に，呼び出し元の関数のス

現在の関数の呼び出し元の関数スコープにおける自コープにおける自動記憶域期間をもつ領域も指動記憶域期間をもつ領域，静的記憶域期間をもつ領

さない．

域，の 4 種類に分類する．そして，これらの領域の型システムがこの不変条件を満たすならば，全ての種類に対して，u(ndef), i(nside), o(utside), g(lobal)

return 文が i 以下の印をもつポインタ値を返さなけの 4 種類の印を対応させる．この 4 つの印の上に，れば，関数から無効なスタック領域を指すポインタがu < i < o < g から従う半順序を導入する．

返されることはないことを保証できる．本解析が行う

C 言語の型に対して，上で導入した印の情報を追型システムの型検査アルゴリズムは，基本的にはそれ加した型を印付き型と呼ぶ．ポインタ型に対応する印ぞれの式や文がこの不変条件を満たすことを確認し付き型には，その型のポインタが指す領域の種類をながら，代入文や制御構文の分岐の合流のたびに型環表す印の情報を追加する．このとき，ポインタ型が印

境を更新するものである．

m をもつことは，その型のポインタ値が指す先の領

ここからは，本解析における型検査アルゴリズムの域に対応する印が，印の上の半順序に関して m 以上

うち，特筆すべき処理について，具体例を交えながらであることを表す．ポインタへのポインタ型の印付き

説明する．

型は，内側のポインタ型の印と外側のポインタ型の

代入文の型検査について，Listing 4 を例に考える．

f において，y はまず g 印をもつヌルポインタで初期†1 g はヌルポインタを返す．

化される．z はローカル変数 y のアドレスで初期化さvoid f ( int n ) {int * x = & n ;int * y = & n ;int ** z = n ? & x : & y ;* z = NULL ;}Listing 5

間接参照による代入

void f ( int ** x , int * y ) {*x = y;}void g ( void ) {int * x = NULL ;int y = 0;f (& x , & y );}Listing 6

引数経由のポインタ値の書き込みれるので，z は g 印の int 型ポインタを指す i 印のポインタ型をもつ．その次の文では y に対して，i 印のポインタ型をもつローカル変数 x のアドレスが代入される．もしこの代入を認めてしまった場合，*zは g 印のポインタであるが，*z の値は y の値つまりローカル変数 x のアドレスである．x は自動記憶域期間をもつ変数なので，型システムの不変条件を満たさtypedef struct {int *a , * b ;} S;
int * f ( short * n , int ** x , S * y );int * g ( int * x ) {short n = 0;S y = {x , NULL };return f (& n , &x , & y );}ない．これを防ぐため，本解析では右辺式の印が左辺式の印未満のときの代入は，型検査エラーとなるよう

Listing 7

関数呼び出し式の印付き型の推論に設計した．
左辺式が間接参照を含む代入文の型検査について，

x = &y という代入文と等価であるので，x はローカ

Listing 5 を例に考える．f において，x も y も i 印のル変数 y を指す．しかし，型システムの側からは，xポインタである．z は n の値に依存して，x か y のいずは依然として g 印のポインタであるので，型システ

れかのアドレスで初期化されるが，いずれにせよ z は i

ムの不変条件を満たさない．この問題は，f の側の型

印のポインタ型への i 印のポインタ型をもつ．ここで，システムからは，f の引数のポインタがどこを指して*z に対する g 印のヌルポインタの代入は，上述の代いるのかわからない点にある．そのため，f における入文における印の制約 (左辺式の印 i ≤ 右辺式の印 g)

代入文 *x = y は，x と y に引き渡されるポインタ値を満たすが，実際に x と y のどちらにヌルポインタの印によっては型システムの不変条件を壊す代入となが代入されるのかわからないため，x と y のどちらのる．そこで本解析では，引数のポインタ値の先の領域

印付き型を更新すべきなのかわからない．このようにに対する g 未満の印付き型をもつ値の代入は，型検

左辺式が間接参照を含む場合，一般に印付き型を更新

査エラーとなるように設計した．g の印付き型をもつするべき変数を特定することができない．そのため値の代入であれば，型システムの不変条件を壊すこと

本解析では，間接参照の先に対する代入の場合には，はないので認めてよい．

印付き型の更新を行わない．印付き型の更新を行わな

関数呼び出し式の型検査について，Listing 7 を例

くても，前述の代入文における印の制約さえ満たしてに考える．構造体 S は int* 型の値を 2 つ保持する型

いれば，型システムの不変条件は保たれる．

である．f の戻り値型は int* なので，f の宣言のみ

C 言語の関数においては，引数に渡したポインタから考えられる f が返しうるポインタは，を経由して関数の出力を行う技法がしばしば用いら

1. 第 2 引数 x が指す先のポインタ値，

れるが，Listing 6 に示すような場合には，型システ

2. 第 3 引数 y が指す先の構造体 S がもつ 2 つのポムの不変条件が壊れる可能性がある．f は第 1 引数が指す先の int* 型の領域に第 2 引数のポインタ値を書き込む関数である．g において，x は g 印のヌルポ
インタで初期化される．g における f の呼び出しは，

インタ値，3. グローバル変数から到達可能なポインタ値，
4. ヌルポインタのいずれかであると考えられる．特に，ポインタ間

キャストは型システムの不変条件を壊すため，本解析はこれを認めてみない．そのため，ここでは short*
から int* へのキャストは考慮しない．前述の代入文における印の制約により，グローバル変数にはローカ
ル変数のアドレスは含まれていないので，3, 4 はいず
れも g 印のポインタ値と考えてよい．1, 2 のポインタの印は，g における f の呼び出しの実引数から知る

void f ( int ** x , int * y ) {*x = y;}int * g ( void ) {int * x = NULL ;f (& x , NULL );return x ;}Listing 8

代入文における印の制約の違反の例

ことができ，順に o と o, g であることがわかる．つまり，f の戻り値の印は o 以上であることがわかる．

き，型検査エラーとなる．

よって，f の呼び出し式の印付き型には o 印を与えれ• 左辺式がポインタの間接参照を含む場合，左辺ばよい．この推論により，呼び出す関数の実装に依存

値の印付き型は更新しない．左辺式がポインタのすることなく解析を行うことができる．

間接参照を含まない場合，左辺値の印付き型を右

以上のアイデアをふまえた，本解析が行う flow-

sensitive な型システムによる型検査アルゴリズムを次にまとめる：
変数宣言• 未初期化のポインタ値の印付き型には u をつける．

辺値の印付き型で更新する．

• 左辺式が o 印のポインタ値に対する間接参照を含み，かつ左辺値がポインタ値を含むとき，型検
査エラーとなる．
制御文• 分岐が合流するとき，各変数の合流後の印付き• 仮引数のポインタ値の印付き型には o をつける．

型を，次の条件を満たす印付き型のうち最大のもアドレス式

ので更新する：任意の分岐に対して，合流後の印• 自動記憶域期間をもつ変数のアドレス値の印付付き型は，その分岐におけるその変数の印付き型

き型には i をつける．

• 自動記憶域期間をもたない変数のアドレス値およびヌルポインタの印付き型には g をつける．
関数呼び出し式

以下である．

return 文• return する値の印付き型が i 以下の印を含むと
き，型検査エラーとなる．

• 関数呼び出し式の戻り値型が基本型の場合，その呼び出し式の印付き型は，戻り値型と対応す

3. 2 偽陽性

る印付き型のうち，次の条件を満たす最大のも他の静的解析手法と同様に，本解析にも偽陽性がのとする：実引数に含まれる任意の値に対して，存在する．Listing 8, 9, 10, 11 に挙げたプログラムは，その値の型が戻り値型と同じならば，呼び出し式

いずれも本解析の検査を通らないが，C 言語プログの印付き型はその値の印付き型以下である．

ラムとして合法なもの，すなわち偽陽性と判断される• 関数呼び出し式の戻り値型が複合型の場合，そプログラムの例である．Listing 8, 9 のような偽陽性の型に含まれる各基本型に与える印を上の規則

は，本解析に特有のものであり，型検査アルゴリズムにしたがって導いたのち，それらの基本型を結合の設計選択の結果である．一方，Listing 10, 11 のよした印付き型を，呼び出し式の印付き型とする．

うな偽陽性は，本手法に限らず静的解析では本質的にキャスト式• ポインタ型への，またはポインタ型からのキャスト式は，型検査エラーとなる．

解決困難な問題である．
代入文における印の制約の違反 (Listing 8)

3. 1 節で述べたように，本解析の型システムの不変

代入文

条件を壊す代入文は，たとえ合法な操作であっても本• 右辺値の印付き型が左辺値の印付き型未満のと解析の検査を通らない．

ない．しかし静的解析では，一般に実行パスの到達可

int * f ( int * x , int * y ) {return y ;}int * g ( void ) {int x = 0;
return f (& x , NULL );}能性を決定不能であるため，型検査は到達可能性にか
かわらず行う必要がある．そのため，到達不能な実行パスにおける違法な操作に対して本解析の検査が通らないために，違法なプログラムであると判定される可能性がある．

Listing 9

印付き型の推論の誤差の例

4 形式化
char a [4] = " abc " ;char * f ( void ) {intptr_t x = ( intptr_t ) a ;++ x ;
return ( char *) x ;}Listing 10

ポインタ型に関するキャストの例

3 節で説明した静的解析手法のアイデアが健全であること，すなわち，本解析を通過したプログラムには，無効なスタック領域へのポインタに対するア
クセスが含まれないことを保証するためには，本解析を形式化し，健全性を証明する必要がある．本節では本解析の形式化を行う．4. 1 節では，解析の対象とする C 言語のサブセット言語 Csub の構文を定義

int * f ( void ) {int x = 0;
if (0) {return & x ;} else {return NULL ;}}Listing 11

する．4. 2 節では，Csub の操作的意味論を定義する．

4. 3 節では，もとの C 言語と Csub との差分について取り上げ，その妥当性を検討する．4. 4 節では，本解析のアイデアを形式化した Csub の型システムを定義する．なお，Csub の構文および操作的意味論の定義においては，Clight [3] の形式化を参考にしている．

到達不能な実行パスの例

4. 1 Csub の構文
印付き型の推論の誤差 (Listing 9)

C 言語のサブセットを形式化した Csub の構文を

本解析は，関数呼び出し式の印付き型を，その関数

図 1 に示す．オリジナルの C 言語全体に対する形式の実装に依存することなく決定する．そのため，関数化は，その規模のために困難であるので，C 言語の代の実装によっては，印付き型と実際の戻り値との間にわりに Csub のプログラムを，形式化された本解析の誤差が生じ，合法なプログラムであっても本解析の検対象とする．

査を通らないということが起こりうる．この問題は，型 型は int 型と ptr 型と pair 型の 3 種類であ

戻り値型と同じ型の引数が複数ある場合に顕著になる．int 型は整数型，ptr 型はポインタ型を表しる．また，前述の Listing 3 もこの種の偽陽性である．

ており，pair 型は int 型または ptr 型からなる

ポインタ型に関するキャスト (Listing 10)列を表す．pair 型を用いて構造体を模倣する．

ポインタ型から異なるポインタ型へのキャスト，あ式 式は左辺値式と右辺値式のいずれかである．式

るいはポインタ型と整数型の間のキャストは，型シ

は型と値を持ち，左辺値式は対応する領域をもつ．

ステムを壊すものであるから，たとえ合法な操作で左辺値式 .0 演算子と .1 演算子は，pair 型の左あっても，型システムに依存した本解析の検査を通ら

辺値式から，それぞれ前者と後者を取り出す演算

ない．

を表す．* 演算子は，ポインタ型の式からそのポ到達不能な実行パス (Listing 11)

インタが指す先の領域を取り出す演算を表す．

到達不能な実行パスにおいて違法な操作が行われ右辺値式 + 演算子は，整数型に対する加算を表す．

た場合，実際にはその違法な操作は実行されることは& 演算子は，左辺値式からその領域を指すポイン

識別子

x

メモリ状態

整数

n

型

メモリブロックbτ ::= σ | pair(σ, τ )

オフセット

δ

σ ::= int | ptr(τ )アドレス

e ::= l | r

式

値

左辺値式

l ::= x | l.0 | l.1 | *e

右辺値式

r ::= n | e + e | &ls ::= skip | return e |文

l = e | l = x(e) | s; s |if(e){s}else{s} | while(e){s}d ::= τ x

変数宣言

f ::= τ x(d){d+ ; s}p ::= (b, δ)v ::= u | cons(u, v)
u ::= integer(n) | pointer(p) | undef

出力ω ::= pass | ret(v)

ローカル環境E : x 7→ b

グローバル環境G : x 7→ b

関数環境

F : x 7→ f

図2

d ::= d | d, d+
+

関数定義

M

Csub の操作的意味論におけるメタ変数

ロック中の各バイトは整数値のオフセット δ を用

f + ::= f | f , f +いて特定する．すなわち，メモリ上のアドレス p

P ::= d+ , f +は，メモリブロック b とオフセット δ の組によっ

プログラム

図1

Csub の構文て表現される．
値 integer(n) は整数値 n を表す．pointer(p) はメモリ上のアドレス p を指すポインタ値を表す．

タを作る演算を表す．
文 l = e は代入文を表す．l = x(e) は，関数呼び

undef は未初期化の値を表す．cons(u, v) は pair

出し x(e) の戻り値を l に代入する代入文を表す．

型の式と対応しており，整数値，ポインタ値また

変数宣言 τ x は，τ 型の変数 x の宣言を表す．
+

は未初期化値の一連の列を表す．

関数定義 τ x(d){d ; s} は，引数宣言が d，戻り

出力 ω は関数定義中の文の実行の状態を表す．

値型が τ である関数 x の定義を表す．d+ は関数

pass は関数を実行中であることを表し，ret(v)x のローカル変数の宣言を，s は関数 x の本体を

は値 v を return する文を実行したあとであるこ

表す．

とを表す．
+

プログラム d , f++は，グローバル変数宣言の列

d と，関数定義の列 f+からなるプログラムを表す．

ローカル環境 E は，ローカル変数 x と，その変数が割り当てられているメモリブロック b との対応を表す写像である．
グローバル環境 G は，グローバル変数 x と，そ4. 2 Csub の操作的意味論の変数が割り当てられているメモリブロック b とCsub の操作的意味論の判断で用いるメタ変数をの対応を表す写像である．

図 2 に示す．
メモリ状態 M は Csub のメモリモデルを数学的関数環境 F は関数名 x とその名をもつ関数定義

f との対応を表す写像である．

に表現したオブジェクトであり，直観的にはいく

Csub におけるメモリモデルの表現には， [9] におつかのメモリブロックの集合である．メモリ状態

けるメモリモデルを採用している． [9] では，メモリの詳細な扱いに関しては，Csub で採用するメモ

状態 M に対して，次の 4 つの操作を定義している．

リモデルとともに後述する．

これらの関数は，いずれも戻り値はオプション型であメモリブロック・オフセット・アドレス メ モ リ
ブロック b は有限のバイト列を表す．メモリブ

り，成功すれば結果が ⌊·⌋ に囲まれて出力され，失敗すれば ε が出力される．

判断とは明示的に区別する必要がある．
左辺値式

G, E ⊢L l, M ⇓ p

式 グローバル環境 G，ローカル環境 E ，メモリ式

G, E ⊢R e, M ⇓ v

状態 M のもとで，式 e は値 v に評価される．

値格納

G, E ⊢V l, v, M ⇓ M ′文

F , G, E ⊢S s, M ⇓ ω, M ′F , G ⊢F x(v), M ⇓ v ′ , M ′関数

G ⊢P P , M ⇓ v

プログラム
図3

Csub の操作的意味論の判断

値格納 グローバル環境 G，ローカル環境 E ，メ
モリ状態 M のもとで，左辺値式 l を評価した先のアドレスに値 v を格納した，新しいメモリ状
態 M ′ に評価される．
文 関数環境 F ，グローバル環境 G，ローカル環
境 E ，メモリ状態 M のもとで，文 s を実行した′

alloc(M, lo, hi) = ⌊(b, M )⌋： メモリブロックを結果の出力 ω と新しいメモリ状態 M ′ に評価さ追加する．メモリ状態 M ，下位オフセット lo ，れる．出力が pass だった場合，後続の文が引き上位オフセット hi を入力として，lo を下界，hi

続き評価されるが，出力が ret(v) だった場合，後を上界とする新しいメモリブロック b と，新しいメモリ状態 b の組を出力する．

続の文は評価されない．
関数 関数環境 F ，グローバル環境 G，メモリ状

free(M, b) = ⌊M ′ ⌋： メモリブロックを解放する．

態 M のもとで，関数 x の引数に値 v を渡して呼メモリ状態 M ，メモリブロック b を入力として，

び出し，その戻り値 v ′ と新しいメモリ状態 M ′そのメモリブロックを解放した後の新しいメモリに評価される．

′

状態 M を出力する．

プログラム グローバル環境 G，メモリ状態 M のload(t, M, b, δ) = ⌊v⌋： メモリから値を読み出す．

もとで，グローバル変数 G が適切に初期化されてメモリ型 t，メモリ状態 M ，メモリブロック b，いるならば，main 関数の戻り値 v に評価される．

オフセット δ を入力として，メモリブロック b とCsub では，左辺値式および式の評価は副作用を引オフセット δ によって指定されるアドレスから，
メモリ型 t のサイズ分の値 v を読み出して出力する．

き起こさない．

Csub の操作的意味論の判断は，実行時エラーに直面した場合に error に評価される．後の 4. 3 節で詳し

store(t, M, b, δ, v) = ⌊M ′ ⌋： メモリへ値を書き込

く述べるように，操作的意味論の判断の評価における

む．メモリ型 t，メモリ状態 M ，メモリブロック

error は，そのまま無効なスタック領域を指すポインb，オフセット δ ，値 v を入力として，メモリブ

タへの間接参照を表すように定義される．導出途中の

ロック b とオフセット δ によって指定されるアド判断で発生した error は伝播し，最終的にプログラム

レスに，値 v を書き込んだ新しいメモリ状態 M ′の判断の結果が error となるように導出規則が定義さを出力する．

れる．

Csub では，これらの操作を primitive な演算として用いることで，メモリモデルの詳細な実装を隠蔽

Csub における操作的意味論の導出規則の抜粋を
図 4 に示す．

し，より高級な操作的意味論の構築に注力している．

(S-Store) 左辺値式に対して値を格納する判断

また，メモリは 4 バイト境界でアラインメントし，の導出規則である．メモリ状態 M0 上のアドレ

integer(n), pointer(p), undef にはいずれも 4 バイト

ス (b, δ) に対して，primitive 演算 store を用いの領域を使用する．

て，値 u を設定した新しいメモリ状態 M1 に評

続いて，Csub の操作的意味論の判断を図 3 に示す．

価される．

左辺値式 グローバル環境 G，ローカル環境 E ，メ

(S-Call) 関数呼び出しの戻り値を左辺値式にモリ状態 M のもとで，左辺値式 l はアドレス p

代入する判断の導出規則である．まず，式 e を評に評価される．左辺値式は式でもあるので，式の価して値 v0 を取り出し，v0 を x に与えた関数呼4. 3 C 言語と Csub との差異

G, E ⊢L l, M0 ⇓ (b, δ)
store(int32, M0 , b, δ, u) = ⌊M1 ⌋G, E ⊢V l, u, M0 ⇓ M1

Csub の操作的意味論におけるエラーは，無効なス(S-Store)

こるように設計されている．つまり，ポインタを間接G, E ⊢R e, M0 ⇓ v0

参照した結果は，次のいずれかに限られる：F , G ⊢F x(v0 ), M0 ⇓ v1 , M1

• 有効なポインタの間接参照であり，ポインタがG, E ⊢V l, v1 , M1 ⇓ M2
F , G, E ⊢S l = x(e), M0 ⇓ pass, M2(S-Call)F , G, E ⊢S return e, M ⇓ ret(v), M
F , G, E ⊢S s0 ; s1 , M0 ⇓ ret(v), M1
G, E ⊢L l, M ⇓ (b, δ)(S-Ret)(S-SeqRet)

こす．
この設計により，Csub は無効なスタック領域を指す
ポインタのみに注目した体系となっている．以下では，もとの C 言語にあって，Csub にはない言語要素

load(int32, M, b, δ) = ε

G, E ⊢R l, M ⇓ errorを，Csub が含まない理由について述べる：
ヌルポインタ ヌルポインタは無効なポインタ値(E-Load)
図4

指す先の領域を取得できる．

• ポインタが指す先は解放済みのスタック領域であり，そのポインタの間接参照はエラーを引き起

G, E ⊢R e, M ⇓ v
F , G, E ⊢S s0 , M0 ⇓ ret(v), M1

タック領域を指すポインタの間接参照によってのみ起

Csub の操作的意味論である．よって，もし Csub にヌルポインタを導入すると，無効なスタック領域を指すポインタのみに注目した設計を壊すことになる．そのため，び出しを評価して，関数の戻り値 v1 と新しいメ

Csub はヌルポインタを含まない．

モリ状態 M1 得る．l, v1 , M1 に対する値格納の構造体 Csub が構造体そのものを持たず，pair 型

判断を評価することで，代入後のメモリ状態 M2によって構造体を模倣する設計を選択しているのを得る．

は，単に体系の簡潔のためである．

(S-Ret) return 文の実行を表す判断の導出規則

pair 型には構造体のようにタグ名がついていなである．式 e を評価した値 v に対して，ret(v) にいため，自分自身の構造体へのポインタをメンバ評価される．

にもつ構造体を表現できない．一方，Csub には(S-SeqRet) 連続する文の実行を表す判断の導

ヌルポインタがないため，このような自己参照的出規則である．前半の文 s0 を実行して出力 ret(v)な構造を初期化することができない．そのため，を得た場合，後半の文 s1 は実行されない．連続

Csub は自己参照的な構造を導入していない．

する文全体の判断における出力と新しいメモリ

pair 型は int 型や ptr 型からなる一列の構造し状態は，前半の文の判断と同じものが使われる．

か成すことができないため，他の構造体をメンバ(E-Load) 左辺値式からの値の読み込み，つまにもつ構造体のような型を表現できない．しかり lvalue-to-rvalue conversion が失敗したことをし，入れ子になった構造体を潰して 1 つの構造表す判断の導出規則である．まず，l を評価してア体に変換する操作を考えると，pair 型は構造体

ドレス (b, δ) を得る．そのアドレスから load をと同程度の表現力をもつといえる．

用いて 4 バイトのメモリを読み出そうとするが，整数値に対する算術演算 Csub には，整数値に対load が無効値 ε を返して失敗したため，error にする算術演算として + しか含まれていないが，こ評価される．

の制限は単に体系の簡潔のためである．本解析
はポインタの指す領域のみに着目しているため，整数値に対するその他の算術演算を Csub に含めても，本解析は影響を受けない．

ポインタ値に対する算術演算 もし Csub においてポインタ値に対する算術演算を行うことができ
れば，メモリブロックの範囲外を指すような無効なポインタ値を表現できるようになり，無効な
スタック領域を指すポインタ値のみに注目した設計を壊すことになる．そのため，Csub はポインタ値に対する算術演算を認めていない．また，

void f ( void ) {int * x = NULL ;{int y = 0;
x = &y;}* x = 0; // NG}
Listing 12

この帰結として，Csub は配列を含まない．

ローカルスコープ内における無効なスタック
領域へのポインタ

共用体・キャスト 共用体やキャストは型システムを壊すことができる．本解析はプログラムを静的解析のみによって検査するため，型システムが壊印

されると何も保証できなくなってしまう．そのた

印付き型

m ::= u | i | o | gµ ::= ν | pair(ν, µ)ν ::= int | ptr(µ, m)

め，Csub は共用体やキャストを含まない．
関数 C 言語における関数呼び出しは式であるが，グローバル型環境∆ : x 7→ µCsub では式から副作用を取り除くために，代入

ローカル型環境Γ : x 7→ µと組み合わせた文として扱っている．

図5

Csub の型判断におけるメタ変数

Csub の関数の引数は，体系の簡潔のためにちょ
うど 1 つに限られている．void 型の引数や戻りと，Listing 12 のような，ローカルスコープ内に値をもつ関数は，ダミーの int 型の値を受け渡おける無効なスタック領域へのポインタが発生ししする関数を対応させることができ，複数の引うる．これに対しても本解析を適用するために数を受け取る関数は，pair を用いて引数を 1 つ

は，印に加えて，ブロックの深さの情報も同時ににまとめた関数を対応させることができるので，扱う必要があり，体系を簡潔に保つことができな

Csub の関数は C 言語の関数と同程度の表現力をい．そのため，Csub では関数定義の先頭以外のもつといえる．

位置でのローカル変数宣言を認めていない．

Csub には，体系の簡潔のために関数ポインタが存在せず，関数呼び出しは常に関数名を直接用い

4. 4 型システム

る必要がある．しかし，もし Csub に関数ポイン

Csub の型判断で用いるメタ変数を図 5 に示す．

タを導入したとしても，関数ポインタは静的記憶

印・印付き型 Csub の型は，3 節において扱った

域期間をもつので，関数ポインタに印 g をつけるようにすれば，容易に本解析を拡張することができると考える．
制御構文 Csub は体系の簡潔のために，制御構文ものと同じ印付き型である．
グローバル型環境 ∆ は，グローバル変数 x と，その印付き型 µ との対応を表す写像である．
ローカル型環境 Γ は，ローカル変数 x と，その印として if と while しかもたない．しかし，本解付き型 µ との対応を表す写像である．

析の型検査アルゴリズムは制御構文の形式に依存

続いて，Csub の型判断を図 6 に示す．

していないので，例えば switch，break や goto

左辺値式 グローバル型環境 ∆，ローカル型環境などのその他の制御構文を Csub に加えても，分Γ のもとで，左辺値式 l が印付き型 µ をもち，l岐の合流における型環境の更新をうまく定義するのアドレスの印が m であることを表す．

ことで，容易に本解析を拡張することができる．

式 グローバル型環境 ∆，ローカル型環境 Γ のも

変数宣言 関数定義の先頭だけでなく，任意のブとで，式 e が印付き型 µ をもつことを表す．

ロックの先頭でのローカル変数宣言を許容する

値格納 グローバル型環境 ∆，ローカル型環境 Γ∆, Γ ⊢V l, µ ⇒ Γ′′

F , ∆, Γ ⊢S s : τ ⇒ Γ

関数定義

F , ∆ ⊢F f

プログラム

⊢P P

図6

Csub の型判断

Γ0 [µ/x] = Γ1∆, Γ0 ⊢V x, µ ⇒ Γ1∆, Γ ⊢R e : µ

式
値格納
文

Γ0 (x) ⊑ µ∆, Γ ⊢L l : (µ, m)

左辺値式∆, Γ ⊢R e : µ∆, Γ0 ⊢V l, µ ⇒ Γ1

F , ∆, Γ0 ⊢S l = e : τ ⇒ Γ1∆, Γ ⊢R e : µµ 0 ⊑ µ1m0 ≤ m1

ptr(µ0 , m0 ) ⊑ ptr(µ1 , m1 )
ν0 ⊑ ν1µ0 ⊑ µ1pair(ν0 , µ0 ) ⊑ pair(ν1 , µ1 )
図7

代入可能な印付き型の対応を表す二項関係|µ| = τ

(T-Assign)

fill(τ, o) ⊑ µΓ ⊢S return e : τ ⇒ Γ(T-Ret)図8

int ⊑ int

(T-StoreLocal)

Csub の型判断の導出規則

は，µ から全ての印を取り除いた型を表す．fill(τ, m)
は，τ に対応する印付き型のうち，その印の全てが mであるものを表す．

(T-StoreLocal) ローカル変数への値の格納の型判断を導出する．変数 x のもとの印付き型

Γ0 (x) に対して µ の印付き型をもつ値が格納可能であれば，Γ0 の x に対する対応を µ で更新し，新しい型環境 Γ1 を得る．

のもとで，左辺値式 l に対して印 µ をもつ値を(T-Assign) 代入文の型判断を導出する．式 e

格納した結果，新しいローカル環境 Γ′ が得られの印付き型 µ を取得し，左辺値式 l に対して µ

ることを表す．

の印付き型をもつ値を格納する．格納可能であれ

文 関数環境 F ，グローバル型環境 ∆，ローカル

ば，更新された新しい環境 Γ1 を得る．

型環境 Γ のもとで，戻り値型 τ である関数定義(T-Ret) return 文の型判断を導出する．returnの中の文 s を実行した結果，新しいローカル環

する値 e の印付き型 µ を取得し，µ に対応する′境 Γ が得られることを表す．

印無し型が現在の関数定義の戻り値型 τ と一致

関数定義 関数環境 F ，グローバル型環境 ∆ のもすることを確認する．µ の印付き型をもつ値がとで，関数 f の本体の文が正しく型付けされ，関fill(τ, o) の印付き型をもつ領域に格納可能である

数 f の本体中の全ての return 文が適切な印付き

とき，つまり，µ が i や u の印を含まないとき，型の値を返していることを表す．

式 e の値を return できる．

プログラム プログラム P 中の全ての関数定義が正しく型付けされることを表す．

5 性質と証明

Csub の型判断の導出規則において用いる二項関係

4 節における解析手法の形式化が完了したので，解の定義を図 7 に表す．二項関係 µ0 ⊑ µ1 は，µ0 の印

析手法の健全性について述べることができるように付き型をもつ左辺値式に対して µ1 の印付き型をもつなった．

右辺値式を代入可能であることを表す．ポインタ型の定理 (健全性). 任意のプログラム P ，グローバル環境間の二項関係 ptr(µ0 , m0 ) ⊑ ptr(µ1 , m1 ) の導出におG，メモリ状態 M に対して，⊢P P かつ，ある v が存いて，m0 ≤ m1 を要求している部分が，3. 1 節にお在して G ⊢P P , M ⇓ v が成り立つならば，v ̸= error

いて説明した，型システムの不変条件を保つための，が成り立つ．

代入文における印の制約を表現している．

Csub の型判断の導出規則の抜粋を図 8 に示す．|µ|⊢P P とは，プログラム P が正しく型付けされる，すなわち P が本解析の検査を通ることを表す．

G ⊢P P , M ⇓ v とは，適切に初期化されたグローバと組み合わせて偽陽性の少ない解析手法にするなど，

ル環境 G とメモリ状態 M のもとで，プログラム P

柔軟に設計の選択を行う余地が存在する．

を実行すると，プログラムが停止して，出力として v

一方，C 言語を拡張せずにそのまま解析する静的が得られることを表す．プログラムが正常に実行でき解析器の研究も盛んに行われている．この種の静的解

れば v は何らかの有効な値になるが，途中で無効な

析器は，現実のプログラムに対してそのまま適用でき

スタック領域へのポインタに対する間接参照が存在る利点をもつが，C 言語の性質上，バグの種類によっした場合，error が伝播して出力される．したがって，ては検出精度の向上が困難な場合も多い．そのため，

この健全性定理の主張は，本解析の検査を通過する検出できるバグの種類とその精度が異なるさまざま

Csub のプログラムには，無効なスタック領域へのポな静的解析器 [1, 2, 4–6] が提案されている．

インタに対する間接参照が存在しないことを表す．
この健全性の証明が，本研究の目標である．現時点
では，この証明は完了していない．

7 おわりに本研究は，C 言語プログラムにおける，無効なスタック領域へのポインタに対する間接参照に起因する

6 関連研究バグを検査する，静的解析手法を開発した．そして，

C 言語プログラムのバグを静的解析によって検出

この静的解析手法の健全性を確かめるために，C 言する研究は，これまでにも数多く行われている．それらの中でも，Cyclone [8] と CCured [10] は本研究のアプローチに近く，大いに参考にした．

語のサブセット言語 Csub を定義した．
今後の課題としては，本解析手法の健全性証明と実装が挙げられる．Csub に対する本解析手法の形式化

Cyclone は，C 言語の ポ イン タ に Region-based

は，本解析が健全であってはじめて意味をもつため，Memory Management [11] を導入した C 言語方言で健全性証明の完遂は急務である．そして，本解析の実ある．Cyclone のポインタには，region と呼ばれる，装を用いて現実の C 言語プログラムを解析すること

そのポインタが指す領域を識別するアノテーションがで，本解析における偽陽性の程度を具体的に評価する

付随している．Cyclone の型システムは，ポインタに必要があると考えている．

付加された region の情報を用いて，ぶら下がりポイ

また，本解析手法は自動記憶域期間に起因するバグ

ンタなどのバグを検出することができる．region のという，限定的な問題に対してしか対処することがで情報は関数宣言におけるポインタ引数にも指定されきない．そのため，今後はヒープ領域におけるぶら下るため，関数をまたいだ型検査が可能である．

がりポインタなど，より多くのバグに対処できる静的

CCured は，C 言語のポインタに対して 3 種類のア

解析手法へと拡張する必要があると考えている．

ノテーションを付加することで，ポインタの機能を細分化した C 言語方言である．3 種類のポインタはそ参 考 文 献れぞれ異なる用途に合わせた異なる性質をもってい[ 1 ] Ball, T. and Rajamani, S. K.: The SLAM
Project: Debugging System Software via Static
Analysis, ACM SIGPLAN Notices, Vol. 37,
No. 1(2002), pp. 1–3.
[ 2 ] Beyer, D., Henzinger, T. A., Jhala, R., and Majumdar, R.: The software model checker Blast, International Journal on Software Tools for Technology Transfer, Vol. 9, No. 5(2007), pp. 505–525.
[ 3 ] Blazy, S. and Leroy, X.: Mechanized Semantics for the Clight Subset of the C Language, Journal of Automated Reasoning, Vol. 43, No. 3(2009),
pp. 263–288.
[ 4 ] Calcagno, C. and Distefano, D.: Infer: An automatic program verifier for memory safety of Cる．ポインタの種類ごとに，その性質に合わせた実行
時検査コードを挿入することで，ポインタに対する操作が正しいことを，型検査と実行時検査の両面から確認する．

C 言語方言に対する静的解析手法は，既存のプログラムに対して適用することが難しい欠点があるが，強固な理論的裏付けをもつために，解析を通過したプログラムにある種のバグが存在しないことが保証できる．また，静的解析単体だけではなく，動的検査

programs, NASA Formal Methods, (2011), pp. 459–
465.
[ 5 ] Cousot, P., Cousot, R., Feret, J., Mauborgne,
L., Miné, A., Monniaux, D., and Rival, X.: The
ASTREÉ Analyzer, European Symposium on Programming, 2005, pp. 21–30.
[ 6 ] Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto,
V., Signoles, J., and Yakobowski, B.: Frama-C,
Software Engineering and Formal Methods, 2012,
pp. 233–247.
[ 7 ] International Organization for Standardization:
ISO/IEC 9899:2011, Programming languages – C,
2011.
[ 8 ] Jim, T., Morrisett, J. G., Grossman, D., Hicks,

M. W., Cheney, J., and Wang, Y.: Cyclone: A Safe
Dialect of C., USENIX Annual Technical Conference, 2002, pp. 275–288.
[ 9 ] Leroy, X. and Blazy, S.: Formal verification of aC-like memory model and its uses for verifying program transformations, Journal of Automated Reasoning, Vol. 41, No. 1(2008), pp. 1–31.
[10] Necula, G. C., McPeak, S., and Weimer, W.:
CCured: Type-safe retrofitting of legacy code, ACM
SIGPLAN Notices, Vol. 37, No. 1(2002), pp. 128–139.
[11] Tofte, M. and Talpin, J. P.: Region-Based Memory Management, Information and Computation,
Vol. 132, No. 2(1997), pp. 109–176.