Revision 936d209e8ce8cce3fd0b0e96692afc2c5730d094 authored by Raphaël Cauderlier on 06 February 2021, 22:41:46 UTC, committed by Raphaël Cauderlier on 07 February 2021, 17:37:21 UTC
There are 3 cases where Dexter emits more than an operation at once. In two of them, a potential attacker is called first. If this attacker can produce DFS calls it may be able to access Dextex before the FA1.2 is updated so some invariants might be broken. We haven't managed to use DFS calls to attack Dexter but always calling uncontrolled contracts last in the operation list is always safer.
1 parent 55e0921
coq-mi-cho-coq.opam
version: "dev"
opam-version: "2.0"
synopsis: "A specification of Michelson in Coq to prove properties about smart contracts in Tezos"
maintainer: "raphael.cauderlier@nomadic-labs.com"
authors: [ "Raphaël Cauderlier" "Bruno Bernardo" "Julien Tesson" "Arvid Jakobsson" ]
homepage: "https://gitlab.com/nomadic-labs/mi-cho-coq/"
dev-repo: "git+https://gitlab.com/nomadic-labs/mi-cho-coq/"
bug-reports: "https://gitlab.com/nomadic-labs/mi-cho-coq/issues"
license: "MIT"
build: [
["./configure"]
[make "-j%{jobs}%"]
]
install: [
make "install"
]
depends: [
"coq-list-string"
"coq-menhirlib" {>= "20190626"}
"coq-moment" {>= "1.2.0"}
"coq-ott" {>= "0.29"}
"coq" {>= "8.8"}
"menhir"
"ocaml" {>= "4.07.1"}
"ocamlbuild"
"ott" {build & >= "0.29"}
"zarith"
]
build-test: [ make "test" ]
description: """
Michelson is a language for writing smart contracts on the Tezos blockchain.
This package provides a Coq encoding of the syntax and semantics of Michelson,
automatically generated by the Ott tool. Also included is a framework called Mi-Cho-Coq
for reasoning about Michelson programs in Coq using a weakest precondition calculus."""
tags: [
"category:Programming Languages/Formal Definitions and Theory"
"keyword:cryptocurrency"
"keyword:michelson"
"keyword:semantics"
"keyword:smart-contract"
"keyword:tezos"
"logpath:Michocoq"
"logpath:Michocott"
]
Computing file changes ...
