mirror of
https://github.com/digital-asset/daml.git
synced 2024-09-20 09:17:43 +03:00
255 lines
10 KiB
ReStructuredText
255 lines
10 KiB
ReStructuredText
|
.. Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
|
||
|
.. SPDX-License-Identifier: Apache-2.0
|
||
|
|
||
|
DAML Verification Tool
|
||
|
======================
|
||
|
|
||
|
This project performs fully automated formal verification of DAML code.
|
||
|
Provided with a choice of a template and a field of a (potentially different) template, the verification tool employs symbolic
|
||
|
execution and an SMT solver, to verify whether the given choice always preserves
|
||
|
the total amount of the given field. This allows it to automatically answer
|
||
|
the common question "Could this smart contract model ever burn money or create
|
||
|
money out of thin air?"
|
||
|
|
||
|
Installation
|
||
|
============
|
||
|
|
||
|
- Install the `DAML development dependecies`_.
|
||
|
|
||
|
- Install the `Z3 SMT solver`_.
|
||
|
Note that on Linux, you can alternatively install Z3 using
|
||
|
``sudo apt install z3``.
|
||
|
|
||
|
.. _DAML development dependecies: https://github.com/digital-asset/daml/
|
||
|
.. _Z3 SMT solver: https://github.com/Z3Prover/z3
|
||
|
|
||
|
Running the Verification Tool
|
||
|
=============================
|
||
|
|
||
|
At the moment, the verification tool is launched from a command line interface.
|
||
|
Execute the tool by passing in the DAR file, the choice to be
|
||
|
verified (``--choice`` / ``-c``), and the field which should be preserved (``--field`` / ``-f``):
|
||
|
|
||
|
.. code-block::
|
||
|
> bazel run //compiler/daml-lf-verify:daml-lf-verify -- file.dar --choice Module:Template.Choice --field Module:Template.Field
|
||
|
|
||
|
Examples
|
||
|
========
|
||
|
|
||
|
Example 1: Transferring value
|
||
|
-----------------------------
|
||
|
|
||
|
As a first example, consider a simple ``Account`` template, with a single choice
|
||
|
``Account_Transfer`` for transfering from one account to another. Note that if
|
||
|
someone tries to transfer more than they own, the choice should just do nothing.
|
||
|
|
||
|
.. code-block:: daml
|
||
|
module Demo where
|
||
|
template Account
|
||
|
with
|
||
|
amount : Decimal
|
||
|
owner : Party
|
||
|
where
|
||
|
ensure amount > 0.0
|
||
|
|
||
|
signatory owner
|
||
|
|
||
|
controller owner can
|
||
|
|
||
|
-- | Transfer some amount to the receiver, or do nothing if this would make the
|
||
|
-- remaining amount in the account negative.
|
||
|
nonconsuming Account_Transfer : (ContractId Account, ContractId Account)
|
||
|
with
|
||
|
transferAmount: Decimal
|
||
|
receiverCid: ContractId Account
|
||
|
do
|
||
|
if amount >= transferAmount
|
||
|
then do
|
||
|
-- The account has sufficient funds.
|
||
|
receiver <- fetch receiverCid
|
||
|
newSelf <- create this with amount = amount - transferAmount
|
||
|
newReceiver <- create receiver with
|
||
|
amount = receiver.amount + transferAmount
|
||
|
archive receiverCid
|
||
|
return (newSelf, newReceiver)
|
||
|
else do
|
||
|
-- The account does not have sufficient funds, and the transfer is
|
||
|
-- cancelled.
|
||
|
return (self, receiverCid)
|
||
|
|
||
|
It is clear that making a transfer between two accounts, should always preserve
|
||
|
the total amount of funds. However, running the verification tool produces the
|
||
|
following output:
|
||
|
|
||
|
.. code-block::
|
||
|
> bazel run //compiler/daml-lf-verify:daml-lf-verify -- demo.dar --choice Demo:Account.Account_Transfer --field Demo:Account.amount
|
||
|
|
||
|
...
|
||
|
|
||
|
==========
|
||
|
|
||
|
Main flow:
|
||
|
|
||
|
Create: [ if this_6.amount >= arg_5.transferAmount then this_6.amount - arg_5.transferAmount else 0 % 1
|
||
|
, if this_6.amount >= arg_5.transferAmount then receiver_9.amount + arg_5.transferAmount else 0 % 1 ]
|
||
|
Archive: [ if this_6.amount >= arg_5.transferAmount then receiver_9.amount else 0 % 1 ]
|
||
|
Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
~~~~~~~~~~
|
||
|
|
||
|
Fail. The choice Account_Transfer does not preserve the field amount. Counter example:
|
||
|
this_10.amount = (/ 1.0 2.0)
|
||
|
this_12.amount = 0.0
|
||
|
receiver_9.amount = (/ 1.0 4.0)
|
||
|
arg_5.transferAmount = (-
|
||
|
(/ 1.0 4.0))
|
||
|
this_6.amount = (/ 1.0 4.0)
|
||
|
|
||
|
==========
|
||
|
|
||
|
Done.
|
||
|
|
||
|
The ``Main flow`` describes all updates performed when exercising the
|
||
|
``Account_Transfer`` choice, without making any additional assumptions on the
|
||
|
inputs. It enumerates all create and archive updates, along with a number of
|
||
|
additional assertions (e.g. arising from the ``ensure`` statement in ``Account``).
|
||
|
|
||
|
The SMT solver figured out that the choice does not actually preserve the total
|
||
|
amount, and provides a handy counter example. In fact, it turns out that we're
|
||
|
creating more money than archiving. A closer look at the create and archive
|
||
|
updates clearly shows that we're never archiving ``this_6.amount``. And indeed,
|
||
|
we forgot to include ``archive self`` in the example. After
|
||
|
adding this line to the definition of ``Account_Transfer``, the new output is as
|
||
|
follows:
|
||
|
|
||
|
.. code-block::
|
||
|
> bazel run //compiler/daml-lf-verify:daml-lf-verify -- demo.dar --choice Demo:Account.Account_Transfer --field Demo:Account.amount
|
||
|
|
||
|
...
|
||
|
|
||
|
==========
|
||
|
|
||
|
Main flow:
|
||
|
|
||
|
Create: [ if this_6.amount >= arg_5.transferAmount then this_6.amount - arg_5.transferAmount else 0 % 1
|
||
|
, if this_6.amount >= arg_5.transferAmount then receiver_9.amount + arg_5.transferAmount else 0 % 1 ]
|
||
|
Archive: [ if this_6.amount >= arg_5.transferAmount then this_6.amount else 0 % 1
|
||
|
, if this_6.amount >= arg_5.transferAmount then receiver_9.amount else 0 % 1 ]
|
||
|
Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
~~~~~~~~~~
|
||
|
|
||
|
Success! The choice Account_Transfer preserves the field amount.
|
||
|
|
||
|
==========
|
||
|
|
||
|
Done.
|
||
|
|
||
|
Now the verification tool can prove that ``Account_Transfer`` does in fact
|
||
|
preserve the ``amount`` field.
|
||
|
|
||
|
Example 2: Recursion
|
||
|
--------------------
|
||
|
|
||
|
For a second example, consider the ``Account_Divide`` choice, which recursively
|
||
|
donates 1.0 amount from the donor to the receiver account, until the receiver
|
||
|
account has at least as much funds as the donor.
|
||
|
|
||
|
.. code-block:: daml
|
||
|
-- | Iteratively transfer 1.0 amount to the receiver, until it has at
|
||
|
-- least as much funds as the donor.
|
||
|
nonconsuming Account_Divide : (ContractId Account, ContractId Account)
|
||
|
with
|
||
|
receiverCid: ContractId Account
|
||
|
do
|
||
|
receiverAccount <- fetch receiverCid
|
||
|
if amount <= receiverAccount.amount
|
||
|
-- The receiver has at least as much funds as the donor.
|
||
|
then return (self, receiverCid)
|
||
|
-- The receiver does not yet have enough funds. Make a new transaction.
|
||
|
else do
|
||
|
(newSelf, newReceiver) <- exercise self Account_Transfer with
|
||
|
transferAmount = 1.0, receiverCid = receiverCid
|
||
|
exercise newSelf Account_Divide with receiverCid = newReceiver
|
||
|
|
||
|
We can again use the formal verification tool to ensure that ``Account_Divide``
|
||
|
always preserves the field ``amount``.
|
||
|
|
||
|
.. code-block::
|
||
|
> bazel run //compiler/daml-lf-verify:daml-lf-verify -- demo.dar --choice Demo:Account.Account_Divide --field Demo:Account.amount
|
||
|
|
||
|
...
|
||
|
|
||
|
==========
|
||
|
|
||
|
Main flow:
|
||
|
|
||
|
Create: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount - 1 % 1 else 0 % 1
|
||
|
, if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount + 1 % 1 else 0 % 1 ]
|
||
|
Archive: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount else 0 % 1
|
||
|
, if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount else 0 % 1 ]
|
||
|
Assert: this_18.amount > 0.0
|
||
|
Assert: receiverAccount_21.amount > 0.0
|
||
|
Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
~~~~~~~~~~
|
||
|
|
||
|
Success! The choice Account_Divide preserves the field amount.
|
||
|
|
||
|
==========
|
||
|
|
||
|
Recursion cycle:
|
||
|
|
||
|
Create: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount - 1 % 1 else 0 % 1
|
||
|
, if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount + 1 % 1 else 0 % 1 ]
|
||
|
Archive: [ if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then this_18.amount else 0 % 1
|
||
|
, if not this_18.amount <= receiverAccount_21.amount and this_18.amount >= 1 % 1 then receiver_9.amount else 0 % 1 ]
|
||
|
Assert: this_18.amount > 0.0
|
||
|
Assert: receiverAccount_21.amount > 0.0
|
||
|
Assert: (+ receiver_9.amount arg_5.transferAmount) = this_12.amount
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
Assert: (- this_6.amount arg_5.transferAmount) = this_10.amount
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: this_6.amount > 0.0
|
||
|
Assert: receiver_9.amount > 0.0
|
||
|
~~~~~~~~~~
|
||
|
|
||
|
Success! The choice Account_Divide preserves the field amount.
|
||
|
|
||
|
==========
|
||
|
|
||
|
Done.
|
||
|
|
||
|
Note that besides the ``Main flow`` verification, the tool also isolates any
|
||
|
(mutual) recursion cycles within the choice. In this scenario, ``Account_Divide``
|
||
|
has one recursion cycle, shown under ``Recursion cycle``. In order for a field
|
||
|
to be preserved, the choice has to always terminate, and every cycle has to
|
||
|
preserve the given field.
|
||
|
|
||
|
Testing Framework
|
||
|
=================
|
||
|
|
||
|
A testing framework is provided for working on the verification tool. Run the
|
||
|
tests as follows:
|
||
|
|
||
|
.. code-block::
|
||
|
> bazel run //compiler/daml-lf-verify:verify-tests
|
||
|
...
|
||
|
All 23 tests passed (9.44s)
|