An Automata Based Approach for Verifying Information Flow Properties Export

@article{DSouza05, 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.}, author = {D'Souza, Deepak and Raghavendra, K. R. and Sprick, Barbara}, citeulike-article-id = {6042096}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.entcs.2005.06.005}, citeulike-linkout-1 = {http://linkinghub.elsevier.com/retrieve/pii/S1571066105050516}, day = {5}, doi = {10.1016/j.entcs.2005.06.005}, issn = {1571-0661}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {2005, automata, information-flow, maks, model-checking, security, unwinding, verification}, month = {July}, number = {1}, pages = {39--58}, posted-at = {2009-10-30 10:34:52}, priority = {2}, title = {An Automata Based Approach for Verifying Information Flow Properties}, url = {http://dx.doi.org/10.1016/j.entcs.2005.06.005}, volume = {135}, year = {2005} }

TY - JOUR ID - DSouza05 L3 - citeulike-article-id:6042096 N2 - 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. IS - 1 JF - Electronic Notes in Theoretical Computer Science SN - 1571-0661 EP - 58 TI - An Automata Based Approach for Verifying Information Flow Properties VL - 135 SP - 39 KW - 2005 KW - automata KW - information-flow KW - maks KW - model-checking KW - security KW - unwinding KW - verification AU - D’Souza, Deepak AU - Raghavendra, KR AU - Sprick, Barbara PY - 2005/07/05/ UR - http://dx.doi.org/10.1016/j.entcs.2005.06.005 ER -