Symbolic object code analysis |
| |
Authors: | Jan Tobias Mühlberg Gerald Lüttgen |
| |
Affiliation: | 1. IBBT-DistriNet, KU Leuven, Celestijnenlaan 200A, 3001, ?Leuven, Belgium 2. Software Technologies Research Group, University of Bamberg, 96045, ?Bamberg, Germany
|
| |
Abstract: | Software model checkers quickly reach their limits when being applied to verifying pointer safety properties in source code that includes function pointers and inlined assembly. This article introduces a novel technique for checking pointer safety violations, called symbolic object code analysis (SOCA), which is based on bounded symbolic execution, incorporates path-sensitive slicing, and employs the SMT solver Yices as its execution and verification engine. Extensive experimental results of a prototypic SOCA Verifier, using the Verisec suite and almost 10,000 Linux device driver functions as benchmarks, show that SOCA performs competitively to modern source-code model checkers, scales well when applied to real operating systems code and pointer safety issues, and effectively explores niches of pointer-complex software that current software verifiers do not reach. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|