search

moralismercatus / crete

Open source concolic testing tool for binaries
1 stars 1 forks source link

Target binary dump is (seemingly) far too large #11

Closed moralismercatus closed 10 years ago

moralismercatus commented 10 years ago

Dumping the LLVM Bitcode for a single line binary produces nearly 100,000 lines of LLVM Bitcode.

I understand system calls, startup and cleanup, but that seems absolutely absurd.

moralismercatus commented 10 years ago

I tried multiple calls to injecting the custom opcode into the binary. No noticeable change. I suspect that this is due to caching. The call is cached and therefore is not translated again. When I changed the opcode to BE from AE, the custom instruction was hit, fortifying the suspicion.

moralismercatus commented 10 years ago

Example case: 1 line program Dumping the static binary with ndisasm -b 32 > yields ~4000 lines. How does 1 line of C translate to 4,000 lines of assembly? I assume it's startup (main) and termination.

Dumping the trace on that same binary yields ~80,000 lines or more.

The one time the instructions were identical (I haven't been able to reproduce it, I'm not sure how I did it), the contiguous static block in the trace dump was located at about lines 61,000-65,000. This means that there is "something" happening for 61,000 lines before the program is executed, and "something" is happening for another ~20,000 lines after the program returns. I suspect that this is OS loading and unloading, but it's only speculation. The only thing I am relatively certain of is that the static binary dump should be roughly equivalent the trace for a one line program that has only one path.

In addition, this extra information, I'm fairly certain, is not necessary or beneficial to the path trace, so it needs to be removed. Kai and Bo concur.

moralismercatus commented 10 years ago

I am attempting to use custom instruction injection to delimit the start and ending translation blocks.

Using the preloaded library, the start custom instruction is injected as normal. For the end, I have set atexit() to call a function that injects an end custom instruction.

This has reduced the number of assembly lines, of the trace dump, to 15,000, which is better, but still needs improvement.

moralismercatus commented 10 years ago

I am unable to determine the correctness of isolating only the instructions that we need. I think part is caused by the translation process. My guest OS is x86 and my host is x64. Even dumping what I believe to be the x86 instructions, they are not identical to the static binary dump. It appears QEMU is modifying the instructions, or my understanding of binary execution is off.

If I can get an identical set of instructions somewhere in the trace dump to the static dump, then I will know where the program begins and ends.

I will try with a guest x64 and see what that trace dump looks like.

moralismercatus commented 10 years ago

In summary, it appears that the OS is doing load/unload preparation/cleanup before and after the execution trace is loaded. Part of this is the C runtime environment, part the VM table, etc.

This information, as far as my current understanding allows, is not only irrelevant, but detrimental to the replay on Klee, so it must be filtered out. Other tickets will describe the approaches.

S2E likely didn't have this issue because the symbolic execution was online.

Part of the reason for the inconsistency may have been the way PIDs were being acquired. The PID is now acquired using QEMU's callback mechanism that executes when the instruction is encountered.

I did get more consistent results with an x64 guest OS, but whether that was the PID issue or something else, I'm unsure.