DHTMLにおけるDOMの解析手法
DOM を正規木文法、DOM 操作を top-down tree transducer として表し、JavaScript プログラムによる DOM 操作前後の DOM を得る手法の提案。ショートペーパーのせいなのか、DOM を正規木文法で得た後にどうするかは述べられていない。
author="立石 孝彰 and 宮下 尚 and 小野 康一 and 斉藤 新",
title="{DHTMLにおけるDOMの解析手法}",
booktitle="FOSE 2006",
pages="47--52",
year="2006"
Gradual Typing for Objects
Object Calculus における漸進的型付けの話。漸進的型付けは、型宣言されている部分は静的に検査し、その他の部分は動的に型付けを行う。境界を表す型 ? を導入して型システムを構築。型付けできれば型エラーが発生しないことの健全性は、型が一致するようにキャストが明示的に記述される言語において示し、元言語からの変換の健全性によって間接的に証明。
author="Jeremy Siek and Walid Taha",
title="{Gradual Typing for Objects}",
booktitle="ECOOP 2007",
publisher="Springer",
pages="2--27",
year="2007"
Hiding Program Slices for Software Security
プログラムを不法コピーから守るためには、プログラムの一部を分離して安全なところに置いてそこで実行するといいよねという話。スライシングを使って適度に複雑に分離することで、隠された方の振る舞いをインタラクションを観測しても推測できないようにする。
author="Xiangyu Zhang and Rajiv Gupta",
title="{Hiding Program Slices for Software Security}",
booktitle="CGO'03",
publisher="IEEE Computer Society",
pages="325--336",
year="2003"
Korset: Automated, Zero False-Alarm Intrusion Detection for Linux
制御フローグラフに基づいてシステムコールに着目したオートマトンを作って、それに従っているか検査しながら実行するシステムの提案。話題としてはあまり目新しさはないけど、LSM を使ってそれなりに実装している。
実装の配布元：http://www.korset.org/
author="Ohad Ben-Cohen and Avishai Wool",
title="{Korset: Automated, Zero False-Alarm Intrusion Detection for Linux}",
booktitle="Linux Symposium 2008",
pages="31--38",
year="2008"
動的解析によるWebアプリケーション・モデル抽出支援手法
HTTPリクエスト・レスポンスに着目した動的解析によって Web アプリケーションの振舞いを MVC ベースのモデルとして抽出する手法の提案。HTTP レスポンス中の HTML を類似しているグループに分類、グループ間の遷移関係を解析、開発者が手を加えながら MVC に落とす、の 3 段階。HTTP しか見ないから View の構築もテンプレート抽出、繰り返し発見とかいろいろがんばるみたい。ツールとして実装して実験して有効性を確認。
author="安部 麻里 and 福田 健太郎 and 堀 雅洋 and 田井 秀樹 and 根路銘 崇 and 小野 康一 and 大野 義夫",
title="{動的解析によるWebアプリケーション・モデル抽出支援手法}",
journal="情報処理学会論文誌",
volumn="46",
number="3",
pages="683--693",
year="2005"
Combining Type-Based Analysis and Model Checking for Finding Counterexamples Against Non-Interference
情報流解析のための型システムで型が付かなかったプログラムが本当に危ないのかモデル検査によって確認するという論文。検査すべきパスを見つけたり枝刈りしたりアルゴリズムがちゃんと提案されていて、C 言語のサブセットに対して実験している。
author="Hiroshi Unno and Naoki Kobayashi and Akinori Yonezawa",
title="{Combining Type-Based Analysis and Model Checking for Finding Counterexamples Against Non-Interference}",
booktitle="PLAS'06",
publisher="ACM",
pages="17--26",
year="2006"
Typestate: A Programming Language Concept for Enhancing Software Reliability
変数の型だけでなく、宣言されただけなのか、領域が割り当てられ たのか、値が代入されたのか、といった状態まで追いかけることでプログラムを安全にしようという論文。「状態」を typestate と言って、いわゆる状態遷移系として定義する。あとはプログラムの制御フローにしたがって typestate の変化を追いかけて、変な状況になったらそのプログラムはよろしくないと判断する。考え方は面白いと思うから、応用を探したい。
author="Robert E. Strom and Shaula Yemini",
title="{Typestate: A Programming Language Concept for Enhancing Software Reliability}",
journal="IEEE Transactions on Software Engineering",
volumn="12",
number="1",
pages="157--171",
year="1986"