SymTEE finds TEE vulnerabilities with GPT-5 and symbolic execution

A team of researchers from Singapore Management University, Nanyang Technological University, and other institutions has developed SymTEE, a novel framework that combines large language models with symbolic execution to detect security vulnerabilities in Trusted Execution Environments (TEEs). TEEs provide hardware-enforced isolation for sensitive operations but are notoriously difficult to analyze due to their complex build environments and hardware isolation constraints.

The SymTEE framework addresses these challenges by using Abstract Syntax Tree analysis to identify TEE code slices that may lack proper input validation. It then leverages GPT-5 to automatically generate KLEE-compatible harness programs with lightweight mock execution environments, enabling symbolic analysis without the need for actual TEE hardware. In evaluations across 26 vulnerabilities (11 real-world and 15 synthetic cases), SymTEE demonstrated remarkable effectiveness—achieving 100% precision and 92.3% recall in detecting missing input validation issues, all at an average cost of just $0.05 per analysis.