It’s been a busy day. http://www.phrack.org/issues.html?issue=64&id=8 describes several methods of finding bugs using static analysis. It talks at one point about path insensitive interval analysis. Interval analysis tries to discover the potential range or interval(s) a particular variable might have. Path insensitive means that the interval it generates for a particular variable is quite conservative and contains values that would otherwise not be included if specific execution paths are taken into account.
Register Tracking is what Zynamics calls what appears to be taint analysis. http://www.zynamics.com/downloads/csw09-slides.pdf talks about it. It starts by tracking a particular register, and all other registers that are influenced by it. I think this would be the basis for a (forward) program slice, but my knowledge of program slicing is pretty limited. Slicing is all about finding instructions that are dependant or resultant of a particular source instruction.
The Zynamics slides above also talks about MonoREIL, which implements a dataflow analysis framework. The basis for most dataflow analysis is founded around such formal constructs as monotonic functions and partially ordered lattices. The original dataflow analysis model, is that each particular node has a set of dataflow equations, and the analysis tries to arrive at a solution for the equations. To arrive at a solution, there are specific restrictions on the types of equations that can be analysed. They need to be monotonic and they should be finite (excuse my simple and probably incorrect explanations). The solution is derived typically through an iterative fixed-point algorithm. The fixed point part is basically saying that after a particular number of iterations of analysis and applying the dataflow equations, the result stops changing, and this particular fixed point is the solution you want. The monotonicity and the finite ceiling means that a fixed point solution always occurs.
I’m not the strongest in the theory, but none the less, as I posted sometime last week or so, I implemented a dataflow analysis framework on top of my IR (intermediate representation). I used this framework to implement classic dataflow analysis such as reaching definitions and live variable analysis. Today, I implemented interval analysis and register tracking. I’m not convinced the interval analysis is working 100% so I’ll have to spend some more time looking over the results. Interval analysis is not well suited to many of my IR instructions such as bitwise arithmetic (logical, shifts and rotates), but it is still worth applying in any case.
Zynamics also describes what they call “Range Tracking” to find negatively indexed arrays. This is something I haven’t grasped yet but I’ll certainly go over it again and try an implementation in the future.