Highly Automated Formal Proofs over Memory Usage of Assembly Code

F. Verbeek*, Joshua Bockenek, Binoy Ravindran

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference article in proceedingAcademicpeer-review

Abstract

We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020, Proceedings, Part II
EditorsArmin Biere, David Parker
Place of PublicationCham
PublisherSpringer Open
Chapter6
Pages98-117
Number of pages20
ISBN (Electronic)9783030452377
ISBN (Print)9783030452360
DOIs
Publication statusPublished - 2020
Event(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020
Conference number: 26
https://etaps.org/2020/tacas
https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf

Publication series

SeriesLecture Notes in Computer Science (LNCS) series
Volume12079
ISSN0302-9743

Conference

Conference(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated titleTACAS 2020
CountryIreland
CityDublin
Period25/04/2030/04/20
Internet address

Fingerprint Dive into the research topics of 'Highly Automated Formal Proofs over Memory Usage of Assembly Code'. Together they form a unique fingerprint.

Cite this