Title: Symbolic object code analysis
Authors: Mühlberg, Jan Tobias ×
Lüttgen, Gerald #
Issue Date: 2010
Publisher: Springer
Conference: SPIN 2010 location:Enschede, The Netherlands
Abstract: Current 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 paper
introduces an alternative 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. 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 source-code model checkers and
scales well when applied to real operating systems code
and pointer safety issues.
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Non-KU Leuven Association publications
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
spin-2010.pdfMain article Published 474KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science