Model-checking infinite state systems for information flow security

Information flow properties are a way of specifying security properties of systems, dating back to the work of Goguen and Meseguer in the eighties. In this framework, a system is modeled as having high-level (or confidential) events as well as low-level (or public) events, and a typical property requires that the high-level events should not ''influence'' the occurrence of low-level events. In this book we study the problem of model-checking the well-known trace-based and bisimulation-based information flow security properties for some popular classes of infinite-state system models, and state-based information flow properties for programs.

About the author

Raghavendra K. R. completed his Ph.D. from Department of Computer Science and Automation, Indian Institute of Science, Bangalore. His research interests include formal verification, program analysis and information flow security.

Product details

• Authors: Raghavendra K R, Raghavendra K. R.
• Publisher: LAP Lambert Academic Publishing
• Languages: English
• Product format: Paperback / Softback
• Released: 01.01.2014
• EAN: 9783659301315
• ISBN: 978-3-659-30131-5
• No. of pages: 160
• Subjects: Guides; Natural sciences, medicine, IT, technology > IT, data processing > Miscellaneous