KIT | KIT-Bibliothek | Impressum

Quantifier Elimination and Information Flow Control for Software Security

Snelting, Gregor

Program Dependency Graphs and Constraint Solving can be combined to achieve a powerful tool for information flow control, allowing to check source code for security problems such as external manipulation of critical computations. The method generates path conditions for critical informa-tion flows, being conditions over the program variables necessary for flow. As all variables are existentially quantified, quantifier elimination and in particular the REDLOG system developed at Volker Weispfenning s group, are used to solve path conditions for the input variables, thus generating witnesses for security leaks.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Proceedingsbeitrag
Jahr 2005
Sprache Englisch
Identifikator ISBN: 3-8334-2669-1
KITopen ID: 1000017654
Erschienen in Algorithmic Algebra and Logic - Proceedings of the A3L 2005, April 3 - 6, Passau, Germany; Conference in honor of the 60th birthday of Volker Weispfenning. Ed.: A. Dolzmann
Verlag Books on Demand, Norderstedt
Seiten 237 - 242
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page