ARCHER: using symbolic, path-sensitive analysis to detect memory access errors

Memory corruption errors lead to non-deterministic, elusive crashes. This paper describes ARCHER (ARray CHeckER) a static, effective memory access checker. ARCHER uses path-sensitive, interprocedural symbolic analysis to bound the values of both variables and memory sizes. It evaluates known values using a constraint solver at every array access, pointer dereference, or call to a function that expects a size parameter. Accesses that violate constraints are flagged as errors. Those that are exploitable by malicious attackers are marked as security holes. We carefully designed ARCHER to work well on large bodies of source code. It requires no annotations to use (though it can use them). Its solver has been built to be powerful in the ways that real code requires, while backing off on the places that were irrelevant. Selective power allows it to gain efficiency while avoiding classes of false positives that arise when a complex analysis interacts badly with statically undecidable program...

• Type: Conference
• Year: 2003
• Where: SIGSOFT
• Authors: Yichen Xie, Andy Chou, Dawson R. Engler
• Keywords: Memory Corruption Errors, Paper Describes Archer, Practice Archer, SIGSOFT 2003, Software Engineering