Verifying a Secure Information Flow Analyzer

Abstract. Denotational semantics for a substantial fragment of Java is formalized by deep embedding in PVS, making extensive use of dependent types. A static analyzer for secure information flow for this language is proved correct, that is, it enforces noninterference.

• Type: Conference
• Year: 2005
• Where: TPHOL
• Authors: David A. Naumann
• Keywords: Artificial Intelligence, Deep Embedding, Denotational Semantics, Substantial Fragment, TPHOL 2005