Quantifier Elimination and Information Flow Control for Software Security.
Gregor Snelting · 2005
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 information 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. 1