Deriving an Information Flow Checker and Certifying Compiler for Java
高レベル言語（Java とか）に対する情報流解析のための型システムと、低レベル言語（バイトコードとか）に対する情報流解析のための型システムを結び付けようという論文。高レベル言語と低レベル言語の命令間の対応はコンパイルの定義として与えられるけど、型システムでも対応をとらなければいけない。そこで、制御が分岐するポイントにラベルをつけて、それぞれのポイントにおけるセキュリティレベルも扱えるような型システムを定義する。そして、高レベル用、低レベル用それぞれの型システムと新しい型システムの対応を与える。論文は対応を与えるという形で書いてあるけど、実際に活用する時は低レベルに対する型システムから高レベル言語に対する型システムを導出するという使い方になるような気がする。
author="Gilles Barthe and David Naumann and Tamara Rezk",
title="Deriving an Information Flow Checker and Certifying Compiler for Java",
booktitle="Proceedings of the 2006 IEEE Symposium of Security and Privacy",
publisher="IEEE Computer Society",
pages="230--242,
year="2006"