Result Details

Byte-Precise Verification of Low-Level List Manipulation

DUDKA, K.; PERINGER, P.; VOJNAR, T. Byte-Precise Verification of Low-Level List Manipulation. 20th Static Analysis Symposium. Lecture Notes in Computer Science. Lecture Notes in Computer Science Volume 7935. Berlin: Springer Verlag, 2013. no. 7935, p. 215-237. ISBN: 978-3-642-38855-2. ISSN: 0302-9743.
Type
conference paper
Language
English
Authors
Dudka Kamil, Ing., DITS (FIT)
Peringer Petr, Dr. Ing., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

We propose a new approach to shape analysis of programs with linked lists that use low-level memory operations. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. Our approach is based on a new representation of sets of heaps, which is to some degree inspired by works on separation logic with higher-order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to support the various low-level memory operations. The approach was implemented in the Predator tool and successfully validated on multiple non-trivial case studies that are beyond the capabilities of other current fully automated shape analysis tools.

Keywords
dynamic linked data structures, separation logic, symbolic memory graphs, list manipulation, low-level memory manipulation, memory safety, shape analysis
Published
2013
Pages
215–237
Journal
Lecture Notes in Computer Science, vol. 20, no. 7935, ISSN 0302-9743
Proceedings
20th Static Analysis Symposium
Series
Lecture Notes in Computer Science Volume 7935
Conference
20th International Static Analysis Symposium -- SAS 2013
ISBN
978-3-642-38855-2
Publisher
Springer Verlag
Place
Berlin
BibTeX
@inproceedings{BUT103494,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Byte-Precise Verification of Low-Level List Manipulation",
  booktitle="20th Static Analysis Symposium",
  year="2013",
  series="Lecture Notes in Computer Science Volume 7935",
  journal="Lecture Notes in Computer Science",
  volume="20",
  number="7935",
  pages="215--237",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-38855-2",
  issn="0302-9743"
}
Projects
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed
Research groups
Departments
Back to top