KIT | KIT-Bibliothek | Impressum | Datenschutz

Efficient Path Conditions in Dependence Graphs for Software Safety Analysis

Snelting, Gregor; Robschink, Torsten; Krinke, Jens

Abstract:
A new method for software safety analysis is presented which uses program slicing and constraint solving to construct and analyze path conditions, conditions defined on a program's input variables which must hold for information flow between two points in a program. Path conditions are constructed from subgraphs of a program's dependence graph, specifically, slices and chops. The article describes how constraint solvers can be used to determine if a path condition is satisfiable and, if so, to construct a witness for a safety violation, such as an information flow from a program point at one security level to another program point at a different security level. Such a witness can prove useful in legal matters.
The article reviews previous research on path conditions in program dependence graphs; presents new extensions of path conditions for arrays, pointers, abstract data types, and multithreaded programs; presents new decomposition formulae for path conditions; demonstrates how interval analysis and BDDs (binary decision diagrams) can be used to reduce the scalability problem for path conditions; and presents case studies illust ... mehr


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Zeitschriftenaufsatz
Jahr 2006
Sprache Englisch
Identifikator ISSN: 1049-331X
KITopen ID: 1000017666
Erschienen in ACM Transactions on Software Engineering and Methodology
Band 15
Heft 4
Seiten 410 - 457
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page