![[Home]](http://www.bayleshanks.com/cartoonbayle.png)
Difference between revision 7 and current revision
No diff available.---
eth formal verification
swordswinger12 1 day ago
The IC3 research group at Cornell, and especially Elaine Shi's group, has been thinking about this recently. They are (I think) working on some kind of program analysis framework using deep PL techniques to formally verify smart contracts.
reply
pipermerriam 1 day ago
There is actually already fledgling support for this in Solidity (the prevailing language that Ethereum developers use to write smart contracts).
https://forum.ethereum.org/discussion/3779/formal-verification-for-solidity-contracts
---
https://www.reddit.com/r/ethereum/comments/4uu9fb/formal_verification_for_solidity/
" The second iteration of formal verification features for Solidity has been released!
It is now possible to verify re-entrancy effects using invariants!
Listen to a talk about it or just view the slides - the talk includes a live demo that shows how to use the new feature in browser-solidity.
What can be done with it: Not all of Solidity is supported, you will see error messages if you use unsupported parts of Solidity. Basically, the uint type, arrays of it, arithmetics on it, assignments, while loops, if statements, functions, internal function calls (also recursive) and sending Ether via .call.value(x)() is supported.
What is not supported: Function calls to other contracts (apart from sending Ether), the msg and block variables (receiving ether is not yet modeled), mappings, custom datatypes and datatypes other than uint.
How are effects of reentrant calls handled? Any conditions that are used atop of the contract definition are automatically applied to (and verified for) all functions of the contract. For now, you still have to make sure that these conditions are transitive. This means that a condition of the form "the balance increases by 1" is invalid (because two calls will not satisfy the condition) and the system will not yet notice that. In contrast, a condition of the form "the balance will not decrease" is valid.
What are the next steps? The next step is to add support for mappings, so that it is possible to formally verify a simple EIP20 token.
Comments welcome!
"
---
" Animats 128 days ago [-]
The system: [1] The Nelson-Oppen decision procedure: [2]
There's a subset of of arithmetic and logic that's completely decidable. It includes addition, subtraction, multiplication by constants, "if", the theory of arrays, a similar theory of structures, and the Boolean operators (on bools, not integers.) This is enough for most subscript and overflow checks. Complete solvers exist for this subset. If you try to prove all constraints that need run-time checks with this approach, you can eliminate maybe 80-90% of run time checks as unnecessary.
Some checks cannot be eliminated, but can be hoisted out of loops. This means making one check before entering the loop, rather than one on each iteration. FOR statements usually can be optimized in this way. That's almost a no-brainer in modern compilers. The "Go" compiler does this. Heavier machinery is needed for more complex loops.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
[2] http://www.cs.cmu.edu/~joshuad/NelsonOppen.pdf "
links 2 abstract:
A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and _<, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier. Key Words and Phrases: program verification, program manipulation, theorem proving, decidability, simplificatio
---
i guess for Oot it would be coolest if we could define ASSERT in terms of a statements that meant "(at this point in the program) (EXPRESSION) is true", eg if the noun phrase "this point in the program" were reified and if the phrase "at this point in the program" were reified, so then you could use the ordinary logic programming syntax to say "EXPRESSION is true"
---
verification:
https://isabelle.in.tum.de/overview.html
---
mentions