Mining interface specifications for generating checkable robustness properties

A software system interacts with its environment through interfaces. Improper handling of exceptional returns from system interfaces can cause robustness problems. Robustness of software systems are governed by various temporal properties related to interfaces. Static verification has been shown to be effective in checking these temporal properties. But manually specifying these properties is cumbersome and requires the knowledge of interface specifications, which are often either unavailable or undocumented. In this paper, we propose a novel framework to automatically infer system-specific interface specifications from program source code. We use a model checker to generate traces related to the interfaces. From these model checking traces, we infer interface specification details such as return value on success or failure. Based on these inferred specifications, we translate generically specified interface robustness rules to concrete robustness properties verifiable by static checking. Hence the generic rules can be specified at an abstract level that needs no knowledge of the source code, system, or interfaces. We implement our framework for an existing static analyzer that employs push down model checking and apply the analyzer to the well known POSIX-API system interfaces. We found 28 robustness violations in 10 open source packages using our framework.