Sciweavers

Share
TPHOL
2005
IEEE

Verifying a Secure Information Flow Analyzer

10 years 3 months ago
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.
David A. Naumann
Added 25 Jun 2010
Updated 25 Jun 2010
Type Conference
Year 2005
Where TPHOL
Authors David A. Naumann
Comments (0)
books