An Automata Based Approach for Verifying Information Flow Properties |
| |
Authors: | Deepak D'Souza KR Raghavendra Barbara Sprick |
| |
Affiliation: | Department of Computer Science and Automation, Indian Institute of Science, Bangalore, India |
| |
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. |
| |
Keywords: | information flow control verification finite state systems |
本文献已被 ScienceDirect 等数据库收录! |
|