SAFECode project aims at providing memory safety guarantees to programs written in unsafe languages like C and C++.
As a part of this project, we developed a relatively simple
compilation strategy that for standard C programs guarantees sound
semantics for an aggressive interprocedural pointer analysis (or
simpler ones), a call graph, 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. A technical report
on this work is available from here
Second, we developed a backwards-compatible run-time array bounds
checking solution that has very low overhead. More information on this
work is available from
here
Finally, we also developed a novel technique that can detect dangling pointer errors (accesses to freed memory) with low over head in some applications. More information on this work is available here
This project is sponsored by the NSF Embedded Systems program under award CCR-02-09202 and in part by an NSF CAREER award, EIA-0093426 and ONR, N0004-02-0102.