Masters Theses
Keywords and Phrases
Checker of Persistent Security (CoPS); Security Process Algebra (SPA)
Abstract
"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.
Advisor(s)
McMillin, Bruce M.
Committee Member(s)
Chellappan, Sriram
Miller, Ann K.
Department(s)
Computer Science
Degree Name
M.S. in Computer Science
Publisher
Missouri University of Science and Technology
Publication Date
Spring 2009
Pagination
viii, 37 pages
Note about bibliography
Includes bibliographical references (pages 127-128).
Rights
© 2009 Ravi Chandra Akella, All rights reserved.
Document Type
Thesis - Open Access
File Type
text
Language
English
Subject Headings
Computer networks -- Security measures -- DesignComputer security
Thesis Number
T 9477
Print OCLC #
436059857
Electronic OCLC #
318539847
Recommended Citation
Akella, Rav, "Information flow properties for cyber-physical systems" (2009). Masters Theses. 4657.
https://scholarsmine.mst.edu/masters_theses/4657