netail.net

_ [論文] データの到達条件の解析方法 ▲

Gregor Snelting, Torsten Robschink, Jens Krinke: Efficient Path Conditions in Dependence Graphs.

To appear in ACM Transactions on Software Engineering and Methodology.

Path Condition (PC) というのは，プログラム中のある２点 x, y に対して，x で定義しているある変数が，y に影響を与えるときの条件を指す．たとえば:

a = 1;     // 1
if (x > 0) // 2
  b = a;   // 3
else       // 4
  b = 0;   // 5
c = b;     // 6

といった状態で，１行目の変数代入が６行目に影響を与えるのは３行目の文が実行されたときだけなので，PC(1,6) = (x > 0)となる．基本的には，if文やfor文での条件節をどんどんANDでつないでいった形にする．プログラムの入力変数以外（中間データ）に関しては変数を消去していって，プログラムへの入力変数がどのような条件を満たせば，その情報の流れが発生するか，ということを示す．

プログラム中の重要な変数が，他の変数から影響を受けないことを調べるには，先ほどのPCを計算して，それが充足不能であることを示せばよいことになる．これは，static program slicing で「影響を受けるかもしれない」と出てくる false positive を取り除くためにも利用できる．また，充足可能である場合は，その条件を求めれば，いつその情報流が発生するかを調べることができる．

この論文では，このPath Conditionの計算方法と，それを色々なプログラムに適用した場合の時間・空間計算量を評価している．

地点 x から y へは複数のパスがあるので，「影響を与えるとき」というのは各パスでの到達条件のORを取ればよいとか，assertionで書かれた条件も含めるとか，dominator（通過しなければならない頂点）を使って解析を前後で分割するとか，手続きに対するサマリ辺の作り方とかが説明されている．いわゆるプログラムスライシング技術がベースで，このあたりの手法自体はわりと普通．メソッドの多態性なんかも，とりうるサブクラスを調べてきて，((a instanceof A) -> PC_for_M_A ) ∧((a instanceof B)-> PC_for_M_B)のように述語をつないでいくだけで表現することができる．

こうやって計算を進めていくと， Path Condition として長々とした条件節が出てきてしまうので，定理証明系(であってるのかな？)で条件節を簡単化していく．実験結果とかを見てると，「P行目での変数xの値がaになっていて，かつQ行目でyになっていて，…」というような条件式がだらだらと並んだ形になる様子．条件式を読み解くのに知識は必要だが，それほど大変でもないというような書き方はされていた．また，セキュリティ解析では，重要情報の危険な変数への到達可能性が充足不能であることさえ示せればよいので，あまり気にしなくても良いのかもしれない，とも思う．

この手法の良いところは，関数単位で独立に処理できるように規定されていることと，PC(x,y) は x から y に情報流が発生するために少なくとも必要な条件であること（十分な条件とは限らない）．メソッド呼び出し階層が深いときなどは，途中で探索を打ち切ってしまっても，「少なくともこれだけ成り立ってたら，情報流が発生する可能性があります」と情報を出すことができる．探索を途中で打ち切ると，条件が弱くなってしまうぶん（冗長な条件を出すことはない），充足不能性とかを示そうとすると大変になる．しかし，プログラム理解などの他の場面では，コールグラフ上で近い階層だけをざっと調べて大雑把な到達条件を見る，といった使い方もできるかもしれない．

この人々，dynamic な手法（実際にどの条件式の影響を受けたかを調べる）というのも Dynamic Path Conditions in Depndence Graphs (PEPM2006) という論文で発表する様子．けっこうがんばっている．