4

I'm interested in formal verification of software at binary code level. Obviously, the first step would be to recover the actual assembly instructions from binaries.

IDAPro can do a pretty good job at disassembly of x86, however, it is still possible that some data can be interpreted as code. Therefore an analysis based on in it is still unsound.

Given that:

  • Software in my application domain is not obfuscated and not self-modifying,
  • and ARM instructions are less variable than x86 (2 or 4 bytes length).

Can the disassembly of ARM binaries be sound? In other words, can disassemblers recover the actual code precisely?

Improve this question

3 Answers 3

Reset to default
5

After some research I think that I can add some explanations from a theoretical perspective. Note that my discussion is restricted to stripped (no debug information) executables. We know that several kinds of data can be mixed with code in executables including padding bytes and switch jump address calculations.

In order to separate date from code we need to precisely extract the bytes that belong to the code and by that we can assume that the rest of the bytes belong to data. The main challenge in precisely extracting code starting from a well-known entry point is indirect jumps i.e. control flow redirection to memory addresses that are computed at run-time. DarthZirka mentioned a few examples including switch tables, function pointers, and vtables in C++.

An analysis that can precisely solve indirect jumps statically (without running the program) can also solve the halting problem which is known to be undecidable. This result has been established since late 70's when work on disassembly started to gain ground in Academia, I can refer to the following early paper for further details.

R.N. Horspool and N. Marovac. An approach to the problem of detranslation of computer programs. The Computer Journal, 23(3):223-229, 1979.

Based on that, the problem of precisely determining addresses of indirect jumps is also undecidable in general. Therefore, any approach to disassembly shall be based on heuristics like recognizing common compiler idioms and/or over(under) approximating the set of addresses reachable from an indirect jump. The later is usually done by static analysis based on the framework of abstract interpretation. Variable size instructions in X86 can make things harder (a more loose overapproximation) compared to ARM but the essential problem still exists.

Improve this answer
4

The coverage/completeness problem has little to do with the 'accuracy' of a disassembly engine or variance in instruction length. The problem arises if and when code is not referenced statically from the call tree rooted at the entry point of the target binary.

Among other things this comprises:

  • other external entry points (DLL exports, TLS callbacks etc.)
  • switch tables
  • vtables
  • non-static function pointers/tables (e.g. C-style objects)
  • funclets/thunks related to exception handling etc.
  • CRT init/exit tables

Accuracy comes into play with regard to switch tables, which in IDA are the responsibility of the individual processor modules. The other things are the responsibility of the loader, the kernel, compiler-specific plugins (RTTI, exception funclets), and ultimately the human operator.

The SEH info in x64 COFF covers all non-leaf functions, and this improves coverage a lot compared to 32-bit COFF. If you have control over the build process then you can achieve almost perfect coverage via debug info (PDB, TDS etc.). Having the linker produce detailed MAP files can also be helpful.

An additional complication arises if a binary has its relocation info stripped; in this case the disassembler may have problems deciding whether a given immediate value is an offset or just a number. The same problem occurs with based pointers, including RVAs outside of places where IDA expects RVAs to occur.

Improve this answer
2

You'll face the same problem that any disassembler has: you don't know the meaning of things.

Real life example i had last week: when i saw the value 0x00408800 passed to a function, i was certain this had to be a bit mask. After a lot of tracing, and seeing the value was stored somewhere, copied somewhere else, used in a class constructor, and accessed in a method of a subclass, i figured out that this was actually a memory location, which happened to be part of a larger array, so it didn't even have a symbol on its own.

And, if it had been an indirect call instead of a memory access, this would have turned the meaning of the bytes at that address from data to code.

Unless your code verifier / disassembler generates a list of every possible state of the program and RAM, and as a results, knows where every literal value might be used, and knows where every used value might be calculated from, you won't be able to find such ambiguities automatically. But, this is only one example for an ambiguity, and i suppose being able to differentiate between a memory location and a bitmap would be quite important for any kind of code verification.

So, unless you make a lot more assumptions (code is generated by a specific compiler that emits a finite number of basic blocks that are combined only in specific ways), no, i don't think it's possible.

Improve this answer
3
  • 1
    As another example: sometimes programs push an argument like 0x40001000, and it could either be the e.g. image base, or a bit mask. IDA often considers it's a function pointer instead a bit mask, and even creates a xref and a function at that address for it. So ultimately, unless you emulate every possible situation (impossible), it's impossible to programmatically know what's the meaning of that number.
    – rev
    Feb 24, 2015 at 15:15
  • That's a problem only in those cases where (1) the signature of the recipient is not known (neither part of the current binary nor in a TIL/PDB), and (2) the recipient executes that pointer. I.e. comparatively rare. IOW, the problem is unsolvable in general but perfectly solvable for big classes of real binaries.
    – DarthGizka
    Feb 24, 2015 at 16:28
  • 1
    If you have access to all that information, i doubt that the OPs statement "Obviously, the first step would be to recover the actual assembly instructions from binaries" holds.
    – Guntram Blohm
    Feb 24, 2015 at 16:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.