Masters Theses

Rav Akella

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 -- Design
Computer security

Thesis Number

T 9477

Print OCLC #

436059857

Electronic OCLC #

318539847

Download

Share

 
COinS