Hinweis zum Urheberrecht
Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bvb:473-opus-2364
URL: http://www.opus-bayern.de/uni-bamberg/volltexte/2010/236/
Symbolic Object Code Analysis
Mühlberg, Jan Tobias ;
Lüttgen, Gerald
| Beteiligte Einrichtung: |
| Fakultät Wirtschaftsinformatik und Angewandte Informatik |
| Dokumentart: |
| Report (Bericht) |
| Schriftenreihe: |
| Bamberger Beiträge zur Wirtschaftsinformatik und Angewandten Informatik |
| Bandnummer: |
| 85 |
| DDC-Sachgruppe: |
| Informatik |
| RVK - Regensburger Verbundklassifikation: |
| ST 233 |
| SWD-Schlagwörter: |
| Programmcode ; Zeiger |Informatik| ; Konsistenzprüfung ; Programmtest ; Online-Publikation |
| Freie Schlagwörter (Englisch): |
| bounded model checking , symbolic execution , program slicing , object code analysis , linux device drivers |
| Sprache: |
| Englisch |
| Erstellungsjahr: |
| 2010 |
| Publikationsdatum: |
| 09.03.2010 |
| Beschreibung auf Englisch: |
| Current software model checkers quickly reach their limit 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. 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 current source-code model checkers and that it also scales well when applied to real operating systems code and pointer safety issues. SOCA effectively explores semantic niches of software that current software verifiers do not reach. |
Universitätsbibliothek Bamberg ·
Feldkirchenstraße 21 · 96052 Bamberg
Tel. (0951) 863 1568 · Fax (0951) 863 1565 ·
E-Mail
opus.ub(at)uni-bamberg.de
Letzte Änderung:
17.12.09
|
