Quantifier Elimination and Information Flow Control for Software Security

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.