Verifying a secure information flow analyzer

Research output: Contribution to journalConference articlepeer-review

13 Scopus citations

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.

Original languageEnglish
Pages (from-to)211-226
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3603
DOIs
StatePublished - 2005
Event18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2005 - Oxford, United Kingdom
Duration: 22 Aug 200525 Aug 2005

Fingerprint

Dive into the research topics of 'Verifying a secure information flow analyzer'. Together they form a unique fingerprint.

Cite this