Dependence analysis for inferring information flow properties in Spark ADA programs

K-REx Repository

Show simple item record

dc.contributor.author Thiagarajan, Hariharan
dc.date.accessioned 2011-12-01T14:00:32Z
dc.date.available 2011-12-01T14:00:32Z
dc.date.issued 2011-12-01
dc.identifier.uri http://hdl.handle.net/2097/13187
dc.description.abstract With the increase in development of safety and security critical systems, it is important to have more sophisticated methods for engineering such systems. It can be difficult to understand and verify critical properties of these systems because of their ever growing size and complexity. Even a small error in a complex system may result in casualty or significant monetary loss. Consequently, there is a rise in the demand for scalable and accurate techniques to enable faster development and verification of high assurance systems. This thesis focuses on discovering dependencies between various parts of a system and leveraging that knowledge to infer information flow properties and to verify security policies specified for the system. The primary contribution of this thesis is a technique to build dependence graphs for languages which feature abstraction and refinement. Inter-procedural slicing and inter-procedural chopping are the techniques used to analyze the properties of the system statically. The approach outlined in this thesis provides a domain-specific language to query the information flow properties and to specify security policies for a critical system. The spec- ified policies can then be verified using existing static analysis techniques. All the above contributions are integrated with a development environment used to develop the critical system. The resulting software development tool helps programmers develop, infer, and verify safety and security systems in a single unified environment. en_US
dc.language.iso en_US en_US
dc.publisher Kansas State University en
dc.subject Information flow en_US
dc.subject Dependence graph en_US
dc.subject Policy language en_US
dc.subject Specification and verification en_US
dc.title Dependence analysis for inferring information flow properties in Spark ADA programs en_US
dc.type Thesis en_US
dc.description.degree Master of Science en_US
dc.description.level Masters en_US
dc.description.department Department of Computing and Information Sciences en_US
dc.description.advisor John Hatcliff en_US
dc.subject.umi Computer Science (0984) en_US
dc.date.published 2011 en_US
dc.date.graduationmonth December en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search K-REx


Advanced Search

Browse

My Account

Statistics








Center for the

Advancement of Digital

Scholarship

118 Hale Library

Manhattan KS 66506


(785) 532-7444

cads@k-state.edu