Abstract

Computer systems handle secret data such as passwords. To check that programs do not leak information about such data, static program analysis called information flow analysis has been studied for high-level programming languages. The purpose of this study is to establish a type-based method for information flow analysis for low-level languages such as assembly languages and virtual machine languages, so that information flow analysis can be performed even if source programs do not exist. Taking a subset of the Java virtual machine language as a target language, we formalize a type system for information flow analysis and prove its correctness.