Repository navigation
Is specifying an input mandatory for SymQEMU to perform symbolic execution and generate test cases? #72
Description
Activity
I don't think command-line options are currently a supported source of symbolic input 🤔
I don't think command-line options are currently a supported source of symbolic input 🤔
Do you mean that currently SymQEMU can only support programs with explicit inputs? Can't do a symbolic execution test on Ardupilot? In that case, most of the programs are unusable? Can you recommend some SymQEMU suitable assemblies for me to test?
Do you mean that currently SymQEMU can only support programs with explicit inputs?
It works with programs that read input from stdin or from a file.
您的意思是目前 SymQEMU 只能支持具有显式输入的程序吗？
它适用于从 stdin 或文件读取输入的程序。
In your example, I see how input is provided from a pipeline, but not all programs just need such simple input. In the binary files compiled for some embedded programs, I tested directly with SymQEMU, similar to this problem, and it didn't work. Do I need to use Symcc to symbolize these programs at compile time before I can do symbolic execution tests?
I think I may not have mastered the correct way to use SymQEMU, can you provide me with more test cases so that I can better grasp the correct use of SymQEMU? Thank you very muchThere's no need to instrument with SymCC when you use SymQEMU; one or the other is enough. They basically do the same thing, SymCC via a compiler pass and SymQEMU by hooking into binary translation.
The core idea is that they both need to know the data that is the input to your program, the data that they can manipulate to make the program take a different path. By default, they assume that your program reads from stdin; anything that comes from there is assumed to be part of the input. Alternatively, you can set the environment variable
SYMCC_INPUT_FILEto a file name, in which case data read from the file is considered to be the input instead.There's a third option for more complex cases in SymCC,
SYMCC_MEMORY_INPUT, which lets your program communicate to the SymCC runtime via an API where to find the input data in memory. But the option is not available SymQEMU; it assumes that you're analyzing a binary because you can't rebuild the source code.There's no need to instrument with SymCC when you use SymQEMU; one or the other is enough. They basically do the same thing, SymCC via a compiler pass and SymQEMU by hooking into binary translation.
The core idea is that they both need to know the data that is the input to your program, the data that they can manipulate to make the program take a different path. By default, they assume that your program reads from stdin; anything that comes from there is assumed to be part of the input. Alternatively, you can set the environment variable
SYMCC_INPUT_FILEto a file name, in which case data read from the file is considered to be the input instead.There's a third option for more complex cases in SymCC,
SYMCC_MEMORY_INPUT, which lets your program communicate to the SymCC runtime via an API where to find the input data in memory. But the option is not available SymQEMU; it assumes that you're analyzing a binary because you can't rebuild the source code.In addition, is SymQEMU suitable for testing some drivers, such as some network card drivers, etc., and generating valid test cases? What should be done?
In principle, it could do that. You'd have to add code to mark your driver's input as symbolic (e.g., data received on a network interface), and you'd have to simulate an entire OS, not just user space. This will likely require handling symbolic data in more places of the emulator.
In principle, it could do that. You'd have to add code to mark your driver's input as symbolic (e.g., data received on a network interface), and you'd have to simulate an entire OS, not just user space. This will likely require handling symbolic data in more places of the emulator.
That is, this requires the driver's input to be marked as a symbol, which requires a modification to the SymQEMU code? And need a full system simulation of QEMU? Can SymQEMU do this?
Correct. Currently SymQEMU only works with QEMU's user space emulation; you'd have to extend it to full system emulation.
We are working on system mode, but it's still WIP, we will make it public at some point. See issue #32
Also, in the case of binary symbol execution, I have generated some test cases for a binary executable via SymQEMU, but how do I test the path coverage? What tools to use? Traditional coverage testing requires source code, which is clearly not feasible
To answer the question about reading input from a file: no compile-time
changes are needed. SymQEMU works on a normally compiled binary (plain
gcc/clang); you do not need to instrument it with SymCC first.The only thing SymQEMU needs to know is which bytes are the input (the
bytes it is allowed to mutate). There are two ways to provide that:- stdin (default): bytes the program reads from standard input are
treated as symbolic. - A file: set
SYMCC_INPUT_FILEto a path; bytes the program reads
from that exact file are treated as symbolic.
Here is a complete, self-contained file-based example.
Program that reads an integer from a file given as
argv[1]:#include <stdio.h> int main(int argc, char *argv[]) { FILE *f = fopen(argv[1], "r"); if (!f) { perror("fopen"); return 1; } int x; if (fscanf(f, "%d", &x) != 1) return 1; if (x > 100) printf("big\n"); else if (x < 100) printf("small\n"); else printf("equal\n"); fclose(f); return 0; }
Compile it normally and create a seed input file:
gcc readfile.c -o readfile printf '100' > seed mkdir -p output
Run SymQEMU:
SYMCC_INPUT_FILE=seed SYMCC_OUTPUT_DIR=output \ ./build/qemu-x86_64 ./readfile seedTwo points that are easy to miss:
SYMCC_INPUT_FILE=seedtells SymQEMU to treat the bytes read from
seedas symbolic.- The trailing
seedis the argument passed to the program so it knows
which file to open. The file the program opens must be the same file
named inSYMCC_INPUT_FILE; otherwise the program reads bytes that were
never marked symbolic and no test cases are produced.
With the seed
100the program takes theequalbranch, and SymQEMU
generates inputs that drive the program down the other branches, written
tooutput/. For example one of the generated files contained198,
which flips the program into thex > 100(big) branch.This is also why the original ArduPilot case produced nothing: it takes
its input from command-line arguments, andargvis not a supported
source of symbolic input (only stdin andSYMCC_INPUT_FILEare).- stdin (default): bytes the program reads from standard input are
We are attempting to perform symbolic execution testing on ArduPilot using SymQEMU, but SymQEMU fails to generate corresponding test cases during the program's runtime. The program utilizes command-line options as input.How do we solve this problem?