Sciweavers

Share
SPC
2005
Springer

A Theorem Proving Approach to Analysis of Secure Information Flow

10 years 19 days ago
A Theorem Proving Approach to Analysis of Secure Information Flow
Abstract. Most attempts at analysing secure information flow in programs are based on domain-specific logics. Though computationally feahese approaches suffer from the need for abstraction and the high cost of building dedicated tools for real programming languages. We recast the information flow problem in a general program logic rather than a problem-specific one. We investigate the feasibility of this approach by showing how a general purpose tool for software verification can be used to perform information flow analyses. We are able to prove security and insecurity of programs including advanced features such as method calls, loops, and object types for the target language Java Card. In addition, we can express declassification of information.
Ádám Darvas, Reiner Hähnle, Dav
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SPC
Authors Ádám Darvas, Reiner Hähnle, David Sands
Comments (0)
books