NeuroSCA: Neuro-Symbolic Constraint Abstraction for Smart Contract Hybrid Fuzzing
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866912935047069696 |
|---|---|
| author | Liang, Haochen Chen, Jiawei Ochiai, Hideya |
| author_facet | Liang, Haochen Chen, Jiawei Ochiai, Hideya |
| contents | Hybrid fuzzing combines greybox fuzzing's throughput with the precision of symbolic execution to uncover deep smart contract vulnerabilities. However, its effectiveness is often limited by constraint pollution: in real world contracts, path conditions pick up semantic noise from global state and defensive checks that are syntactically intertwined with, but semantically peripheral to, the target branch, causing SMT timeouts. We propose NeuroSCA (Neuro-Symbolic Constraint Abstraction), a lightweight framework that selectively inserts a Large Language Model (LLM) as a semantic constraint abstraction layer. NeuroSCA uses the LLM to identify a small core of goal-relevant constraints, solves only this abstraction with an SMT solver, and validates models via concrete execution in a verifier-in-the-loop refinement mechanism that reintroduces any missed constraints and preserves soundness. Experiments on real-world contracts show that NeuroSCA speeds up solving on polluted paths, increases coverage and bug-finding rates on representative hard contracts, and, through its selective invocation policy, achieves these gains with only modest overhead and no loss of effectiveness on easy contracts. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_01272 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | NeuroSCA: Neuro-Symbolic Constraint Abstraction for Smart Contract Hybrid Fuzzing Liang, Haochen Chen, Jiawei Ochiai, Hideya Software Engineering Hybrid fuzzing combines greybox fuzzing's throughput with the precision of symbolic execution to uncover deep smart contract vulnerabilities. However, its effectiveness is often limited by constraint pollution: in real world contracts, path conditions pick up semantic noise from global state and defensive checks that are syntactically intertwined with, but semantically peripheral to, the target branch, causing SMT timeouts. We propose NeuroSCA (Neuro-Symbolic Constraint Abstraction), a lightweight framework that selectively inserts a Large Language Model (LLM) as a semantic constraint abstraction layer. NeuroSCA uses the LLM to identify a small core of goal-relevant constraints, solves only this abstraction with an SMT solver, and validates models via concrete execution in a verifier-in-the-loop refinement mechanism that reintroduces any missed constraints and preserves soundness. Experiments on real-world contracts show that NeuroSCA speeds up solving on polluted paths, increases coverage and bug-finding rates on representative hard contracts, and, through its selective invocation policy, achieves these gains with only modest overhead and no loss of effectiveness on easy contracts. |
| title | NeuroSCA: Neuro-Symbolic Constraint Abstraction for Smart Contract Hybrid Fuzzing |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2603.01272 |