SymTEE: Finding Missing Input Validation in TEEs via LLM-Assisted Symbolic Execution

Dependence

• Host OS: Ubuntu 22.04
• Python 3.12
• KLEE

Directory Structure

• benchmark: Contains TEE projects used to evaluate SymTEE.
• slicer.py: Extracting the code slices with AST analysis.
• klee_gen.py: Generating the KLEE-supported code file.

Preparation

1. Create Python 3.12 venv with tree-sitter-languages, tree_sitter and openai.

python3.12 -m venv py312
source py312/bin/activate
pip install tree-sitter-languages
pip install tree_sitter==0.21.3
pip install --upgrade openai

2. KLEE installation by brew.

sudo apt-get install build-essential curl file git
sudo apt-get install gcc-multilib g++-multilib
/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
brew install klee

Usage

1. AST analysis

python slicer.py <path_to_c_file_or_directory>

Code slices that may have vulnerabilities will be extracted to the folder slices/.

2. KLEE analysis

First, generate the KLEE-supported file with gpt-5, the generated code file will be placed into klee_output/.

export OPENAI_API_KEY="sk-xxxx"
python klee_gen.py <path_to_sliced_c_file> --model gpt-5 --output_dir ./klee_output

Then, compile the code into an LLVM bitfile.

clang -I /home/linuxbrew/.linuxbrew/opt/klee/include/ -emit-llvm -c <path_to_generated_c_file> -o <output_bc_file>.bc

Finally, do the symbolic execution analysis

klee <output_bc_file>.bc