Efficient Strong Updates For Path Sensitive Data Dependence Analysis

Path-sensitive data dependence analysis is a powerful technique widely used in static vulnerability detection. One of the central challenges is how to resolve indirect data dependencies induced by pointer operations: the value loaded from a memory location may depend on different values stored before. Resolving indirect data dependencies in a path-sensitive manner significantly improves the analysis precision, but also induces high overhead that limits its scalability.

We observe that much of the computation effort in path-sensitive data dependence analysis is spent on performing strong updates during load-store matching: a stored value propagates to a load statement only if it is not overwritten by other values stored to the same memory location during the propagation. Answering this question path-sensitively is extremely challenging and often leads to a state explosion that precludes efficient static analysis.

To improve the efficiency for performing strong updates in pathsensitive data dependence analysis, our key insight is that the relation among multiple store statements could be determined in stages: most of the easy cases are handled efficiently by inferring a must-kill relation among the heap store statements, reserving the computationally expensive path-sensitive analysis for the rest. We design a tree-like data structure to encode both the control flow and alias information, which incrementally updates the relation during the analysis. Experiments have shown significant speed-ups and improved state coverage in static analysis through the algorithmic improvements of path-sensitive strong updates.

• Software and its engineering → Software verification and validation.