VeriChain: A Hybrid Formal Verification Approach Using Control Flow, Symbolic Execution, and Static Analysis for Smart Contract Vulnerability Detection.
Saved in:
| Title: | VeriChain: A Hybrid Formal Verification Approach Using Control Flow, Symbolic Execution, and Static Analysis for Smart Contract Vulnerability Detection. |
|---|---|
| Authors: | Ramesh, Vankudoth1 v.ramesh406@gmail.com, Reddy, K. Govardhan2 govardhan.cse@gprec.ac.in |
| Source: | Informatica (03505596). Mar2026, Vol. 50 Issue 1, p25-43. 19p. |
| Subjects: | Formal verification, Flowgraphs, Computer software testing, Blockchains, Penetration testing (Computer security) |
| Abstract (English): | Smart contracts facilitate the trustless and automated execution of agreements on blockchains, however several programming patterns in them (such as re-entrancy, integer overflow/underflow, access control) have led to substantial thefts due to vulnerabilities. Current verification tools (e.g., Mythril, Oyente, and Securify) are essentially based on symbolic execution, taint analysis, and pattern matching with high falsepositives as well as large time cost, poor scalability for complex contracts. This paper develops VeriChain, a hybrid verification framework that combines (i) lexicon/syntax parsing for abstract syntax tree (AST), (ii) Control Flow Graph (CFG) generation for path and dependency representation, (iii) CFG-guided symbolic execution with model checking to search feasible execution paths and (iv) rule-based static analysis towards identifying/characterizing vulnerability patterns. VeriChain was tested on N benchmark smart contracts (including re-entrancy, arithmetic and access-control vulnerabilities) and contrasted with Mythril, Oyente, and Securify. Experiments show that VeriChain enables 98.3% detection accuracy with only 1 false positive (and no false negative in our testing set) and finishes analysis within 2.3 seconds, surpassing state-of-the-art tools in both precision and execution efficiency. VeriChain also outputs a structured security report to categorise detected flaws by severity and to offer developers traces of execution as well as mitigation advice, enabling realistic pre-deployment audit of blockchain smart contract. [ABSTRACT FROM AUTHOR] |
| Abstract (Slovenian): | Predstavljen je napreden sistem za odkrivanje ranljivosti v pametnih pogodbah, ki deluje natančneje in hitreje kot obstoječe rešitve. [ABSTRACT FROM AUTHOR] |
| Copyright of Informatica (03505596) is the property of Slovene Society Informatika and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Links: – Type: pdflink Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 194608714 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: VeriChain: A Hybrid Formal Verification Approach Using Control Flow, Symbolic Execution, and Static Analysis for Smart Contract Vulnerability Detection. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Ramesh%2C+Vankudoth%22">Ramesh, Vankudoth</searchLink><relatesTo>1</relatesTo><i> v.ramesh406@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Reddy%2C+K%2E+Govardhan%22">Reddy, K. Govardhan</searchLink><relatesTo>2</relatesTo><i> govardhan.cse@gprec.ac.in</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Informatica+%2803505596%29%22">Informatica (03505596)</searchLink>. Mar2026, Vol. 50 Issue 1, p25-43. 19p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Formal+verification%22">Formal verification</searchLink><br /><searchLink fieldCode="DE" term="%22Flowgraphs%22">Flowgraphs</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+testing%22">Computer software testing</searchLink><br /><searchLink fieldCode="DE" term="%22Blockchains%22">Blockchains</searchLink><br /><searchLink fieldCode="DE" term="%22Penetration+testing+%28Computer+security%29%22">Penetration testing (Computer security)</searchLink> – Name: Abstract Label: Abstract (English) Group: Ab Data: Smart contracts facilitate the trustless and automated execution of agreements on blockchains, however several programming patterns in them (such as re-entrancy, integer overflow/underflow, access control) have led to substantial thefts due to vulnerabilities. Current verification tools (e.g., Mythril, Oyente, and Securify) are essentially based on symbolic execution, taint analysis, and pattern matching with high falsepositives as well as large time cost, poor scalability for complex contracts. This paper develops VeriChain, a hybrid verification framework that combines (i) lexicon/syntax parsing for abstract syntax tree (AST), (ii) Control Flow Graph (CFG) generation for path and dependency representation, (iii) CFG-guided symbolic execution with model checking to search feasible execution paths and (iv) rule-based static analysis towards identifying/characterizing vulnerability patterns. VeriChain was tested on N benchmark smart contracts (including re-entrancy, arithmetic and access-control vulnerabilities) and contrasted with Mythril, Oyente, and Securify. Experiments show that VeriChain enables 98.3% detection accuracy with only 1 false positive (and no false negative in our testing set) and finishes analysis within 2.3 seconds, surpassing state-of-the-art tools in both precision and execution efficiency. VeriChain also outputs a structured security report to categorise detected flaws by severity and to offer developers traces of execution as well as mitigation advice, enabling realistic pre-deployment audit of blockchain smart contract. [ABSTRACT FROM AUTHOR] – Name: Abstract Label: Abstract (Slovenian) Group: Ab Data: Predstavljen je napreden sistem za odkrivanje ranljivosti v pametnih pogodbah, ki deluje natančneje in hitreje kot obstoječe rešitve. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Informatica (03505596) is the property of Slovene Society Informatika and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=194608714 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.31449/inf.v50i1.9267 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 19 StartPage: 25 Subjects: – SubjectFull: Formal verification Type: general – SubjectFull: Flowgraphs Type: general – SubjectFull: Computer software testing Type: general – SubjectFull: Blockchains Type: general – SubjectFull: Penetration testing (Computer security) Type: general Titles: – TitleFull: VeriChain: A Hybrid Formal Verification Approach Using Control Flow, Symbolic Execution, and Static Analysis for Smart Contract Vulnerability Detection. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Ramesh, Vankudoth – PersonEntity: Name: NameFull: Reddy, K. Govardhan IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 03 Text: Mar2026 Type: published Y: 2026 Identifiers: – Type: issn-print Value: 03505596 Numbering: – Type: volume Value: 50 – Type: issue Value: 1 Titles: – TitleFull: Informatica (03505596) Type: main |
| ResultId | 1 |
