netail.net

_ AOSD ▲

registration 確認の FAX の送信に失敗するなーと思ったら書いている番号が間違っていたらしい．ひどい話だ．

_ 風邪でダウンしてました ▲

PPL2005から戻って以来約一週間ダウンして，ようやく復帰．日本で会わないけれどAOSDで会うかもしれなかった人には申し訳ないことをしました．

_ tDiary に移行してみました． ▲

トラックバック使いたさに tDiary，実際に使ってみると，書式に関するサービスは貧弱な印象で，いっぱいあるプラグインも，単に ERb で後からHTMLを色々挿入できるからいいよね，というだけに聞こえるのがいまいち…．

前の日記にあってこっちにないものが，スケジュール記録とキーワード検索．キーワード検索がないと，過去にたまった論文情報がまったく使い物にならなくなってしまう．最大の問題は，「コンテンツのフィルタリング」部分がプラグイン機構になっていないので拡張できない，ことのような気が．namazuみたいな全文検索では，実際，論文には特殊用語が多く出現するので分かち書き失敗してうまく検索できなくなったりするので，個別CGIで外部インタフェースでtDiaryソースを処理して検索結果（このスタイルに合わせたインタフェースで）提供するのが正しいあり方？

_ 過去の日記． ▲

過去の論文の情報など，丸ごと変換してみました．過去にいただいたコメントは全部変換途中ですっ飛ばしています．

また，文章の構造として認識される要素がtDiaryでは違うので，一部うまくいっていないところもあるかもしれません．古い日記はそれはそれで残しておくので，変だなーと思ったらオリジナル側を参照してください．

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

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) という論文で発表する様子．けっこうがんばっている．

_ [近況] 研究室移転 ▲

今日から３日間かけて，新しい建物へ移転します．メールサーバもネットワーク機器も電話も取り外すので，外部との連絡はほとんどできなくなります．

何か重要な連絡が必要なイベントが入ってるわけではないので（SIGSEとは日程が重なっていますが），あまり影響はないと信じています．