Effective Domain-Specific Formal Verification Techniques

Ákos Hajdu's PhD dissertation, link: http://hdl.handle.net/10890/13523

The dissertation presents results on making formal verification more effective in three domains: (1) extending algorithms for verifying concurrent and asynchronous systems modeled with Petri nets, (2) new abstraction-based algorithms for verifying embedded software, and (3) verifying smart contracts for blockchains.

Transcript

1. Effective Domain-Specific Formal Verification Techniques Ákos Hajdu Advisor: Zoltán Micskei, PhD Public PhD defense 2020/11/24 Critical Systems Research Group Department of Measurement and Information Systems Budapest University of Technology and Economics
2. Effective Domain-Specific Formal Verification Techniques 2 • Critical systems and programs – Serious damage – Financial consequences • Formal verification – Rigorous reasoning – Find errors – Prove correctness Scope and Motivation
3. Effective Domain-Specific Formal Verification Techniques 3 Formal Verification System/program from a domain Formal model Formal property Verification algorithm Background logic Translation VC generation int abs(int x) { int y = x; if (y < 0) y = -y; return y; } y := x [y ≥ 0] [y < 0] y := -y Return y ≥ 0 y 0 = x Ʌ y 0 ≥ 0 Ʌ y 1 = y 0 => y 1 ≥ 0 y 0 = x Ʌ y 0 < 0 Ʌ y 1 = -y 0 => y 1 ≥ 0 (1) Holds (2) Holds
4. Effective Domain-Specific Formal Verification Techniques 4 Properties and Challenges Accepted desirables False alarms (incomplete) Missed violations (unsound) Caught violations Desirable behavior Violating behavior Passes Rejects Formal verification System or program Conclusive Terminate with answer Supported by verification Model and property space Inconclusive Resource limits reached Unsupported modeling element or property Conclusive answers Efficiency Expressive power Objective: effective trade-off in practice by balancing the challenges
5. Thesis 1 Extensions to the CEGAR Approach on Petri Nets Effective Domain-Specific Formal Verification Techniques 5 t 0 t 1 t 2 p 0 p 1 p 2 p 3
6. Effective Domain-Specific Formal Verification Techniques 6 Background Concurrent/asynchronous Inhibitor arcs Predicates State equation and CEGAR Integer linear programming Petri nets Reachability State space: H 2 O 2 H 2 O 4 2 0 2 1 2 0 0 4 t 0 t 0 t 1 t 1 H 2 O 2 H 2 O t 0 t 1 Place Token Transition T1.1 T1.2 T1.3 T1.4 2 2 2 2
7. Effective Domain-Specific Formal Verification Techniques 7 • State equation: structural abstraction for reachability – Integer linear programming problem – Encodes the acyclic part – Necessary but not sufficient criterion CEGAR Approach for Petri Nets −1 0 0 1 0 0 0 1 −1 0 −1 1 𝑚0 + 𝐶𝑥 = 𝑚1 Initial state Target state Transitions to be fired t 0 t 1 t 2 p 0 p 1 p 2 p 3 m 0 m m m 1 m m m m
8. Effective Domain-Specific Formal Verification Techniques 8 • Infeasible solution: introduce cyclical behavior – Extend equation with constraints: T-invariants – Iterative process: Counterexample-Guided Abstraction Refinement (CEGAR) CEGAR Approach for Petri Nets t 0 t 1 t 2 p 0 p 1 p 2 p 3 −1 0 0 1 0 0 0 1 −1 0 −1 1 𝑚0 + 𝐶𝑥 = 𝑚1 m 0 m m m 1 m m m m T-invariant Objective: increase expressive power and conclusive answers
9. Effective Domain-Specific Formal Verification Techniques 9 • Reachability of predicates – Linear predicate over state to be reached – E.g., define target state in one component – Transform predicates over places to predicates over transitions • Inhibitor arcs – Allow testing for emptiness – Turing complete expressive power – Reachability undecidable – Use cycles to “move tokens away” T1.1/T1.2 Improving Expressive Power 𝐴𝑚1 ≥ 𝑏 𝑚0 + 𝐶𝑥 = 𝑚1 𝐴𝐶 𝑥 ≥ 𝑏 − 𝐴𝑚0 t 0 t 1 t 2 p 0 p 1 p 2 p 3 t 0 cannot fire as long as p 2 has tokens
10. Effective Domain-Specific Formal Verification Techniques 10 • Involving an invariant might not help – Algorithm stops with inconclusive answer • Proposed approach – Involve another “distant” (indirect) invariant – Proper termination criterion needed – Keeping track of refinement progress • Search strategy – Standard: BFS, DFS – Hybrid strategy T1.3/T1.4 Increasing Conclusive Answers m 0 m m m 1 m m m m m m m m m
11. Effective Domain-Specific Formal Verification Techniques 11 • Scalability – Usually linear scalability w.r.t. marking – Often exponential w.r.t. net structure • Comparison – Original algorithm is more efficient, but the extended can answer more problems – Complementary to saturation (symbolic) • Search strategies – Hybrid strategy converges faster with less inconclusive results Evaluation
12. Effective Domain-Specific Formal Verification Techniques 12 I proposed various extensions and improvements to the CEGAR-based reachability analysis of Petri nets, lifting its expressive power and increasing the amount of conclusive answers. 1.1 I generalized the algorithm to be able to solve reachability of predicates, where the target state to be reached can be described with a set of linear constraints. 1.2 I extended the algorithm to be able to handle Petri nets with inhibitor arcs, raising its expressive power. 1.3 I defined the concept of distant invariants and proposed a new iteration strategy, which extended the kind of problems the algorithm could solve. 1.4 I defined a new ordering between partial solutions and a corresponding hybrid search strategy that can speed up the convergence of the algorithm without losing solutions. Publications: ActaCyb’14, ICATPN’15, SPLST’13, ICATPN’16, SCP’18 Thesis 1 – Summary Extensions to the efficient CEGAR-based analysis of Petri nets improve expressive power and increase conclusive answers. Σ
13. Thesis 2 Efficient Strategies for CEGAR- based Software Model Checking Effective Domain-Specific Formal Verification Techniques 13
14. Effective Domain-Specific Formal Verification Techniques 14 Background Embedded software Control-flow automata Reachability of location Predicates, explicit values and CEGAR Satisfiability modulo theories int x; 0: x = 0; 1: while (x < 5) { 2: x = x + 1; } 3: assert (x <= 5); 0 2 1 3 F E x := 0 x := x+1 [x < 5] [x ≥ 5] [x ≤ 5] [x > 5] Program Control-flow automata Assertion violation T2.1 T2.2 T2.3 T2.4
15. Effective Domain-Specific Formal Verification Techniques 15 • Tackle complexity with abstraction – Represent states w.r.t. an abstract domain Abstract Domains • Explicit-value abstraction – Subset of variables is tracked – Others are unknown int x = 0; for (int i = 0; i < 10000; i++) { x = (x + 1) % 10; } assert (x < 10); No need to track i to prove safety • Predicate abstraction – Track predicates instead concrete values int x = 0; while (x < 1000) { x++; } assert (x <= 1000); Track x < 1000 for loop exit Track x = 1000 for precise exit
16. Effective Domain-Specific Formal Verification Techniques 16 • Counterexample-Guided Abstraction Refinement – Iteratively build and refine abstraction – ARG: Abstract Reachability Graph (state space) CEGAR Abstraction Refinement ARG Safe Unsafe Abstract counterexample Refined precision Initial precision Build Prune Objective: Make CEGAR more efficient in software model checking
17. Effective Domain-Specific Formal Verification Techniques 17 • Configurable explicit domain – Unknown values (e.g., input, abstraction) – Try enumerating up to limit, propagate unknown above – Finer grained control of the level of abstraction • Error-based search strategy – Estimate distance to error using program graph – Under-approximation (A* search) – Safe programs also have intermediate (abstract) counterexamples T2.1/T2.2 More Efficient Abstraction x = ? 0 2 4 3 5 [x != 1] x = ? 3 1 2
18. Effective Domain-Specific Formal Verification Techniques 18 • Backward binary interpolation – Trace infeasibility back to earliest point • Multiple counterexamples – Collect more/all counterexamples – Overhead at abstraction – Refine at once – Better quality refinements – Shared refinements T2.3/T2.4 More Efficient Refinement … … x := 0 … … 2 [x > 0] … 1 3 3 counterexamples One refinement is sufficient Contradiction Ok up to this point Real reason lies here
19. Effective Domain-Specific Formal Verification Techniques 19 • Input models – 445 C tasks from SV-Comp – 90 PLC models from CERN – 300 benchmarks from HWMCC • Results – Configurable explicit domain combines advantages of abstraction and enumeration – Error-based search improves convergence – Backward analysis outperforms forward – Multiple counterexamples efficient on complex models Evaluation
20. Effective Domain-Specific Formal Verification Techniques 20 I proposed various improvements and strategies to CEGAR-based software model checking, increasing the efficiency of the algorithm. 2.1 I generalized explicit-value analysis to be able to enumerate a predefined, configurable number of successor states, improving its precision, but avoiding state space explosion. 2.2 I adapted a search strategy to the context of CEGAR that estimates the distance from the erroneous state in the abstract state space based on the structure of the software, efficiently guiding exploration towards counterexamples. 2.3 I introduced an interpolation strategy based on backward reachability, that traces back the reason of infeasibility to the earliest point in the program, yielding faster convergence. 2.4 I described an approach for refinement based on multiple counterexamples, which allows exchanging information between counterexamples and provides better refinements. Publications: JAR’19, FORTE’16, VPT’17, FMCAD’17, MiniSym’17, MiniSym’18 Thesis 2– Summary Efficient, CEGAR-based strategies help software model checking scale to industrial use cases. Σ OpenMBEE’20
21. Thesis 3 Modular Specification and Verification of Smart Contracts Effective Domain-Specific Formal Verification Techniques 21 The author was also affiliated with SRI International during the work described in this thesis.
22. Effective Domain-Specific Formal Verification Techniques 22 • The blockchain • Distributed ledgers Background Decentralized/blockchain
23. Effective Domain-Specific Formal Verification Techniques 23 • Conceptually a single global state • Distributed computing platforms – Executable code on ledger Background Decentralized/blockchain
24. Effective Domain-Specific Formal Verification Techniques 24 • Smart contracts (Solidity) Background Decentralized/blockchain Boogie IVL Modular spec. Modular program verification Satisfiability modulo theories Objective: Check high level, functional properties efficiently T3.1 T3.2 T3.3 T3.4 contract SimpleBank { } State variable Function Function mapping(address=>uint) balances; function deposit() public payable { balances[msg.sender] += msg.value; } function withdraw(uint amount) public { require(balances[msg.sender] >= amount); balances[msg.sender] -= amount; msg.sender.transfer(amount); }
25. Effective Domain-Specific Formal Verification Techniques 25 T3.1/T3.2 Annotations • Adapt modular properties – Contract level invariants – Pre/postconditions – Loop invariants • Domain specific extensions – Balances, transactions, … – Sum over collections /// invariant sum(balances) == this.balance contract SimpleBank { mapping(address=>uint) balances; function deposit() public payable { balances[msg.sender] += msg.value; } function withdraw(uint amount) public { require(balances[msg.sender] >= amount); balances[msg.sender] -= amount; msg.sender.transfer(amount); } }
26. Effective Domain-Specific Formal Verification Techniques 26 • Smart contracts → Boogie – SMT-based intermediate verification language • Similar to program verification, but much more in the details – Balances, payments – Message passing – Transactional behavior – Large bit-widths (256) T3.3/T3.4 Encoding to Boogie IVL Solidity uint8 x = 255; uint8 y = 1; x + y == 0; int x = 255; int y = 1; x + y == 256; bv8 x = 255bv8; bv8 y = 1bv8; x + y == 0bv8; int x = 255; int y = 1; (x + y) % 256 == 0; 8-256 bits, Wraparound overflow Boogie encoding SMT integers Scalable Not precise SMT bitvectors Precise Not scalable Modulo Precise Scalable
27. Effective Domain-Specific Formal Verification Techniques 27 • Unannotated contracts – Implicit specification – require, assert, overflows – Mostly false alarms due to wrong usage – Found some overflow issues • Annotated contracts – High level, functional properties – Detect, fix and prove real issues – Token overflow, reentrancy – Modular arithmetic is efficient – 256 bits, nonlinear properties Evaluation /// @notice invariant sum(balances) == totalSupply contract BecToken { using SafeMath for uint256; uint256 totalSupply; mapping(address => uint256) balances; function batchTransfer(address[] _recvs, uint256 _value) { uint cnt = _recvs.length; uint256 amount = uint256(cnt) * _value; require(cnt > 0 && cnt <= 20); require(_value > 0 && balances[msg.sender] >= amount); balances[msg.sender] = balances[msg.sender].sub(amount); /// @notice invariant totalSupply == sum(balances) + (cnt - i) * _value /// @notice invariant i <= cnt for (uint i = 0; i < cnt; i++) balances[_recvs[i]] = balances[_recvs[i]].add(_value); } }
28. Effective Domain-Specific Formal Verification Techniques 28 I defined a modular specification and verification approach for smart contracts by annotating and translating them to an intermediate verification language. 3.1 I adapted existing modular specification constructs to the context of smart contracts. 3.2 I proposed domain-specific annotations for the modular specification and verification of smart contracts. 3.3 I introduced a mapping from the Solidity contract-oriented programming language to the Boogie intermediate verification language. 3.4 I described a modular arithmetic encoding that supports scalable bit-precise reasoning on arithmetic operations. Publications: VSTTE’19, ESOP’20 Thesis 3 – Summary Modular specification and verification can check high level, functional properties of smart contracts efficiently. Σ FMBC’20, IEEE Access’20
29. Summary Effective Domain-Specific Formal Verification Techniques 29
30. Effective Domain-Specific Formal Verification Techniques 30 Publications Thesis 1 Thesis 2 Thesis 3 Journal ActaCyb SCP JAR Conference SPLST 2x ICATPN FORTE VPT FMCAD VSTTE ESOP Local event 2x BME Related to theses Highlights 19 publications • 3 journal (incl. JAR, SCP) • 8 conference (incl. ICATPN, FMCAD, ESOP) • 3 workshop (incl. VPT, FESCA) • 4 local event (BME) • 1 technical report (CERN) • 1 pending US patent 75+ citations based on Google Scholar 30 independent peer-reviewed 23 4 5 PGP 100+ 40+
31. • Free and open source tools • Case studies • Talks Effective Domain-Specific Formal Verification Techniques 31 Applications Education Modeling and analysis of public transport Formal verification of PLC codes Analysis of public smart contracts petridotnet.inf.mit.bme.hu/en github.com/FTSRG/theta github.com/SRI-CSL/solidity solcverify Fault injection
32. Effective Domain-Specific Formal Verification Techniques 32 Conclusions Concurrent/asynchronous Inhibitor arcs Predicates State equation and CEGAR Integer linear programming Petri nets Reachability Embedded software Control-flow automata Reachability of location Predicates, expl. vals. and CEGAR Satisfiability modulo theories Decentralized/blockchain Boogie IVL Modular specification Modular program verification Satisfiability modulo theories Thesis 1 Thesis 2 Thesis 3 • Check high-level, functional properties efficiently • Improve practical scalability • Improve expressive power and conclusive answers • Gazer: LLVM-based C frontend & SV-Comp • Gamma: statechart frontend Ongoing work after the dissertation: • Spec and verif. of events • Fault injection • Upgrade Solidity version