Keywords and Phrases
Checker of Persistent Security (CoPS); Security Process Algebra (SPA)
"In cyber-physical systems, which are the integrations of computational and physical processes, security properties are difficult to enforce. Fundamentally, physically observable behavior leads to violations of confidentiality. This work analyzes certain noninterference based security properties to ensure that interactions between the cyber and physical processes preserve confidentiality. A considerable barrier to this analysis is the representation of physical system interactions at the cyber-level. This thesis presents encoding of these physical system properties into a discrete event system and represents the cyber-physical system using Security Process Algebra (SPA). The model checker, Checker of Persistent Security (CoPS) shows Bisimulation based NonDeducibility on Compositions (BNDC) properties, which are a variant of noninterference properties, to check the system's security against all potential high-level interactions. This work considers a model problem of invariant pipeline flow to examine the BNDC properties and their applicability for cyber-physical systems--Abstract, page iii.
McMillin, Bruce M.
Miller, Ann K.
M.S. in Computer Science
Missouri University of Science and Technology
viii, 37 pages
© 2009 Ravi Chandra Akella, All rights reserved.
Thesis - Open Access
Library of Congress Subject Headings
Computer networks -- Security measures -- Design
Print OCLC #
Electronic OCLC #
Link to Catalog Recordhttp://laurel.lso.missouri.edu/record=b7076656~S5
Akella, Rav, "Information flow properties for cyber-physical systems" (2009). Masters Theses. 4657.