Would Facebook bring dawn to smart contracts?

Move Programming Language — Technical Paper

Author: Yu Guo, Founder of SECBIT Labs.

Everyone must have been bombarded by Facebook news recently.

Libra, the cryptocurrency project started by Facebook, got published officially on June 18th along with its website and whitepaper offering global currency & financial service to billions of people.

Also, it has several technical whitepapers to explain the new programming language ‘Move’ and consensus protocol — LibraBFT. Its source code has been published on GitHub, and the test network has gone online.

Libra is designed as a permissioned blockchain as the developing team states that no mature solution in the permissionless (public) blockchain is…

Photo by gustavo centurion on Unsplash

Abstract: The failure of Fomo3D and its followers is highly related to bugs in their smart contract design. Here we offer a detailed analysis of two problems in Fomo3D-like games from the view of security, along with several practical solutions for your reference. We welcome anyone interested to join our community for further discussion.

The Falling of Fomo3D-like Games Caused By Hacking

Fomo3D has already entered the third round. According to data on 2:00 GMT, Oct 9th, the pool only drew 103.4482 ethers. The total amount is less than 800 ethers plus 680 ethers from the last round, which is a great recession compared to prior rounds.


Photo by Tom Roberts on Unsplash

The first round of Fomo3D has ended and the winner’s address is 0xa169, with a prize of 10,469.66 ethers.

You may think that the winner is just an ordinary participant.

SECBIT Labs first found that the Fomo3D winner played a special attack trick to sharply decrease the number of transactions packed by miners near the end of the game (multiple blocks were involved), accelerating the approach of the game end and increasing the winning probability. SECBIT Labs also observed several similar abnormal blocks and transactions regarding to the last round of Last Winner.

A Series of Abnormal Blocks and Transactions

Photo by Roman Mager on Unsplash

Vulnerabilities in smart contracts are threatening blockchain projects, developers and investors for a long time. A growing number of security teams are putting efforts in this field with various approaches to secure contracts. SECBIT Labs proposes combining the formal proofs with the traditional test and security audit. In this article, we take the ERC20 formal proof in our GitHub repository tokenlibs-with-proofs as an example to show the use of formal proofs on smart contracts. We hope the formal proofs can help to eliminate buggy contracts, and secure all aspects of smart contracts including design logic, implementation, economic system, etc.

What is Formal Proof


an Analysis of ATN Token’s CUSTOM_CALL Bug

Photo by Michał Parzuchowski on Unsplash

On June 20th, 2018, AI Technology Network (ATN) reported an attack on ATN smart contract: an hacker set his address as owner via a bug in ATN Token contracts and issued 11 million ATN tokens for himself on May 11th, 2018. ATN team located the bug, discovered the hacking method and upgraded the contract in no time [1]. The hacker made use of passing custom fallback functions in ERC223 contracts along with ds-auth approving check, then called the function of this contract when ERC223 contract invoked this CUSTOM_CALL.

Afterwards, '隐形人真忙' of Baidu Security also shared experience of 'call injection attack…


Research on smart contract security, smart contract formal verification, crypto-protocols, compilation, contract analysis, game theory and crypto-economics.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store