IKOS: Sound Static Program Analysis

Arthaud, Maxime

关键词: C++ (PROGRAMMING LANGUAGE);    COST ANALYSIS;    ERROR ANALYSIS;    KERNEL FUNCTIONS;    PROGRAM VERIFICATION (COMPUTERS);    RUN TIME (COMPUTERS);    SOFTWARE RELIABILITY;    SYSTEMS ANALYSIS;   

RP-ID  :  ARC-E-DAA-TN74038

美国|英语

来源: NASA Technical Reports Server

【 摘 要 】

IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. It can detect or prove the absence of runtime errors (e.g, buffer overflows, integer overflows, null pointer dereferences, etc.) in the source code. IKOS uses Abstract Interpretation techniques to compute an over-approximation of all the reachable states of the program, thus it cannot miss a bug. In this talk, I will give an overview of the tool, then show how to apply it to a large software. I will present ikos-view, a web interface to examine the analysis results. I will discuss about methods to improve the analysis, such as adding code annotations, modeling library functions, and avoiding specific code patterns.