Some questions

[Git-JekG]

Great work. The idea of statically devirtualizing Themida through symbolic evaluation and aggressive optimization is fascinating.

After reading the article, I was left with a few technical questions that I hope you might be willing to elaborate on.

The most interesting part of the article, in my opinion, is control-flow recovery. It also seems to be the area where the least implementation detail is provided. Would it be fair to say that recovering virtual control flow is the main remaining challenge, while most VM handler logic naturally collapses through symbolic evaluation, constant propagation, dead-store elimination, and related optimization passes?

Regarding VMEXITs, how are they discovered automatically? Do you rely on Themida-specific signatures or patterns, or is there a more generic mechanism for identifying exits from the virtual machine?

The article mentions that Themida-specific knowledge is mainly required for control-flow recovery. Could you elaborate on how virtual conditional branches are recovered? How do you determine the targets of virtual JCCs during symbolic evaluation, especially when dealing with more complex control-flow structures?

How do you handle path explosion when exploring virtualized control flow? Are there any techniques such as path merging, state pruning, selective exploration, or other heuristics involved?

I am also curious about the practical limits of the approach. How well does it perform on larger real-world protected functions containing loops, indirect branches, virtual switches, and more complex CFGs? Do you have any statistics regarding success rates, coverage, or known limitations?

Was the implementation developed and tested against a specific Themida generation, or does it work across multiple versions of Themida and CodeVirtualizer?

Finally, how much of the process is currently fully automated? Are there still scenarios where manual analyst intervention is required, or can the pipeline run end-to-end without user guidance?

I would also be very interested in any future documentation describing the IR design, symbolic evaluation engine, and CFG recovery algorithms in greater detail.

Thank you for sharing the research and open-sourcing the project.

[CR3Swapper]

Great work. The idea of statically devirtualizing Themida through symbolic evaluation and aggressive optimization is fascinating.

After reading the article, I was left with a few technical questions that I hope you might be willing to elaborate on.

The most interesting part of the article, in my opinion, is control-flow recovery. It also seems to be the area where the least implementation detail is provided. Would it be fair to say that recovering virtual control flow is the main remaining challenge, while most VM handler logic naturally collapses through symbolic evaluation, constant propagation, dead-store elimination, and related optimization passes?

Regarding VMEXITs, how are they discovered automatically? Do you rely on Themida-specific signatures or patterns, or is there a more generic mechanism for identifying exits from the virtual machine?

The article mentions that Themida-specific knowledge is mainly required for control-flow recovery. Could you elaborate on how virtual conditional branches are recovered? How do you determine the targets of virtual JCCs during symbolic evaluation, especially when dealing with more complex control-flow structures?

How do you handle path explosion when exploring virtualized control flow? Are there any techniques such as path merging, state pruning, selective exploration, or other heuristics involved?

I am also curious about the practical limits of the approach. How well does it perform on larger real-world protected functions containing loops, indirect branches, virtual switches, and more complex CFGs? Do you have any statistics regarding success rates, coverage, or known limitations?

Was the implementation developed and tested against a specific Themida generation, or does it work across multiple versions of Themida and CodeVirtualizer?

Finally, how much of the process is currently fully automated? Are there still scenarios where manual analyst intervention is required, or can the pipeline run end-to-end without user guidance?

I would also be very interested in any future documentation describing the IR design, symbolic evaluation engine, and CFG recovery algorithms in greater detail.

Thank you for sharing the research and open-sourcing the project.

Hello, I am currently under a car wrenching so bear with me.

Regarding VMEXITs, how are they discovered automatically? Do you rely on Themida-specific signatures or patterns, or is there a more generic mechanism for identifying exits from the virtual machine?

Since we concretize the stack pointer when lifting we can essentially refer to the concrete stack pointer value through various points of lifting. RSP should never be symbolic really because all stack changes are known on 99% of code (done in the prolog). We can just check to see what the RSP concrete value is at every RET instruction. Is it 0x10 above what it was when we started lifting? If it is then we know it is some sort of VMEXIT-CALL. It can get complicated with tail calls however.

The article mentions that Themida-specific knowledge is mainly required for control-flow recovery. Could you elaborate on how virtual conditional branches are recovered? How do you determine the targets of virtual JCCs during symbolic evaluation, especially when dealing with more complex control-flow structures?

Control flow inside of virtual machine is indeed the only adhoc/vm specific thing we must understand and handle.

1.) When we symbolically evaluate the virtual machine and we come to a VJCC handler we will come to a stop at a native JCC inside of the VJCC handler. I posted a fully documented VJCC handler in the article showing how themida/cv VJCC works. You can see that they reimpliment the flag checks using native control flow if (eflags.zf) -> vmcontext->branch_taken = true;. This "branch_taken" value is then used later in the VM handler to determine which branch to take. So our symbolic evaluation halts on the if (eflags.zf). We must evaluate (emulate the IR) both sides of this if statement until the next indirect jmp (end of the VJCC handler). Keep in mind that if the original JCC was more complex than a single flag dependant JCC we will hit another JCC inside of the VJCC handler (like if eflag.sf). I will talk about tracking VIP in a follow up question

2.) "dealing with more complex control-flow structures" (I.E jump tables?) I currently have no solution for and have yet to come across them in virtualized samples. IIRC CodeVirtualizer/Themida struggled for many years with jump tables and only recently supported them?

How do you handle path explosion when exploring virtualized control flow? Are there any techniques such as path merging, state pruning, selective exploration, or other heuristics involved?

To prevent path explosion we must track VIP. This is so we do not re-lift virtualized control flow that we have already lifted before. I talk about it in the article and there is even a graphic showing why. When two paths merge together we must create phi's. Tracking VIP is another adhoc/vmspecific component to this approach of devirtualization.

I am also curious about the practical limits of the approach. How well does it perform on larger real-world protected functions containing loops, indirect branches, virtual switches, and more complex CFGs? Do you have any statistics regarding success rates, coverage, or known limitations?

The binaries we have had to devirtualize were using the macros to mark start/end of the virtualization. The control flow as limited to JCC logic at most and sometimes loops. Again I have not had to deal with virtualized jump tables etc.. most of the time compilers will turn a switch case into a series of JCC operations. If we need to deal with virtualized jump tables ill find an adhoc solution that works. I dont have any stats for coverage or success rates.

Was the implementation developed and tested against a specific Themida generation, or does it work across multiple versions of Themida and CodeVirtualizer?

The techniques described in the article should work on any combination of virtual machines. I dont know if it works on specific version of CodeVirtualizer/Themida. When we take a contract we just focus on the binary given to us, however our tools are becoming more and more automated as we go.

Finally, how much of the process is currently fully automated? Are there still scenarios where manual analyst intervention is required, or can the pipeline run end-to-end without user guidance?

It requires baby sitting, it is not a drag-and-drop situation. Things happen, edge cases come up. However it works for us as our contracts usually specify a specific target. Maybe if someone is interested in paying us a huge amount of money (and a mean a lot) for a drag-and-drop solution for specific protectors we will consider it, however we have yet to been approach with an offer like that.

I would also be very interested in any future documentation describing the IR design, symbolic evaluation engine, and CFG recovery algorithms in greater detail.

All of this is private/closed source. It is our companies core IP. If a company/person wishes to have such information it can be done via acquisition. Its taken a long time to build our framework and we are improving it every day. We are mostly focused on obfuscation though, this deobfuscation stuff is more side biz for us.

https://discord.gg/sgedeapTMm

[Git-JekG]

Thank you for the explanation, it's incredibly helpful.

Just out of curiosity: do you find that CodeVirtualizer targets usually exhibit the same handler complexity as full Themida builds, or are they generally tamer? Also, during initial triage, do you have a methodology for identifying the VM generation or protector version, or do you focus primarily on the VM's actual implementation rather than its version number?

I'm currently looking at a CV sample myself, which is why I'm asking. If you're ever interested in discussing additional real-world samples, I'd be happy to share some observations from it.

Really appreciate you taking the time to explain your workflow.

[CR3Swapper]

Thank you for the explanation, it's incredibly helpful.

Just out of curiosity: do you find that CodeVirtualizer targets usually exhibit the same handler complexity as full Themida builds, or are they generally tamer? Also, during initial triage, do you have a methodology for identifying the VM generation or protector version, or do you focus primarily on the VM's actual implementation rather than its version number?

I'm currently looking at a CV sample myself, which is why I'm asking. If you're ever interested in discussing additional real-world samples, I'd be happy to share some observations from it.

Really appreciate you taking the time to explain your workflow.

I would be interested in continuing this conversation elsewhere. Do you want to join the Discord or shoot me an email at contact@back.engineering. Would be nice to exchange signal/telegram/matrix.