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

• URL: http://arxiv.org/abs/2605.22058v1
• Date: Thu, 21 May 2026 06:47:36 GMT
• Title: Finding Missing Input Validation in TEEs via LLM-Assisted Symbolic Execution
• Abstract summary: This paper presents SymTEE, a novel large language model (LLM)-assisted symbolic execution framework.<n>SymTEE detects missing input validation issues in TEE applications without requiring real TEE setups.<n> Evaluations show that SymTEE achieves 100% precision and 92.3% recall in detecting missing input validation vulnerabilities.
• Score: 13.508257116044021
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Trusted Execution Environments (TEEs) provide hardware-enforced isolation that protects sensitive code and data from untrusted software. Despite their strong security guarantees, analyzing TEE applications remains challenging due to the high cost and complexity of configuring complete TEE build and runtime environments, as well as the limited observability imposed by hardware isolation. This paper presents SymTEE, a novel large language model (LLM)-assisted symbolic execution framework for detecting missing input validation issues in TEE applications without requiring real TEE setups. SymTEE begins by leveraging Abstract Syntax Tree (AST) analysis to extract TEE code slices that may lack sufficient input validation, and then employs an LLM (GPT-5 in our case) to automatically convert the extracted slices into KLEE-compatible harness programs containing lightweight mock execution environments for symbolic analysis. Evaluations on 26 vulnerabilities (11 real-world and 15 synthetic) show that SymTEE achieves 100% precision and 92.3% recall in detecting missing input validation vulnerabilities while incurring an average analysis cost of only $0.05. These results demonstrate the effectiveness and practicality of SymTEE's pioneering paradigm of LLM-assisted symbolic execution, where LLMs autonomously generate mock environments to enable automated security analysis without complex setup, providing a more accessible and scalable framework for trusted computing systems.

Related papers

• LLMs for Secure Hardware Design and Related Problems: Opportunities and Challenges [13.013353332008869]
  Large Language Models (LLMs) are being integrated into Electronic Design Automation (EDA) and hardware security.<n>LLMs offer unprecedented capabilities in generating Register Transfer Level (RTL) code, automating testbenches, and bridging the semantic gap between high-level specifications and silicon.<n>This review provides an in-depth analysis of the state-of-the-art in LLM-driven hardware design, organized around key advancements in EDA synthesis, hardware trust, design for security, and education.
  arXiv  Detail & Related papers  (2026-05-11T16:31:14Z)
• SecureForge: Finding and Preventing Vulnerabilities in LLM-Generated Code via Prompt Optimization [61.91729298584227]
  We introduce SecureForge, an automated pipeline that audits security risks of frontier models and produces auditing-informed secure system prompts.<n>SecureForge first identifies benign prompts that produce statically detectable vulnerabilities, and then amplifies them into a large synthetic prompt corpus of diverse scenarios.<n>On frontier models, SecureForge yields a statistically significant improvement in both unit test success and output security, with output vulnerabilities reduced by up to 48%.
  arXiv  Detail & Related papers  (2026-05-08T18:40:47Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Multi-Agent Taint Specification Extraction for Vulnerability Detection [49.27772068704498]
  Static Application Security Testing (SAST) tools using taint analysis are widely viewed as providing higher-quality vulnerability detection results.<n>We present SemTaint, a multi-agent system that strategically combines the semantic understanding of Large Language Models (LLMs) with traditional static program analysis.<n>We integrate SemTaint with CodeQL, a state-of-the-art SAST tool, and demonstrate its effectiveness by detecting 106 of 162 vulnerabilities previously undetectable by CodeQL.
  arXiv  Detail & Related papers  (2026-01-15T21:31:51Z)
• FLAMES: Fine-tuning LLMs to Synthesize Invariants for Smart Contract Security [41.836337574143535]
  FLAMES is an automated approach that synthesizes runtime guards as Solidity "require" statements to harden smart contracts against exploits.<n>FLAMES employs domain-adapted large language models trained through fill-in-the-middle supervised fine-tuning on real-world invariants extracted from 514,506 verified contracts.
  arXiv  Detail & Related papers  (2025-10-24T12:44:08Z)
• ParaVul: A Parallel Large Language Model and Retrieval-Augmented Framework for Smart Contract Vulnerability Detection [43.41293570032631]
  ParaVul is a retrieval-augmented framework to improve the reliability and accuracy of smart contract vulnerability detection.<n>We develop Sparse Low-Rank Adaptation (SLoRA) for LLM fine-tuning.<n>We construct a vulnerability contract dataset and develop a hybrid Retrieval-Augmented Generation (RAG) system.
  arXiv  Detail & Related papers  (2025-10-20T03:23:41Z)
• Towards Effective Complementary Security Analysis using Large Language Models [3.203446435054805]
  A key challenge in security analysis is the manual evaluation of potential security weaknesses generated by static application security testing (SAST) tools.<n>We propose using Large Language Models (LLMs) to improve the assessment of SAST findings.
  arXiv  Detail & Related papers  (2025-06-20T10:46:35Z)
• SEC-bench: Automated Benchmarking of LLM Agents on Real-World Software Security Tasks [11.861657542626219]
  SEC-bench is the first fully automated benchmarking framework for evaluating large language model (LLM) agents.<n>Our framework automatically creates high-quality software vulnerability datasets with reproducible artifacts at a cost of only $0.87 per instance.<n>A comprehensive evaluation of state-of-the-art LLM code agents reveals significant performance gaps.
  arXiv  Detail & Related papers  (2025-06-13T13:54:30Z)
• AutoPT: How Far Are We from the End2End Automated Web Penetration Testing? [54.65079443902714]
  We introduce AutoPT, an automated penetration testing agent based on the principle of PSM driven by LLMs. Our results show that AutoPT outperforms the baseline framework ReAct on the GPT-4o mini model.
  arXiv  Detail & Related papers  (2024-11-02T13:24:30Z)
• IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities [14.188864624736938]
  Large language models (or LLMs) have shown impressive code generation capabilities but they cannot do complex reasoning over code to detect such vulnerabilities.<n>We propose IRIS, a neuro-symbolic approach that systematically combines LLMs with static analysis to perform whole-repository reasoning for security vulnerability detection.
  arXiv  Detail & Related papers  (2024-05-27T14:53:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.