A practical approach to formal software verification by static analysis
Abstract
Static analysis by Abstract Interpretation is a promising way for conducting formal verification of large software applications. In spite of recent successes in the verification of aerospace codes, this approach has limited industrial applicability due to the level of expertise required to engineer static analyzers. In this paper we investigate a pragmatic approach that consists of focusing on the most critical components of the application first. In this approach the user provides a description of the usage of functionalities in the critical component via a simple specification language, which is used to drive a fully automated static analysis engine. We present experimental results of the application of this approach to the verification of absence of buffer overflows in a critical library of the OpenSSH distribution.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Apr 01, 2008
- Source ID
- 10.1145/1387830.1387836
Entities
People
- Arnaud Venet
Organizations
- Office of the Secretary of Defense