cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

SMTChecker tutorial and docs cleanup

Browse Source
This commit is contained in:
Leonardo Alt
2021-03-18 11:09:26 +01:00
parent e179d0aa4d
commit 569afe711a
3 changed files with 738 additions and 288 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/security-considerations.rst
-288
View File
@@ -413,291 +413,3 @@ Ask for Peer Review
The more people examine a piece of code, the more issues are found.
Asking people to review your code also helps as a cross-check to find out whether your code
is easy to understand - a very important criterion for good smart contracts.
.. _formal_verification:
*******************
Formal Verification
*******************
Using formal verification, it is possible to perform an automated mathematical
proof that your source code fulfills a certain formal specification.
The specification is still formal (just as the source code), but usually much
simpler.
Note that formal verification itself can only help you understand the
difference between what you did (the specification) and how you did it
(the actual implementation). You still need to check whether the specification
is what you wanted and that you did not miss any unintended effects of it.
Solidity implements a formal verification approach based on SMT solving. The
SMTChecker module automatically tries to prove that the code satisfies the
specification given by ``require/assert`` statements. That is, it considers
``require`` statements as assumptions and tries to prove that the conditions
inside ``assert`` statements are always true. If an assertion failure is
found, a counterexample is given to the user, showing how the assertion can be
violated.
The other verification targets that the SMTChecker checks at compile time are:
- Arithmetic underflow and overflow (`underflow` and `overflow`).
- Division by zero (`divByZero`).
- Trivial conditions and unreachable code (`constantCondition`).
- Popping an empty array (`popEmptyArray`).
- Insufficient funds for a transfer (`balance`).
The names after each target above can be used when specifying subsets of targets.
It is currently an experimental feature, therefore in order to use it you need
to enable it via :ref:`a pragma directive<smt_checker>`.
The SMTChecker traverses the Solidity AST creating and collecting program constraints.
When it encounters a verification target, an SMT solver is invoked to determine the outcome.
If a check fails, the SMTChecker provides specific input values that lead to the failure.
While the SMTChecker encodes Solidity code into SMT constraints, it contains two
reasoning engines that use that encoding in different ways.
SMT Encoding
============
The SMT encoding tries to be as precise as possible, mapping Solidity types
and expressions to their closest `SMT-LIB <http://smtlib.cs.uiowa.edu/>`_
representation, as shown in the table below.
+-----------------------+--------------------------------+-----------------------------+
|Solidity type |SMT sort |Theories (quantifier-free) |
+=======================+================================+=============================+
|Boolean |Bool |Bool |
+-----------------------+--------------------------------+-----------------------------+
|intN, uintN, address, |Integer |LIA, NIA |
|bytesN, enum | | |
+-----------------------+--------------------------------+-----------------------------+
|array, mapping, bytes, |Tuple |Datatypes, Arrays, LIA |
|string |(Array elements, Integer length)| |
+-----------------------+--------------------------------+-----------------------------+
|struct |Tuple |Datatypes |
+-----------------------+--------------------------------+-----------------------------+
|other types |Integer |LIA |
+-----------------------+--------------------------------+-----------------------------+
Types that are not yet supported are abstracted by a single 256-bit unsigned
integer, where their unsupported operations are ignored.
For more details on how the SMT encoding works internally, see the paper
`SMT-based Verification of Solidity Smart Contracts <https://github.com/leonardoalt/text/blob/master/solidity_isola_2018/main.pdf>`_.
Model Checking Engines
======================
The SMTChecker module implements two different reasoning engines that use the
SMT encoding above, a Bounded Model Checker (BMC) and a system of Constrained
Horn Clauses (CHC). Both engines are currently under development, and have
different characteristics.
Bounded Model Checker (BMC)
---------------------------
The BMC engine analyzes functions in isolation, that is, it does not take the
overall behavior of the contract throughout many transactions into account when
analyzing each function. Loops are also ignored in this engine at the moment.
Internal function calls are inlined as long as they are not recursive, direct
or indirectly. External function calls are inlined if possible, and knowledge
that is potentially affected by reentrancy is erased.
The characteristics above make BMC easily prone to reporting false positives,
but it is also lightweight and should be able to quickly find small local bugs.
Constrained Horn Clauses (CHC)
------------------------------
The Solidity contract's Control Flow Graph (CFG) is modelled as a system of
Horn clauses, where the lifecycle of the contract is represented by a loop
that can visit every public/external function non-deterministically. This way,
the behavior of the entire contract over an unbounded number of transactions
is taken into account when analyzing any function. Loops are fully supported
by this engine. Internal function calls are supported, but external function
calls are currently unsupported.
The CHC engine is much more powerful than BMC in terms of what it can prove,
and might require more computing resources.
Abstraction and False Positives
===============================
The SMTChecker implements abstractions in an incomplete and sound way: If a bug
is reported, it might be a false positive introduced by abstractions (due to
erasing knowledge or using a non-precise type). If it determines that a
verification target is safe, it is indeed safe, that is, there are no false
negatives (unless there is a bug in the SMTChecker).
In the BMC engine, function calls to the same contract (or base contracts) are
inlined when possible, that is, when their implementation is available. Calls
to functions in other contracts are not inlined even if their code is
available, since we cannot guarantee that the actual deployed code is the same.
The CHC engine creates nonlinear Horn clauses that use summaries of the called
functions to support internal function calls. The same approach can and will be
used for external function calls, but the latter requires more work regarding
the entire state of the blockchain and is still unimplemented.
Complex pure functions are abstracted by an uninterpreted function (UF) over
the arguments.
+-----------------------------------+--------------------------------------+
|Functions |SMT behavior |
+===================================+======================================+
|``assert`` |Verification target |
+-----------------------------------+--------------------------------------+
|``require`` |Assumption |
+-----------------------------------+--------------------------------------+
|internal |BMC: Inline function call |
| |CHC: Function summaries |
+-----------------------------------+--------------------------------------+
|external |BMC: Inline function call or |
| |erase knowledge about state variables |
| |and local storage references. |
| |CHC: Function summaries and erase |
| |state knowledge. |
+-----------------------------------+--------------------------------------+
|``gasleft``, ``blockhash``, |Abstracted with UF |
|``keccak256``, ``ecrecover`` | |
|``ripemd160``, ``addmod``, | |
|``mulmod`` | |
+-----------------------------------+--------------------------------------+
|pure functions without |Abstracted with UF |
|implementation (external or | |
|complex) | |
+-----------------------------------+--------------------------------------+
|external functions without |BMC: Unsupported |
|implementation |CHC: Nondeterministic summary |
+-----------------------------------+--------------------------------------+
|others |Currently unsupported |
+-----------------------------------+--------------------------------------+
Using abstraction means loss of precise knowledge, but in many cases it does
not mean loss of proving power.
::
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.5.0;
pragma experimental SMTChecker;
// This may report a warning if no SMT solver available.
contract Recover
{
function f(
bytes32 hash,
uint8 _v1, uint8 _v2,
bytes32 _r1, bytes32 _r2,
bytes32 _s1, bytes32 _s2
) public pure returns (address) {
address a1 = ecrecover(hash, _v1, _r1, _s1);
require(_v1 == _v2);
require(_r1 == _r2);
require(_s1 == _s2);
address a2 = ecrecover(hash, _v2, _r2, _s2);
assert(a1 == a2);
return a1;
}
}
In the example above, the SMTChecker is not expressive enough to actually
compute ``ecrecover``, but by modelling the function calls as uninterpreted
functions we know that the return value is the same when called on equivalent
parameters. This is enough to prove that the assertion above is always true.
Abstracting a function call with an UF can be done for functions known to be
deterministic, and can be easily done for pure functions. It is however
difficult to do this with general external functions, since they might depend
on state variables.
External function calls also imply that any current knowledge that the
SMTChecker might have regarding mutable state variables needs to be erased to
guarantee no false negatives, since the called external function might direct
or indirectly call a function in the analyzed contract that changes state
variables.
Reference Types and Aliasing
=============================
Solidity implements aliasing for reference types with the same :ref:`data
location<data-location>`.
That means one variable may be modified through a reference to the same data
area.
The SMTChecker does not keep track of which references refer to the same data.
This implies that whenever a local reference or state variable of reference
type is assigned, all knowledge regarding variables of the same type and data
location is erased.
If the type is nested, the knowledge removal also includes all the prefix base
types.
::
// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.5.0;
pragma experimental ABIEncoderV2;
pragma experimental SMTChecker;
// This will report a warning
contract Aliasing
{
uint[] array1;
uint[][] array2;
function f(
uint[] memory a,
uint[] memory b,
uint[][] memory c,
uint[] storage d
) internal {
array1[0] = 42;
a[0] = 2;
c[0][0] = 2;
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
assert(array1[0] == 42);
// However, an assignment to a storage reference will erase
// storage knowledge accordingly.
d[0] = 2;
// Fails as false positive because of the assignment above.
assert(array1[0] == 42);
// Fails because `a == b` is possible.
assert(a[0] == 2);
// Fails because `c[i] == b` is possible.
assert(c[0][0] == 2);
assert(d[0] == 2);
assert(b[0] == 1);
}
function g(
uint[] memory a,
uint[] memory b,
uint[][] memory c,
uint x
) public {
f(a, b, c, array2[x]);
}
}
After the assignment to ``b[0]``, we need to clear knowledge about ``a`` since
it has the same type (``uint[]``) and data location (memory). We also need to
clear knowledge about ``c``, since its base type is also a ``uint[]`` located
in memory. This implies that some ``c[i]`` could refer to the same data as
``b`` or ``a``.
Notice that we do not clear knowledge about ``array`` and ``d`` because they
are located in storage, even though they also have type ``uint[]``. However,
if ``d`` was assigned, we would need to clear knowledge about ``array`` and
vice-versa.
Real World Assumptions
======================
Some scenarios can be expressed in Solidity and the EVM, but are expected to
never occur in practice.
One of such cases is the length of a dynamic storage array overflowing during a
push: If the ``push`` operation is applied to an array of length 2^256 - 1, its
length silently overflows.
However, this is unlikely to happen in practice, since the operations required
to grow the array to that point would take billions of years to execute.