Saluki: finding taint style vulnerabilities with static property checking

We present Saluki, a new tool for checking taintstyle (data dependence) security properties in binary code. Saluki provides a domain specific language for expressing taint-based policies. Saluki can find vulnerabilities in real programs for a number of CWE types, including those for command injection, weak PRNG seeds, and missing sanitization checks such as SQL escape routines or checks on buffer lengths. Saluki includes two new ideas in binary program analysis. First, Saluki uses µflux, a new static analysis technique for path-sensitive, contextsensitive recovery of data dependence facts in binaries. Second, Saluki introduces a sound logic system for reasoning over data dependence facts. We develop a domain-specific language on top of our logic system to express security properties as formal specifications. Saluki includes a decidable solver procedure to prove (based on the underlying logic) whether a set of data dependence facts satisfy a security property. Our evaluation shows that Saluki is capable of finding vulnerabilities in COTS x86, x86-64, and ARM software, including 0-days