A Theorem Proving Approach to Analysis of Secure Information Flow


 Authors: Adam Darvas and Reiner Hähnle and Dave Sands

----------------------------------------------------------


  Most attempts at analysing secure information flow in programs are
  based on domain-specific logics. Though computationally feasible,
  these 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 handle phenomena like method calls, loops, and object
  types for the target language Java Card. We are also able to prove
  insecurity of programs.