KLEE

💎Vulnerabiltiies to be discovered

The next vulnerabilities should be discovered in this sections:

• VULN-RECOVERY-OOB

⚙️AFL++ setup

If you didn't set up the dynamic-analysis profile's infrastructure, please do so by running the command docker-compose --profile dynamic-analysis up.

Use docker exec --interactive --tty klee bash to enter the container where the CLI application is contained.

📚KLEE documentation

The KLEE documentation is available here.

Steps

Obtaining the LLVM bytecode

1. At the moment, the files from sandcastle/c_modules are used to compile a shared object using Makefile. Copy the folder with C sources in /root/analysis/klee/c_modules and modify test.c to call generate_recovery_token with two variables, which are both marked as symbolic variables (with the klee_make_symbolic method)
2. Use clang to generate the LLVM bytecode.

🚧Solution

To display the solution of this task, enter the text i-surrender-to-the-code-security-gods in the field below.

Symbolically executing the LLVM bytecode

1. Use klee to run the generated file with the LLVM bytecode

🚧Solution

To display the solution of this task, enter the text i-surrender-to-the-code-security-gods in the field below.

Validating the test cases

1. Compile again the program using the -lkleeRuntest flag.
2. For each test case, run the program and check if it is crashing.
3. Inspect the associated test<n>.<type>.err file to see where in the program the problem appears.

🚧Solution

To display the solution of this task, enter the text i-surrender-to-the-code-security-gods in the field below.