Model checking trace-based information flow properties: For finite state systems and pushdown systems

Kagalavadi Ramesh, Raghavendra, D*Souza, Deepak, Sprick, Bar

ISBN 10: 383837780X / ISBN 13: 9783838377803

Published by LAP LAMBERT Academic Publishing, 2012

About this Item

NEW. SHIPS FROM MULTIPLE LOCATIONS.

Seller Inventory # ERICA829383837780X6

Bibliographic Details

• Title: Model checking trace-based information flow properties: For finite state systems and pushdown systems
• Publisher: LAP LAMBERT Academic Publishing
• Publication Date: 2012
• Language: English
• ISBN 10: 383837780X
• ISBN 13: 9783838377803
• Binding: paperback
• Condition: New
• Book Type: book

About this title

Synopsis

Information flow properties are a way of specifying security properties of systems. A system is viewed as generating traces containing “confidential” and “visible” events (only the latter being observable by a “low-level” user) and the information flow properties specify restrictions on the kind of traces the system may generate, so as to restrict the amount of information a low-level user can infer about confidential events having taken place (or not) in an execution. Mantel identifies "basic security predicates” or BSPs and shows them to be the building blocks of most of the known trace-based properties in the literature. Traditionally BSPs have been reasoned about via unwinding conditions that capture whether a system satisfies a particular BSP. First, we show that the checking of unwinding conditions can be simplified to checking conditions on a maximal simulation relation. Second, we show that the BSPs can be characterized 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. Finally, we prove that the problem of verifying BSPs for pushdown systems is undecidable.

About the Author

Raghavendra obtained Bachelor of Engineering degree from Visveswaraiah Technological University, India. He obtained Master of Science (Engineering) degree for his thesis 'Verification of information flow properties'. Currently he is doing Ph.D. under the supervision of Prof. Deepak D'Souza at Indian Institute of Science.