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"