KIT | KIT-Bibliothek | Impressum | Datenschutz

Efficient Path Conditions in Dependence Graphs for Software Safety Analysis

Snelting, Gregor; Robschink, Torsten; Krinke, Jens


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 illustrating the use of path conditions in safety analysis. ... mehr

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