Skip to main content

Browse the archive

https://gitlab.com/nomadic-labs/mi-cho-coq
08 June 2021, 12:39:06 UTC
Revision 16eec8a79400c3b5987e733fd4b440d212fee5e7 authored by Raphaël Cauderlier on 06 February 2021, 22:05:50 UTC, committed by Arvid Jakobsson on 02 March 2021, 18:13:44 UTC 
Dexter DFS compat: assert that `to` and `owner` args are always implicit accounts
 
In order to reduce the attack surface of Dexter in the presence of
both BFS and DFS calls, we add assertions that guarantee that:

- Dexter is not called by a smart-contract so no BFS operations can be
injected before the operations emitted by Dexter. This is checked
by (SOURCE = SENDER) which can never hold in internal transactions.

- uncontrolled addresses (the `to` and `owner` parameters) are
prevented to do any call (DFS or BFS) by requesting them to be
implicit accounts. There is unfortunately no instruction in Michelson
to check that an address is implicit (see
https://gitlab.com/nomadic-labs/tezos/-/merge_requests/93) but we know
that the transaction source is always implicit (since Babylon) so we
use the over approximation (to = SOURCE) and (owner = SOURCE).
1 parent 027833e
History
Tip revision: 16eec8a79400c3b5987e733fd4b440d212fee5e7 authored by Raphaël Cauderlier on 06 February 2021, 22:05:50 UTC
Dexter DFS compat: assert that `to` and `owner` args are always implicit accounts
Tip revision: 16eec8a
File Mode Size
doc
scripts
src
.gitignore -rw-r--r-- 336 bytes
.gitlab-ci.yml -rw-r--r-- 920 bytes
LICENSE -rw-r--r-- 1.1 KB
Makefile.local -rw-r--r-- 379 bytes
README.org -rw-r--r-- 8.5 KB
_CoqProject -rw-r--r-- 4 bytes
configure -rwxr-xr-x 1.6 KB
coq-mi-cho-coq.install -rw-r--r-- 73 bytes
coq-mi-cho-coq.opam -rw-r--r-- 1.4 KB

README.org

back to top