A Formal Semantics for P-Code

Nico Naus; Freek Verbeek; Dale Walker; Binoy Ravindran

doi:10.1007/978-3-031-25803-9_7

A Formal Semantics for P-Code

Nico Naus^*, Freek Verbeek, Dale Walker, Binoy Ravindran

^*Corresponding author for this work

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

Abstract

Decompilation is currently a widely used tool in reverse engineering and exploit detection in binaries. Ghidra, developed by the National Security Agency, is one of the most popular decompilers. It decompiles binaries to high P-Code, from which the final decompilation output in C code is generated. Ghidra allows users to work with P-Code, so users can analyze the intermediate representation directly. Several projects make use of this to build tools that perform verification, decompilation, taint analysis and emulation, to name a few. P-Code lacks a formal semantics, and its documentation is limited. It has a notoriously subtle semantics, which makes it hard to do any sort of analysis on P-Code. We show that P-Code, as-is, cannot be given an executable semantics. In this paper, we augment P-Code and define a complete, executable, formal semantics for it. This is done by looking at the documentation and the decompilation results of binaries with known source code. The development of a formal P-Code semantics uncovered several issues in Ghidra, P-Code, and the documentation. We show that these issues affect projects that rely on Ghidra and P-Code. We evaluate the executability of our semantics by building a P-Code interpreter that directly uses our semantics. Our work uncovered several issues in Ghidra and allows Ghidra users to better leverage P-Code.

Original language	English
Title of host publication	Verified Software. Theories, Tools and Experiments
Subtitle of host publication	14th International Conference, VSTTE 2022
Editors	Akash Lal, Stefano Tonetta
Publisher	Springer, Cham
Pages	111-128
Number of pages	18
Edition	1
ISBN (Electronic)	9783031258039
ISBN (Print)	9783031258022
DOIs	https://doi.org/10.1007/978-3-031-25803-9_7
Publication status	Published - 2023
Event	14th International Conference on Verified Software. Theories, Tools and Experiments, VSTTE 2022 - Trento, Italy Duration: 17 Oct 2022 → 18 Oct 2022 https://vstte22.fbk.eu/

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13800 LNCS
ISSN	0302-9743

Conference

Conference	14th International Conference on Verified Software. Theories, Tools and Experiments, VSTTE 2022
Country/Territory	Italy
City	Trento
Period	17/10/22 → 18/10/22
Internet address	https://vstte22.fbk.eu/

Keywords

Decompilation
Formal semantics
P-Code

Access to Document

10.1007/978-3-031-25803-9_7Licence: CC BY

Cite this

Naus, Nico ; Verbeek, Freek ; Walker, Dale et al. / A Formal Semantics for P-Code. Verified Software. Theories, Tools and Experiments: 14th International Conference, VSTTE 2022. editor / Akash Lal ; Stefano Tonetta. 1. ed. Springer, Cham, 2023. pp. 111-128 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13800 LNCS).

@inproceedings{7052956080f84387ba1961c14d36c7ad,

title = "A Formal Semantics for P-Code",

abstract = "Decompilation is currently a widely used tool in reverse engineering and exploit detection in binaries. Ghidra, developed by the National Security Agency, is one of the most popular decompilers. It decompiles binaries to high P-Code, from which the final decompilation output in C code is generated. Ghidra allows users to work with P-Code, so users can analyze the intermediate representation directly. Several projects make use of this to build tools that perform verification, decompilation, taint analysis and emulation, to name a few. P-Code lacks a formal semantics, and its documentation is limited. It has a notoriously subtle semantics, which makes it hard to do any sort of analysis on P-Code. We show that P-Code, as-is, cannot be given an executable semantics. In this paper, we augment P-Code and define a complete, executable, formal semantics for it. This is done by looking at the documentation and the decompilation results of binaries with known source code. The development of a formal P-Code semantics uncovered several issues in Ghidra, P-Code, and the documentation. We show that these issues affect projects that rely on Ghidra and P-Code. We evaluate the executability of our semantics by building a P-Code interpreter that directly uses our semantics. Our work uncovered several issues in Ghidra and allows Ghidra users to better leverage P-Code.",

keywords = "Decompilation, Formal semantics, P-Code",

author = "Nico Naus and Freek Verbeek and Dale Walker and Binoy Ravindran",

note = "Funding Information: This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under contract N6600121C4028 and Agreement No. HR.00112090028, and the US Office of Naval Research (ONR) under grant N00014-17-1-2297. Publisher Copyright: {\textcopyright} 2023, The Author(s).; 14th International Conference on Verified Software. Theories, Tools and Experiments, VSTTE 2022 ; Conference date: 17-10-2022 Through 18-10-2022",

year = "2023",

doi = "10.1007/978-3-031-25803-9\_7",

language = "English",

isbn = "9783031258022",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer, Cham",

pages = "111--128",

editor = "Akash Lal and Stefano Tonetta",

booktitle = "Verified Software. Theories, Tools and Experiments",

edition = "1",

url = "https://vstte22.fbk.eu/",

}

Naus, N , Verbeek, F, Walker, D & Ravindran, B 2023, A Formal Semantics for P-Code. in A Lal & S Tonetta (eds), Verified Software. Theories, Tools and Experiments: 14th International Conference, VSTTE 2022. 1 edn, Springer, Cham, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13800 LNCS, pp. 111-128, 14th International Conference on Verified Software. Theories, Tools and Experiments, VSTTE 2022, Trento, Italy, 17/10/22. https://doi.org/10.1007/978-3-031-25803-9_7

A Formal Semantics for P-Code. / Naus, Nico ; Verbeek, Freek; Walker, Dale et al.
Verified Software. Theories, Tools and Experiments: 14th International Conference, VSTTE 2022. ed. / Akash Lal; Stefano Tonetta. 1. ed. Springer, Cham, 2023. p. 111-128 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13800 LNCS).

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

TY - GEN

T1 - A Formal Semantics for P-Code

AU - Naus, Nico

AU - Verbeek, Freek

AU - Walker, Dale

AU - Ravindran, Binoy

N1 - Funding Information: This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) and Naval Information Warfare Center Pacific (NIWC Pacific) under contract N6600121C4028 and Agreement No. HR.00112090028, and the US Office of Naval Research (ONR) under grant N00014-17-1-2297. Publisher Copyright: © 2023, The Author(s).

PY - 2023

Y1 - 2023

N2 - Decompilation is currently a widely used tool in reverse engineering and exploit detection in binaries. Ghidra, developed by the National Security Agency, is one of the most popular decompilers. It decompiles binaries to high P-Code, from which the final decompilation output in C code is generated. Ghidra allows users to work with P-Code, so users can analyze the intermediate representation directly. Several projects make use of this to build tools that perform verification, decompilation, taint analysis and emulation, to name a few. P-Code lacks a formal semantics, and its documentation is limited. It has a notoriously subtle semantics, which makes it hard to do any sort of analysis on P-Code. We show that P-Code, as-is, cannot be given an executable semantics. In this paper, we augment P-Code and define a complete, executable, formal semantics for it. This is done by looking at the documentation and the decompilation results of binaries with known source code. The development of a formal P-Code semantics uncovered several issues in Ghidra, P-Code, and the documentation. We show that these issues affect projects that rely on Ghidra and P-Code. We evaluate the executability of our semantics by building a P-Code interpreter that directly uses our semantics. Our work uncovered several issues in Ghidra and allows Ghidra users to better leverage P-Code.

AB - Decompilation is currently a widely used tool in reverse engineering and exploit detection in binaries. Ghidra, developed by the National Security Agency, is one of the most popular decompilers. It decompiles binaries to high P-Code, from which the final decompilation output in C code is generated. Ghidra allows users to work with P-Code, so users can analyze the intermediate representation directly. Several projects make use of this to build tools that perform verification, decompilation, taint analysis and emulation, to name a few. P-Code lacks a formal semantics, and its documentation is limited. It has a notoriously subtle semantics, which makes it hard to do any sort of analysis on P-Code. We show that P-Code, as-is, cannot be given an executable semantics. In this paper, we augment P-Code and define a complete, executable, formal semantics for it. This is done by looking at the documentation and the decompilation results of binaries with known source code. The development of a formal P-Code semantics uncovered several issues in Ghidra, P-Code, and the documentation. We show that these issues affect projects that rely on Ghidra and P-Code. We evaluate the executability of our semantics by building a P-Code interpreter that directly uses our semantics. Our work uncovered several issues in Ghidra and allows Ghidra users to better leverage P-Code.

KW - Decompilation

KW - Formal semantics

KW - P-Code

U2 - 10.1007/978-3-031-25803-9_7

DO - 10.1007/978-3-031-25803-9_7

M3 - Conference Article in proceeding

AN - SCOPUS:85151045477

SN - 9783031258022

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 111

EP - 128

BT - Verified Software. Theories, Tools and Experiments

A2 - Lal, Akash

A2 - Tonetta, Stefano

PB - Springer, Cham

T2 - 14th International Conference on Verified Software. Theories, Tools and Experiments, VSTTE 2022

Y2 - 17 October 2022 through 18 October 2022

ER -

Naus N , Verbeek F, Walker D, Ravindran B. A Formal Semantics for P-Code. In Lal A, Tonetta S, editors, Verified Software. Theories, Tools and Experiments: 14th International Conference, VSTTE 2022. 1 ed. Springer, Cham. 2023. p. 111-128. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13800 LNCS). doi: 10.1007/978-3-031-25803-9_7