filmov
tv
[N40AI'24] Trust but Verify: Scaling Deductive Verification with Abstract Interpretation
Показать описание
[N40AI'24] Trust but Verify: Scaling Deductive Verification with Abstract Interpretation
Mooly Sagiv
The Certora Prover formally verifies high-level functional correctness properties of low-level smart contract code using automated techniques. Most real-world programs that the Certora Prover verifies are large and complex. Verification conditions generated by straightforward translation to SMT are frequently too complex for solvers, leading to slow verification times and timeouts.
To scale this product to realistic code, we developed a unique pointer analysis algorithm for low-level code. Our algorithm assumes certain invariants about low-level code generated by the compiler but verifies that the invariants are met. This algorithm has uncovered security errors in the Solidity compiler and sped up formal verification by orders of magnitude in several cases by enabling sound program simplifications. A key challenge in developing pointer analysis for low-level code in the domain of smart contracts is that the EVM manages memory using strategies like bump allocation that, while practical for usage in the blockchain, make analysis harder.
In this talk, I will first describe some lessons learned over the past five years at Certora and then suggest new static analysis problems for our community to target as new low-level languages like EVM bytecode and WebAssembly become more popular.
Mooly Sagiv
The Certora Prover formally verifies high-level functional correctness properties of low-level smart contract code using automated techniques. Most real-world programs that the Certora Prover verifies are large and complex. Verification conditions generated by straightforward translation to SMT are frequently too complex for solvers, leading to slow verification times and timeouts.
To scale this product to realistic code, we developed a unique pointer analysis algorithm for low-level code. Our algorithm assumes certain invariants about low-level code generated by the compiler but verifies that the invariants are met. This algorithm has uncovered security errors in the Solidity compiler and sped up formal verification by orders of magnitude in several cases by enabling sound program simplifications. A key challenge in developing pointer analysis for low-level code in the domain of smart contracts is that the EVM manages memory using strategies like bump allocation that, while practical for usage in the blockchain, make analysis harder.
In this talk, I will first describe some lessons learned over the past five years at Certora and then suggest new static analysis problems for our community to target as new low-level languages like EVM bytecode and WebAssembly become more popular.