Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

13

TPHOL
2005
IEEE

favoriteEmaildiscussreport

116views Automated Reasoning» more TPHOL 2005»

Verifying a Secure Information Flow Analyzer

13 years 10 months ago

Verifying a Secure Information Flow Analyzer

Download www.cs.stevens.edu

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 ﬂow for this language is proved correct, that is, it enforces noninterference.

David A. Naumann

Real-time Traffic

Artificial Intelligence | Deep Embedding | Denotational Semantics | Substantial Fragment | TPHOL 2005 |

claim paper

Related Content

» An Information Flow Verifier for Small Embedded Systems

» Flexible SchedulerIndependent Security

» Java Bytecode Dependence Analysis for Secure Information Flow

» Securing electronic health records without impeding the flow of information

» Crafting a usable microkernel processor and IO system with strict and provable information...

» Modeling and analyzing security protocols in SAM A case study

» Formally verifying information flow type systems for concurrent and thread systems

» Quantitative Analysis of Secure Information Flow via Probabilistic Semantics

» Analyzing Information Flow in JavaScriptBased Browser Extensions

Post Info
More Details (n/a)

Added	25 Jun 2010
Updated	25 Jun 2010
Type	Conference
Year	2005
Where	TPHOL
Authors	David A. Naumann

Comments (0)