A formal semantics for high P-Code

[niconaus]

Recent efforts by Virginia Tech and Open University of The Netherlands on a DAPRA funded project have resulted in the formalization of Ghidra's high P-Code. The work was presented at VSTTE 2022, and springer has just now published the open-access paper associated with this work.

A Formal Semantics for High P-Code by Nico Naus, Freek Verbeek, Dale Walker & Binoy Ravindran

This work might be interesting for anyone doing analysis on or processing of Ghidra's High P-Code output. The paper gives a formal description of its semantics. These semantics have also been implemented as an interpreter in Haskell, which can be found here.

During the development of the formal semantics, several issues have been uncovered in Ghidra, P-Code and Ghidra's documentation. These are described in Section 6 of the paper, but where appropriate, I will open/have opened separate issues on Ghidra's GitHub page: #4947 #4946 #4945

The formal semantics and issues uncovered have been disclosed to the Ghidra team at NSA, several months ago. I'm really interested in discussing the results we found with the community here on GitHub too.

[KevOrr]

Thank you for your work in this area. Currently the P-Code docs could use a bit of love, and the situation isn't helped when the implementation's behavior diverges from the spec laid out in the docs.

I haven't read the paper in its entirety yet but I have some questions after skimming through some sections:

• In section 6.1, you say that MULTIEQUAL (P-Code's phi function) doesn't contain information about each argument's address of origin. However, varnodes already include the address at which they are defined, which can be accessed with their .getPCAddress() method. This should be sufficient for SSA right?
• In section 5, you say "We assume that direct calls and direct branches are encoded by having a constant varnode as an argument. In all other cases, the call and branch will be interpreted as indirect". Is this about the CALL operation only? If so, I'm not sure if a constant varnode makes any sense there. As I understand it, for CALL/BRANCH, the input varnode itself is the target of the call, not the value, interpreted as a pointer, located at the varnode. This latter behavior is how CALLIND/BRANCHIND works.
• Similarly in figure 8, in T-Branch, the input varnode in is "evaluated" to a constant. Looking at the rule V-Mem of figure 5, if the input varnode is in memory, then this amounts to looking up the value contained at that address. Is goto then supposed to have the same semantics as BRANCHIND instead of BRANCH?
• "Looking at P-Code programs, it is immediately clear that this cannot be true. A function can have arguments and return a value, and this behavior is certainly not captured by a basic BRANCH instruction". Wow, I'm glad you pointed this out. I had been trusting the docs blindly on this one, but on at least x86 linux, the CALL instruction does seem to fully capture the argument passing and the control-flow operation, with no instructions preceding it explicitly indicating how arguments are copied to the stack and registers before the call

Again, thank you for this work and your time.

[niconaus]

@KevOrr Great questions! Let me try to answer them the best I can:

• In section 6.1, you say that MULTIEQUAL (P-Code's phi function) doesn't contain information about each argument's address of origin. However, varnodes already include the address at which they are defined, which can be accessed with their .getPCAddress() method. This should be sufficient for SSA right?

Thank you so much for this suggestion! I was not aware of this. Indeed calling getPCAddress() on the alternative values for the phi-node returns the address it should be guarded by. I had found another method, by looking at the in-branches for the block, but this is a much better solution. The problem that remains is that the information has to be accessed trough the API, rather than it be included in the P-Code instruction itself.
I've developed a script to dump high P-Code that solves some of the issues described in the paper, which is available here. I'll update the code to include your suggestion, which I think is a much neater solution!

• In section 5, you say "We assume that direct calls and direct branches are encoded by having a constant varnode as an argument. In all other cases, the call and branch will be interpreted as indirect". Is this about the CALL operation only? If so, I'm not sure if a constant varnode makes any sense there. As I understand it, for CALL/BRANCH, the input varnode itself is the target of the call, not the value, interpreted as a pointer, located at the varnode. This latter behavior is how CALLIND/BRANCHIND works.

Yes, you are correct. There is some discrepancy here about how Ghidra produces high P-Code, and the way in which we've defined the formal semantics. Our idea was to reduce the number of instructions even further by evaluating the varnode argument to both call and branch. In our experiments we have only seen BRANCH and CALL being used with a memory varnode, and never a constant. We therefore thought it would be a good idea to join the BRANCH and BRANCHIND instructions, exactly as you described. However, when discussing the results with the Ghidra team, they pointed out that BRANCH is actually sometimes used with a constant varnode, specifically in a Harvard architecture binary. We've ran some experiments and could not replicate it. Therefore we chose not to include it in the recommendations, but still keep it in the formalized semantics. I'm really curious to hear if anyone else has some additional thoughts on this. I still think it is a good idea to merge the indirect variants with the direct variants of these instructions.

• Similarly in figure 8, in T-Branch, the input varnode in is "evaluated" to a constant. Looking at the rule V-Mem of figure 5, if the input varnode is in memory, then this amounts to looking up the value contained at that address. Is goto then supposed to have the same semantics as BRANCHIND instead of BRANCH?

Yes, if BRANCH is supplied with a memory varnode, it behaves as BRANCHIND. When a regular BRANCH is intended, we expect a constant. Again, this is just a suggestion by our team, not how high P-Code works at the moment.

• "Looking at P-Code programs, it is immediately clear that this cannot be true. A function can have arguments and return a value, and this behavior is certainly not captured by a basic BRANCH instruction". Wow, I'm glad you pointed this out. I had been trusting the docs blindly on this one, but on at least x86 linux, the CALL instruction does seem to fully capture the argument passing and the control-flow operation, with no instructions preceding it explicitly indicating how arguments are copied to the stack and registers before the call

I think this is one of the biggest omissions in the documentation. I've opened an issue regarding high/low P-Code doc, so hopefully this gets resolved soon.

Let me know if you have any further thoughts!

[KevOrr]

Thank you very much for the in-depth response. That clears up my confusion about BRANCH and company: I was misinterpreting your suggestions as observations. Like mentioned in the paper, it has been my assumption that a driving motivation for ghidra's model of memory---where every address is not just an offset, but an offset within some abstract chunk of memory---is to support non-von Neumann architectures. Certainly Harvard architectures, but I also assumed that it's built the way it is to support architectures that have multiple ISAs that can be switched out at runtime, such as ARM and THUMB (or on chips that support it, Jazelle). I've never tested this assumption though, and I could easily see it implemented as a callother instead, but I would be curious to see if any of these multiple ISA architectures make use of multiple address spaces for memory.

[sad-dev]

6.4 Response from Ghidra Developers

We have reached out to the Ghidra development team at NSA with our findings and the above recommendations. They have confirmed our findings and acknowledged all issues we found. As for the conditional branch, they refer to a GitHub issue where this problem is also identified link. Their stance is that although it is semantically incorrect, they do not consider this to be a bug. The destination of the conditional jump is preserved from low to high P-Code, which they deem more important than the correctness of the instruction itself.

Could you show where this discussion with the Ghidra team is? I would love to understand P-Code better, but am having trouble finding this in the github issues.

[niconaus]

The discussion took place though our NSA liaison at Virginia Tech. I will have to check if the correspondence with them is in any way classified, or if it can be shared freely here.

[ghidracadabra]

@niconaus Thank you for initiating this discussion! There are a number of issues to consider, both those mentioned above and those in the issues you've submitted.

I think the first one to discuss involves the BRANCH op. A constant varnode (i.e., a varnode in the const space) appears as an input to a BRANCH op in the case of a "pcode relative branch". This is used when the pcode for a single machine instruction is not just a straight-line program but instead contains jumps or loops. In the simple case, all of the pcode ops for a single machine instruction are associated with the same address in the binary (things like delay slots can complicate matters). If you want to branch within the ops for one instruction, you need something other than a machine address as a jump target. Constant inputs to the BRANCH op are used in this case; the constant represents the number of pcode ops to jump from BRANCH op (can be positive or negative).

As an example, consider the 64-bit variant of the BSF instruction

ghidra/Ghidra/Processors/x86/data/languages/ia.sinc

Line 1840 in 601ab94

:BSF Reg64,rm64 is $(LONGMODE_ON) & vexMode=0 & opsize=2 & byte=0xf; byte=0xbc; rm64 & Reg64 ...

You can make a simple function (with the default x64 linux calling convention) using this instruction with the bytes 48 0f bc c7 c3 (BSF RAX, RDI; RET)

In the high pcode for this function you should see a BRANCH op with a constant input.

Hopefully that's at least somewhat helpful; please let me know if I've misunderstood the issue you raised.

[niconaus]

Thank you for your reply, this is very insightful! In our communication with the NSA team, it was indicated that this occurs when using for example a Harvard architecture, but we were unable to reproduce this.
We'll try your suggestion to see what results we get, and update our High P-Code interpreter accordingly!

Again, thanks for the extensive reply!