An Automata Based Approach for Verifying Information Flow Properties
Deepak D'Souza, Raghavendra K. R., Barbara Sprick
IISc-CSA-TR-2005-4
(April 2005) Available formats: [ps] [ps.gz] [pdf]
Filed on April 25, 2005
Updated on April 26, 2005
We present an automated verification technique to verify trace based
information flow properties for finite state systems.
We show that the Basic Security Predicates (BSPs) defined by Mantel in
[Mantel:2000a], which are shown to be the building blocks of known
trace based information flow properties, can be characterised in
terms of regularity preserving language theoretic operations. This
leads to a decision procedure for checking whether a finite state
system satisfies a given BSP.
Verification techniques in the literature (e.g. unwinding) are based on the structure
of the transition system and are incomplete in some cases. In contrast,
our technique is language based and complete for all information flow
properties that can be expressed in terms of BSPs.
Please bookmark this technical report as http://aditya.csa.iisc.ernet.in/TR/2005/4/.Problems ? Contact techrep@csa.iisc.ernet.in
[Updated at 2009-10-22T06:42Z]