<< Changing Programs Correctly: Refactoring with Specifications | ホーム | Using CafeOBJ to Mechanise Refactoring Proofs and Application >>

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"

タグ : ,



コメント追加 トラックバック送信