Highly Automated Formal Proofs over Memory Usage of Assembly Code

F. Verbeek; Joshua Bockenek; Binoy Ravindran

doi:10.1007/978-3-030-45237-7_6

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 proceeding › Conference Article in proceeding › Academic › peer-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 language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	26th 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
Editors	Armin Biere, David Parker
Place of Publication	Cham
Publisher	Springer Open
Chapter	6
Pages	98-117
Number of pages	20
ISBN (Electronic)	9783030452377
ISBN (Print)	9783030452360
DOIs	https://doi.org/10.1007/978-3-030-45237-7_6
Publication status	Published - 2020
Event	(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Dublin, Ireland Duration: 25 Apr 2020 → 30 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

Series	Lecture Notes in Computer Science (LNCS) series
Volume	12079
ISSN	0302-9743

Conference

Conference	(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Abbreviated title	TACAS 2020
Country/Territory	Ireland
City	Dublin
Period	25/04/20 → 30/04/20
Internet address	https://etaps.org/2020/tacas https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf

Keywords

Assembly
Formal Verification
Memory Usage
x86-64

Access to Document

10.1007/978-3-030-45237-7_6Licence: CC BY

Cite this

Verbeek, F., Bockenek, J., & Ravindran, B. (2020). Highly Automated Formal Proofs over Memory Usage of Assembly Code. In A. Biere, & D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 26th 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 (pp. 98-117). Springer Open. https://doi.org/10.1007/978-3-030-45237-7_6

Verbeek, F. ; Bockenek, Joshua ; Ravindran, Binoy. / Highly Automated Formal Proofs over Memory Usage of Assembly Code. Tools and Algorithms for the Construction and Analysis of Systems: 26th 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. editor / Armin Biere ; David Parker. Cham : Springer Open, 2020. pp. 98-117 (Lecture Notes in Computer Science (LNCS) series, Vol. 12079).

@inproceedings{d69f26b79b0746cd922aed11d45c2cb6,

title = "Highly Automated Formal Proofs over Memory Usage of Assembly Code",

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.",

keywords = "Assembly, Formal Verification, Memory Usage, x86-64",

author = "F. Verbeek and Joshua Bockenek and Binoy Ravindran",

year = "2020",

doi = "10.1007/978-3-030-45237-7_6",

language = "English",

isbn = "9783030452360",

series = "Lecture Notes in Computer Science (LNCS) series",

publisher = "Springer Open",

pages = "98--117",

editor = "Armin Biere and David Parker",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "United Kingdom",

note = "(Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020 ; Conference date: 25-04-2020 Through 30-04-2020",

url = "https://etaps.org/2020/tacas, https://link.springer.com/content/pdf/10.1007%2F978-3-030-45237-7.pdf",

}

Verbeek, F, Bockenek, J & Ravindran, B 2020, Highly Automated Formal Proofs over Memory Usage of Assembly Code. in A Biere & D Parker (eds), Tools and Algorithms for the Construction and Analysis of Systems: 26th 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. Springer Open, Cham, Lecture Notes in Computer Science (LNCS) series, vol. 12079, pp. 98-117, (Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Dublin, Ireland, 25/04/20. https://doi.org/10.1007/978-3-030-45237-7_6

Highly Automated Formal Proofs over Memory Usage of Assembly Code. / Verbeek, F.; Bockenek, Joshua; Ravindran, Binoy.
Tools and Algorithms for the Construction and Analysis of Systems: 26th 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. ed. / Armin Biere; David Parker. Cham: Springer Open, 2020. p. 98-117 (Lecture Notes in Computer Science (LNCS) series, Vol. 12079).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Highly Automated Formal Proofs over Memory Usage of Assembly Code

AU - Verbeek, F.

AU - Bockenek, Joshua

AU - Ravindran, Binoy

N1 - Conference code: 26

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Assembly

KW - Formal Verification

KW - Memory Usage

KW - x86-64

U2 - 10.1007/978-3-030-45237-7_6

DO - 10.1007/978-3-030-45237-7_6

M3 - Conference Article in proceeding

SN - 9783030452360

T3 - Lecture Notes in Computer Science (LNCS) series

SP - 98

EP - 117

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Biere, Armin

A2 - Parker, David

PB - Springer Open

CY - Cham

T2 - (Cancelled) 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

Y2 - 25 April 2020 through 30 April 2020

ER -

Verbeek F, Bockenek J, Ravindran B. Highly Automated Formal Proofs over Memory Usage of Assembly Code. In Biere A, Parker D, editors, Tools and Algorithms for the Construction and Analysis of Systems: 26th 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. Cham: Springer Open. 2020. p. 98-117. (Lecture Notes in Computer Science (LNCS) series, Vol. 12079). doi: 10.1007/978-3-030-45237-7_6

Highly Automated Formal Proofs over Memory Usage of Assembly Code

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this