Blog

Tags | Categories

Finding Real-World Bugs in Smart Contract Interactions with Property-Based Testing (Mon, Dec 14, 2020) By Mikkel Milo et al.

Recently, Nomadic Labs made a blog post detailing their work on formally verifying the Dexter smart contract, a contract that provides decentralized exchange of digital assets. They verified functional properties of the contract using Mi-Cho-Coq, a Coq framework for proving properties about Michelson contracts in Tezos. A key limitation of Mi-Cho-Coq is that it does not allow for proving properties about contract-to-contract communications (also referred to as inter-contract communications, or just contract interactions).

Read more
Commuting Quantifiers (Tue, Oct 6, 2020) By Amin Timany
Category : Technical

When does the universal quantifier commute with the existential quantifier? That is, when does $\forall x \in A. \exists y \in B. P(x, y)$ imply $\exists y \in B. \forall x \in A. P(x, y)$? Obviously, this is not always the case. There are many counter examples — every house in Aarhus has an owner but there is no person that owns all houses in Aarhus. Here, we will see two criteria where the universal quantifier commutes with the existential quantifier.

Read more
Preventing an $8M attack on Ethereum's bZx deFI platform with property-based testing (Fri, Aug 7, 2020) By Mikkel Milo et al.

On September 12, the bZx decentralized finance (deFI) platform suffered from an attack where the attacker was able to obtain control over $8 million worth of cryptocurrency. The fault was due a single misplaced line in their iToken smart contract’s transferFrom method, allowing an attacker to duplicate their tokens, consequently allowing them to increase their token balance arbitrarily. The bug remained hidden, though, during an extensive 19 person-week auditing by two security companies, Peckshield and CertiK.

Read more
Value Restriction (Mon, Aug 12, 2019) By Amin Timany
Category : Technical
Tag : PL basics

There is a problem with mixing impredicative polymorphism, i.e., polymorphism in System F, and side effects, e.g., references, continuations, etc. This problem arises when we allow arbitrary computations to considered polymorphic. The solution usually used is to restrict the programming language so that only values are allowed to be abstracted as polymorphic programs. Here we discuss this issue and its solution which is usually referred to as “Value Restriction”.

Read more