Non-interference for a JVM-like language
Gilles Barthe, Tamara Rezk · 2005
We define an information flow type system for a sequential JVM-like language that includes classes, objects, and exceptions. Furthermore, we show that it enforces non-interference. Our work provides, to our best knowledge, the first analysis that has been shown to guarantee non-interference for a realistic low level language.