Formally verified lifting of C-compiled x86-64 binaries

Freek Verbeek; Joshua Bockenek; Zhoulai Fu; Binoy Ravindran

doi:10.1145/3519939.3523702

Formally verified lifting of C-compiled x86-64 binaries

Freek Verbeek, Joshua Bockenek, Zhoulai Fu, Binoy Ravindran

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

Abstract

Lifting binaries to a higher-level representation is an essential step for decompilation, binary verification, patching and security analysis. In this paper, we present the first approach to provably overapproximative x86-64 binary lifting. A stripped binary is verified for certain sanity properties such as return address integrity and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an overapproximation of all possible execution paths of the binary. The lifted representation contains disassembled instructions, reconstructed control flow, invariants and proof obligations that are sufficient to prove the sanity properties as well as correctness of the lifted representation. We apply this approach to Linux Foundation and Intel's Xen Hypervisor covering about 400K instructions. This demonstrates our approach is the first approach to provably overapproximative binary lifting scalable to commercial off-the-shelf systems. The lifted representation is exportable to the Isabelle/HOL theorem prover, allowing formal verification of its correctness. If our technique succeeds and the proofs obligations are proven true, then - under the generated assumptions - the lifted representation is correct.

Original language	English
Title of host publication	PLDI 2022
Subtitle of host publication	Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
Editors	Ranjit Jhala, Isil Dillig
Publisher	Association for Computing Machinery
Pages	934-949
Number of pages	16
ISBN (Print)	978-1-4503-9265-5
DOIs	https://doi.org/10.1145/3519939.3523702
Publication status	Published - 9 Jun 2022
Event	43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022 - Virtual, Online, United States Duration: 13 Jun 2022 → 17 Jun 2022 https://pldi22.sigplan.org/

Conference

Conference	43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022
Country/Territory	United States
Period	13/06/22 → 17/06/22
Internet address	https://pldi22.sigplan.org/

Keywords

Binary Analysis
Disassembly
Formal Verification

Access to Document

10.1145/3519939.3523702Licence: CC BY

Cite this

@inproceedings{263cc83f24914c00a7a831473bd36300,

title = "Formally verified lifting of C-compiled x86-64 binaries",

abstract = "Lifting binaries to a higher-level representation is an essential step for decompilation, binary verification, patching and security analysis. In this paper, we present the first approach to provably overapproximative x86-64 binary lifting. A stripped binary is verified for certain sanity properties such as return address integrity and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an overapproximation of all possible execution paths of the binary. The lifted representation contains disassembled instructions, reconstructed control flow, invariants and proof obligations that are sufficient to prove the sanity properties as well as correctness of the lifted representation. We apply this approach to Linux Foundation and Intel's Xen Hypervisor covering about 400K instructions. This demonstrates our approach is the first approach to provably overapproximative binary lifting scalable to commercial off-the-shelf systems. The lifted representation is exportable to the Isabelle/HOL theorem prover, allowing formal verification of its correctness. If our technique succeeds and the proofs obligations are proven true, then - under the generated assumptions - the lifted representation is correct.",

keywords = "Binary Analysis, Disassembly, Formal Verification",

author = "Freek Verbeek and Joshua Bockenek and Zhoulai Fu and Binoy Ravindran",

note = "Funding Information: The following grant information was disclosed by the authors: Shenyang Agricultural University Talent Introduction Scientific Research: Funding Information: Shenyang Agricultural University Talent Introduction Scientific Research Project (Grant No. 2016026) The funders had no role in study design, data collection and analysis, decision to publish, or preparation of the manuscript. Publisher Copyright: {\textcopyright} 2022 Owner/Author.; 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022 ; Conference date: 13-06-2022 Through 17-06-2022",

year = "2022",

month = jun,

day = "9",

doi = "10.1145/3519939.3523702",

language = "English",

isbn = "978-1-4503-9265-5",

pages = "934--949",

editor = "Ranjit Jhala and Isil Dillig",

booktitle = "PLDI 2022",

publisher = "Association for Computing Machinery",

address = "United States",

url = "https://pldi22.sigplan.org/",

}

Verbeek, F, Bockenek, J, Fu, Z & Ravindran, B 2022, Formally verified lifting of C-compiled x86-64 binaries. in R Jhala & I Dillig (eds), PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery, pp. 934-949, 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022, United States, 13/06/22. https://doi.org/10.1145/3519939.3523702

Formally verified lifting of C-compiled x86-64 binaries. / Verbeek, Freek; Bockenek, Joshua; Fu, Zhoulai et al.
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation. ed. / Ranjit Jhala; Isil Dillig. Association for Computing Machinery, 2022. p. 934-949.

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

TY - GEN

T1 - Formally verified lifting of C-compiled x86-64 binaries

AU - Verbeek, Freek

AU - Bockenek, Joshua

AU - Fu, Zhoulai

AU - Ravindran, Binoy

N1 - Funding Information: The following grant information was disclosed by the authors: Shenyang Agricultural University Talent Introduction Scientific Research: Funding Information: Shenyang Agricultural University Talent Introduction Scientific Research Project (Grant No. 2016026) The funders had no role in study design, data collection and analysis, decision to publish, or preparation of the manuscript. Publisher Copyright: © 2022 Owner/Author.

PY - 2022/6/9

Y1 - 2022/6/9

N2 - Lifting binaries to a higher-level representation is an essential step for decompilation, binary verification, patching and security analysis. In this paper, we present the first approach to provably overapproximative x86-64 binary lifting. A stripped binary is verified for certain sanity properties such as return address integrity and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an overapproximation of all possible execution paths of the binary. The lifted representation contains disassembled instructions, reconstructed control flow, invariants and proof obligations that are sufficient to prove the sanity properties as well as correctness of the lifted representation. We apply this approach to Linux Foundation and Intel's Xen Hypervisor covering about 400K instructions. This demonstrates our approach is the first approach to provably overapproximative binary lifting scalable to commercial off-the-shelf systems. The lifted representation is exportable to the Isabelle/HOL theorem prover, allowing formal verification of its correctness. If our technique succeeds and the proofs obligations are proven true, then - under the generated assumptions - the lifted representation is correct.

AB - Lifting binaries to a higher-level representation is an essential step for decompilation, binary verification, patching and security analysis. In this paper, we present the first approach to provably overapproximative x86-64 binary lifting. A stripped binary is verified for certain sanity properties such as return address integrity and calling convention adherence. Establishing these properties allows the binary to be lifted to a representation that contains an overapproximation of all possible execution paths of the binary. The lifted representation contains disassembled instructions, reconstructed control flow, invariants and proof obligations that are sufficient to prove the sanity properties as well as correctness of the lifted representation. We apply this approach to Linux Foundation and Intel's Xen Hypervisor covering about 400K instructions. This demonstrates our approach is the first approach to provably overapproximative binary lifting scalable to commercial off-the-shelf systems. The lifted representation is exportable to the Isabelle/HOL theorem prover, allowing formal verification of its correctness. If our technique succeeds and the proofs obligations are proven true, then - under the generated assumptions - the lifted representation is correct.

KW - Binary Analysis

KW - Disassembly

KW - Formal Verification

U2 - 10.1145/3519939.3523702

DO - 10.1145/3519939.3523702

M3 - Conference Article in proceeding

AN - SCOPUS:85132251848

SN - 978-1-4503-9265-5

SP - 934

EP - 949

BT - PLDI 2022

A2 - Jhala, Ranjit

A2 - Dillig, Isil

PB - Association for Computing Machinery

T2 - 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2022

Y2 - 13 June 2022 through 17 June 2022

ER -

Formally verified lifting of C-compiled x86-64 binaries

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this