A certified lightweight non-interference java bytecode verifier

摘要: Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and can be enforced by appropriate type systems. Much previous work systems for noninterference has focused calculi or high-level programming languages, existing low-level languages typically omit objects, exceptions, method calls, and/or do not prove formally soundness system. We define an system sequential JVM-like language includes classes, arrays, exceptions it non-interference. For increased confidence, we have formalized proof in assistant Coq; additional benefit formalization extracted from our certified lightweight bytecode verifier flow. Our provides, to best knowledge, first sound implemented such expressive fragment JVM.