Effective generation of interface robustness properties for static analysis

Mithun Acharya, Tanu Sharma, Xu Jun, Xie Tao

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A software system interacts with its environment through system interfaces. Robustness of software systems are governed by various temporal properties related to these interfaces, whose violation leads to system crashes and security compromises. These properties can be formally specified for system interfaces and statically verified against a software system. But manually specifying a large number of interface properties for static verification is often inaccurate or incomplete, apart from being cumbersome. In this paper, we propose a novel framework that effectively generates interface properties for static checking from a few generic, high level robustness rules that capture interface behavior. We implement our framework for an existing static analyzer with simple data flow extensions and apply it on POSIX-API system interfaces used in 10 Redhat-9.0 open source packages. The results show that the framework can effectively generate a large number of useful interface properties from a few generically specified rules.

Original languageEnglish (US)
Title of host publicationProceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006
Pages293-296
Number of pages4
DOIs
StatePublished - 2006
Externally publishedYes
Event21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006 - Tokyo, Japan
Duration: Sep 18 2006Sep 22 2006

Publication series

NameProceedings - 21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006

Other

Other21st IEEE/ACM International Conference on Automated Software Engineering, ASE 2006
Country/TerritoryJapan
CityTokyo
Period9/18/069/22/06

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Effective generation of interface robustness properties for static analysis'. Together they form a unique fingerprint.

Cite this