AI Boosted Verifier
The correctness of smart contract is essential as they control billions
dollars worth of digital asset on blockchain platform. Unfortunately, existing approaches
using static analysis and manual auditing are proved to fail: static analysis techniques
suffer from false positive and the requirement for attack pattern, while manual auditing
is too labor-intensive and error-prone.
To mitigate the security concern on smart contract, we present an efficient formal verifier for smart contract. It employs symbolic execution and abstract interpretation techniques to verify contract behaviors against a set of safety specifications. Our formal verifier ensures sound and accurate result, as it explores all possible execution states of a smart contract, and at the same time guarantees practicality by abstracting out complicated blockchain storage.
Our formal verifier uses a novel abstract-refinement apparoch to resolve the state explosion problem which commonly presented in verification, and meanwhile tries to refine its inaccuracy by counterexample elimination.
At the beginning, the smart contract bytecode and a relevant safety specification are used as inputs. Optionally, user may also provide some predicates as hint to optimize the verification.
At pre-process stage, both the bytecode and specifications (as well as predicates if provided) are processed together, so that specifications can be parsed and converted into reachability problems which can be intrumented as assertions in the bytecode.
A symbolic execution engine is later used to check the behavior of contract at each transcation. Between each iteration, symbolic contract states are optimized using abstractions to resolve state explosion issues. The symbolic execution will stop when contract states reach a fixed point.
Abstract states are verified against instrumented properties using SAT solver. If the solver produces SAT, specification is verified as no violation. However, as our abstraction may introduce over-approximation, counterexamples need to be further confirmed if the solver gives UNSAT. The verification will finish as specification violation if counterexamples are proved to be true violation. Otherwise, counterexample is removed from contract state and SAT solver is invoked again.
We express safety properties using past linear temporal logic, or Past LTL for short. For further details on our specification language please refer to developer document .
To mitigate the security concern on smart contract, we present an efficient formal verifier for smart contract. It employs symbolic execution and abstract interpretation techniques to verify contract behaviors against a set of safety specifications. Our formal verifier ensures sound and accurate result, as it explores all possible execution states of a smart contract, and at the same time guarantees practicality by abstracting out complicated blockchain storage.
Our formal verifier uses a novel abstract-refinement apparoch to resolve the state explosion problem which commonly presented in verification, and meanwhile tries to refine its inaccuracy by counterexample elimination.
At the beginning, the smart contract bytecode and a relevant safety specification are used as inputs. Optionally, user may also provide some predicates as hint to optimize the verification.
At pre-process stage, both the bytecode and specifications (as well as predicates if provided) are processed together, so that specifications can be parsed and converted into reachability problems which can be intrumented as assertions in the bytecode.
A symbolic execution engine is later used to check the behavior of contract at each transcation. Between each iteration, symbolic contract states are optimized using abstractions to resolve state explosion issues. The symbolic execution will stop when contract states reach a fixed point.
Abstract states are verified against instrumented properties using SAT solver. If the solver produces SAT, specification is verified as no violation. However, as our abstraction may introduce over-approximation, counterexamples need to be further confirmed if the solver gives UNSAT. The verification will finish as specification violation if counterexamples are proved to be true violation. Otherwise, counterexample is removed from contract state and SAT solver is invoked again.
We express safety properties using past linear temporal logic, or Past LTL for short. For further details on our specification language please refer to developer document .
Updated 7 months ago