3 ms·

Binary Symbolic Execution with KLEE-Native

50 points by matt_d 7y ago

carapace 7y ago
Some discussion of KLEE from last year: https://news.ycombinator.com/item?id=16851893 https://news.ycombinator.com/item?id=16851893
- symbex 7y ago
  An alternative is S2E (https://s2e.systems https://s2e.systems), it combines KLEE and QEMU to enable whole-system symbolic execution. It is most suitable when you have a program binary that heavily interacts with the system (system code, device drivers, etc.). S2E does not require writing any syscall models to run programs. This is important from a practical point of view: first, if your program can run in QEMU, it will run on S2E, and second, you will not run into issues of clobbering execution states that you have in KLEE when calling external functions that don't have a model. Of course, S2E is not magic and is still facing path explosion challenges, but you have flexible ways of managing it via a powerful plugin architecture. E.g., you can instrument the guest to use function models, control when to concretize data or prevent execution from forking, writing searcher heuristics, etc.
  - carapace 7y ago
    Oh, that is cool! Thank you.
saagarjha 7y ago
Unrelated, but maybe someone might know the answer to this: > To do this, we use a neat trick of parsing the /proc/[pid]/maps file for the target process to discover the base virtual address of the loaded program. Is there any better way to do this? Everyone I know just parses /proc/pid/maps for detecting the slide but this seems so ugly…
- pag 7y ago
  If you're inside the process, as the LD_PRELOAD interceptor mentioned in the article is, then in theory you could try to get the address of the binary's main function or some other symbol that you expect to be exported, and scan down in until you find the lowest mapped page, and then store that address somewhere that you could know of in advance. You could scan down and detect the first unmapped page by clever use of system calls that return EFAULT as a possible return code.
- pag 7y ago
  If you can modify the kernel, you could modify binfmt_elf.c in the case of the Linux kernel, and log out the load address to dmesg or something like that. Another alternative, which I believe are both options available with PIN and DynamoRIO, is to implement or use an existing ELF loader, forking yourself, and loading in the target binary of interest at a known location.
Grimm1 7y ago
Hey my friend wrote this article woot woot, just messaged him that this made it front page

50 points by matt_d 7y ago

Some discussion of KLEE from last year: https://news.ycombinator.com/item?id=16851893 https://news.ycombinator.com/item?id=16851893

symbex 7y ago
An alternative is S2E (https://s2e.systems https://s2e.systems), it combines KLEE and QEMU to enable whole-system symbolic execution. It is most suitable when you have a program binary that heavily interacts with the system (system code, device drivers, etc.). S2E does not require writing any syscall models to run programs. This is important from a practical point of view: first, if your program can run in QEMU, it will run on S2E, and second, you will not run into issues of clobbering execution states that you have in KLEE when calling external functions that don't have a model. Of course, S2E is not magic and is still facing path explosion challenges, but you have flexible ways of managing it via a powerful plugin architecture. E.g., you can instrument the guest to use function models, control when to concretize data or prevent execution from forking, writing searcher heuristics, etc.
- carapace 7y ago
  Oh, that is cool! Thank you.

saagarjha 7y ago

Unrelated, but maybe someone might know the answer to this: > To do this, we use a neat trick of parsing the /proc/[pid]/maps file for the target process to discover the base virtual address of the loaded program. Is there any better way to do this? Everyone I know just parses /proc/pid/maps for detecting the slide but this seems so ugly…

pag 7y ago
If you're inside the process, as the LD_PRELOAD interceptor mentioned in the article is, then in theory you could try to get the address of the binary's main function or some other symbol that you expect to be exported, and scan down in until you find the lowest mapped page, and then store that address somewhere that you could know of in advance. You could scan down and detect the first unmapped page by clever use of system calls that return EFAULT as a possible return code.
pag 7y ago
If you can modify the kernel, you could modify binfmt_elf.c in the case of the Linux kernel, and log out the load address to dmesg or something like that. Another alternative, which I believe are both options available with PIN and DynamoRIO, is to implement or use an existing ELF loader, forking yourself, and loading in the target binary of interest at a known location.

Grimm1 7y ago

Hey my friend wrote this article woot woot, just messaged him that this made it front page