Towards a Semantic-Based Verification Environment for the pi-calculus
π計算のインタプリタと双模倣関係の判定器のプロトタイプを作ったという論文。π計算は名前の代入があって操作的意味論がCCSみたいな「普通」のLTSでは表せなくて、既存のツールが再利用できない。そこで「普通」のLTSで意味論が表せるπ計算の変種を定義して、それをJACKという既存のツール上に実現したらしい。π計算の変種の話は別の論文読んだほうがいいかな。
author="Gianluigi Ferrari and Gianfranco Modoni and Paola Quaglia",
title="{Towards a Semantic-Based Verification Environment for the $\pi$-calculus}",
booktitle="5th Italian Conference on Theoretical Computer Science",
pages="451--465",
year="1995"
Using CafeOBJ to Mechanise Refactoring Proofs and Application
リファクタリングのルールが正しいことの証明を CafeOBJ を使って半自動的に行おうという論文。ROOL という Refinement Calculus をベースにした言語に対し、条件付きの書き換えとしてリファクタリングを定義。その書き換えが正しいことを言語の意味論と補題を使って証明している。第三著者の博論で展開された議論を CafeOBJ を使って再現したみたい。この論文では「メソッド抽出およびインライン化」と「フィールドのカプセル化」が例に挙げられている。
ここで定義されたリファクタリングを行ってもプログラムの結果が変わらないことはわかるけど、なんとなく違和感があるのは意味論が公理系のようなものだからかな。
author="Antonio Carvalho Junior and Leila Silva and Marcio Cornelio",
title="{Using CafeOBJ to Mechanise Refactoring Proofs and Application}",
booktitle="Brazilian Symposium of Formal Methods",
page="32--46",
year="2005"
A Theorem Proving Approach to Analysis of Secure Information Flow
定理証明器を使って情報流解析しようという論文。機密度の低いデータが高いデータに依存しないことを論理式で表して、プログラムが満たしているか定理証明器を使って確かめる。満たしていれば安全な情報流であるといえる。この論文では論理式に Java Card DL (Dynamic Logic) を、定理証明器に KeY を使っている。
author="Adam Darvas and Reiner Haehnle and Dave Sands",
title="{A Theorem Proving Approach to Analysis of Secure Information Flow}",
booktitle="Proceeding of 2nd International Conference on Security in Pervasive Computing",
volume="3450",
series="LNCS",
publisher="Springer",
page="193--209",
year="2005"
Changing Programs Correctly: Refactoring with Specifications
リファクタリング操作がプログラムの振舞いを変更しないことを形式的に保証しようという研究。プログラムの状態を、変数、ヒープ、IO 操作の 3 項組とし、ステートメント単位で状態遷移を定義してプログラムを形式化。リファクタリング操作を、元のプログラムとリファクタリング後のプログラムの対応として定義して、それぞれの IO 操作が同じであれば振舞いが同じであるとする。プログラムの振舞いを IO 操作の列として定義しているのが特徴的。論文では「フィールドの移動」を例として挙げて、リファクタリング操作が IO 操作を変更しないことを示している。
この論文はカンファレンスに投稿された論文で、基になったテクニカルレポートも読まないといけない感じ。190 ページあるけど。
author="Fabian Bannwart and Peter Muellar",
title="Changing Programs Correctly: Refactoring with Specifications",
booktitle="Formal Methods 2006",
publisher="Springer",
volue="4085",
series="LNCS",
pages="492--507",
year="2006"
カンファレンスは今年の 8 月で、プロシーディングはまだ出版されていないので volume と pages は不明。
Downgrading Policies and Relaxed Noninterference
機密度を下げる仕組みを導入した情報流解析に関する論文。従来の手法では機密度は上がりこそすれ下がることはなく、非干渉性は非常に強い性質になっていたため現実的ではなかった。そこで、どのようにすれば機密度を下げる（downgrading）ことができるかその仕様を与え、プログラムがそれを守っているか静的に解析する。仕様をラベルとしてプログラムに付け、型システムにかける。非干渉性は、仕様で与えられたよりも低い機密度を持つデータに影響しないことと緩められる。
author="Peng Li and Steve Zdancewic",
title="{Downgrading Policies and Relaxed Noninterference}",
booktitle="POPL'05",
pages="158--170",
year="2005"
Challenges for Information-flow Security
情報流解析に関する研究は数多くなされているが、なぜ実用化されないのか、何が問題になっているのか、複数存在する要因のうち 3 つのポイントについて議論した論文。
一つ目は既存のインフラ（OSなど）とどのように統合するか、二つ目は現実的でない非干渉性に代わる有用な性質が必要、三つ目はセキュリティポリシーをどのように管理するか。
現実的なセキュリティポリシーは非干渉性モデルには落とし込めないこと、ポリシーにはコーディング時に既にわかるものから実行時までわからないものまで様々なものがあることなど、実用する際の様々な問題を指摘し、情報流解析に関する今後の研究の方向性を示唆している。
情報流解析の既存の研究を調べ始めてすぐに非干渉性が現実には強力すぎることに気付いたし、そのことがちゃんと文書になっていたなという感じ。これらの問題に取り組んでいる研究にも触れていて、この分野の研究を始める時に Sabelfeld and Myers のサーベイ論文と一緒に読むといいかも。
author="Steve Zdancewic",
title="Challenges for Information-flow Security",
booktitle="Proceedings of PLID'04",
year="2004"