Name
Abstract | ||
|---|---|---|
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, H., Possibilistic Definitions of Security - An Assembly Kit, in: Proceedings of the 13th IEEE Computer Security Foundations Workshop (2000), pp. 185-199], 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. |
Year | DOI | Venue |
|---|---|---|
2005 | 10.1016/j.entcs.2005.06.005 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
information flow property,ieee computer security foundations,information flow control,automated verification technique,known trace,finite state system,assembly kit,finite state systems,language theoretic operation,verification,basic security predicates,transition system,verifying information flow properties,verification technique,computer security,satisfiability,information flow | Transition system,Information flow (information theory),Programming language,Computer science,Automaton,Finite state,Theoretical computer science,Finite state systems,Predicate (grammar) | Journal |
Volume | Issue | ISSN |
135 | 1 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
8 | 0.52 | 8 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Deepak D'souza | 1 | 239 | 17.90 |
| K. R. Raghavendra | 2 | 17 | 1.71 |
| Barbara Sprick | 3 | 74 | 7.27 |