Enforcing Alias Analysis for Weakly Typed Languages

Static analysis of programs in weakly typed languages such as C and C++ generally is not guaranteed to be sound because programs in these languages may have undetected memory errors such as dangling pointer references, references using uninitialized pointers, and array bounds overflow. Optimizing compilers can produce undefined results for programs with memory access errors, but this is quite undesirable for many tools that aim to analyze security and reliability properties with guarantees of soundness. We describe a relatively simple compilation strategy for standard C programs that guarantees sound semantics for a call graph, an aggressive interprocedural pointer analysis, and type information for a subset of memory. These provide the foundation for sophisticated static analyses to be applied to such programs with a guarantee of soundness. Our work builds on a previously published transformation called Automatic Pool Allocation to ensure that hard-to-detect memory errors (dangling pointer references and certain array bounds errors) cannot invalidate the call graph, points-to information or type information. The key insight behind our approach is that pool allocation can be used to create a run-time partitioning of memory that matches the compile-time memory partitioning in a points-to graph, and efficient checks can be used to isolate the run-time partitions. Furthermore, we show that the sound analysis information enable static checking techniques that reliably eliminate many run-time checks. Our approach requires no source code changes, allows memory to be managed explicitly, and do not use meta-data on pointers or individual tag bits for memory thus avoiding any external library compatibility issues. Using many benchmarks and system codes, we show experimentally that the run-time overheads are low (less than 10% in nearly all cases and 30% in the worst case we have seen). We also show the effectiveness of reliable static analyses for eliminating run-time checks