Low-Level Library Analysis and Summarization

Programs typically make extensive use of libraries, including dynamically linked libraries, which are often not available in source-code form, and hence not analyzable by tools that work at source level (i.e., that analyze intermediate representations created from source code). A common approach is to write library models by hand. A library model is a collection of function stubs and variable declarations that capture some aspect of the library code’s behavior. Because these are hand-crafted, they are likely to contain errors, which may cause an analysis to return incorrect results. This paper presents a method to construct summary information for a library function automatically by analyzing its low-level implementation (i.e., the library’s binary).

• Type: Conference
• Year: 2007
• Where: CAV
• Authors: Denis Gopan, Thomas W. Reps
• Keywords: CAV 2007, Formal Methods, Library Code Behavior, Library Function, Library Model