Presenter: Mithun Acharya
Advisor(s): Tao Xie
Author(s): Mithun Acharya, Tao Xie, Jun Xu
Graduate Program: Computer Science

Title: Automatic Property Inference via Static Analysis and Model Checking

Abstract: Robustness and security are critical for the dependable operation of software-systems. Many generic and system-specific correctness rules govern the robust and secure operation of software-systems. Manual verification of these rules across all program paths is error prone. Formally specifying them for static verification requires deep system knowledge and is cumbersome. Our research focuses on automatically inferring robustness and security properties directly from the program source code.

Software-systems interact with their environment through interfaces. Improper handling of interface return exceptions cause robustness problems leading to system crashes and security compromises. In traditional robustness testing, different interface exceptions cannot be easily generated. We propose a framework that employs static-analysis to automatically mine interface robustness rules from the program source code. Our static-analyzer infers generic robustness rules for an interface from its usage pattern. These generic robustness rules are translated to re-usable "concrete" properties verifiable by a static-analyzer. The translation uses interface specifications and exceptions mined from the source code through simple data-flow-analysis.

Intra-procedural analysis is sufficient to extract most robustness properties from the source code. But many security properties cut across procedural boundaries. In this research we show how  model-checking can be used to automatically infer such inter-procedural properties. Existing research shows how bugs can be mined from program code by inferring deviant/dominant behavior using statistical pattern analysis. We use this observation with push-down-model-checking and program-slicing to propose an inter-procedural property inference framework.

We are currently implementing our ideas in an existing static-analyzer. As a part of the feasibility study, we manually generate the interface specification database for the widely used POSIX-APIs and write a few generic robustness rules. Using these rules, our framework effectively generates numerous concrete robustness properties for 280 POSIX-APIs. Given these properties, the static-analyzer with our data-flow extensions detected around 200 robustness problems in 10 Redhat-9.0 packages.