View article

Some of the most dangerous and exploitable security problems are caused by insufficiently validated user input. This includes command injections, path traversals, and format string flaws which are part of the 2011 CWE/SANS list of the “Top 25 Most Dangerous Software Errors”. These weaknesses have the common characteristic to pass user input obtained from an external source to a vulnerable function without appropriate input validation. I will present a new technique which combines data flow analysis and model checking to find weaknesses of this kind. The data flow analysis tracks the propagation of user input in the program and tags statements which are influenced by it. Model checking is then used in a second step to eliminate false positives and to produce a readable counter-example trace. A summary-based inter-procedural analysis extends the approach to problems which span multiple functions and compilation units. It achieves an average detection rate of 86% for applicable test cases of the Sate IV benchmark. The analysis evaluates 1,000 lines of code in 2.3 to 7 seconds measured on the basis of four large open source projects. My approach is easily extendable to similar weaknesses and is built into the top notch bug finding tool Goanna.