[FREE] Formal verification tool. Mathematically-proven 100% safe smart-contracts

hjort

newbie

Activity: 1

Merit: 0

Very cool that you wrote this tool! Can't wait to have a closer look at it!

Just to qualify some claims (for other people reading this thread): It's a bit strong to say that only 30-40 companies use formal methods, in part because it is slightly hard to pin down exactly what formal methods are, and there are a lot of companies working with some forms of formal verification. In addition, there are many, many projects in academia which focus on formal verification, but I don't know to what extent these are put to use in industry. I found this to be a good overview, albeit slightly opinionated: http://www.imm.dtu.dk/~dibj/2014/tokyo/tokyo-p.pdf

Also, deciding exactly which contracts are formally verified is not always clear-cut. Most often you verify some properties. Deciding what properties are important is still a human decision. It's hard to say a program will always function correctly because you need to have an exact idea of what "correct" is, which is non-trivial for complex software.

scp1001

newbie

Activity: 3

Merit: 1

This publication going viral

scp1001

newbie

Activity: 3

Merit: 1

Formal Verification is the most powerful security conception in the world, there are only 2 Blockchains which already use it: Ethereum and Ziliqa.
This is not an absolute solution, but the nearest to 100% safety.

Outside of blockchain, just 30-40 companies use formal methods: for example, NASA, DARPA, Airbus, IBM, Apple.
https://github.com/ligurio/practical-fm

Formal Verification allows to find all vulnerabilities in any smart-contract, or get the formal proof that contract is absolutely safe.
There are only 9 formally-verifified contracts in the world for now:

2019-02-27 GnosisSafe contract
2018-10-12 Uniswap contract
2018-07-12 Ethereum Casper FFG contract
2018-03-12 DappSys DSToken ERC20 token contract
2018-02-28 Bihu KEY token operation contracts
2018-01-30 MyKidsEducationToken ERC20 token contract
2018-01-26 OpenZeppelin ERC20 token contract
2018-01-16 HackerGold (HKG) ERC20 token contract
2017-12-23 Philip Daian's Vyper ERC20 token contract
https://github.com/runtimeverification/verified-smart-contracts

You can see more information about formal verification on reddit, with some comments of Vitalik Buterin, who is a huge proponent of those ideas.
It is unbiased discussion, where you can see advantanges and criticism of formal verification both.
https://www.reddit.com/r/ethereum/comments/7bdm1g/so_can_we_again_have_a_talk_about_formal/

I decided to start creating of such tools for another blockchains.
Waves matches perfectly: they have turing-uncomplete smart-contracts with limited complexity.
I called this tool Hyperbox, because it can process wide range of input and output values for smart contract in one launch,
instead of a single set in normal contract execution.

Hyperbox is a symbolic execution virtual machine for Waves RIDE smart-contracts, based on php, python and Z3Prover.
It mainly intended for formal verification and allows to find all existing vulnerabilities.
Hyperbox implements modern and powerful fully automatic multi-transactional search. For example, multi-transactional analysis support appeared in Mythril just recently:
https://medium.com/consensys-diligence/the-tech-behind-mythx-smart-contract-security-analysis-32c849aedaef

Architecture Overview:
https://habrastorage.org/webt/jo/mj/5_/jomj5_tltmq3td9_r-xhyavhhqq.png

You can use Hyperbox on http://2.59.42.98/hyperbox/
It is free and open-source tool: http://github.com/scp1001/hyperbox
Version is 0.1, so syntax is very limited. It is just very early prototype, which was created during one hard week.

You can automatically solve predefinded crossing-river puzzle, or solve this smart-contract a bit lower as easy example (requires just 2 transaction).

Code:

let contract = tx.sender
let a= extract(getInteger(contract,"a"))
let b= extract(getInteger(contract,"b"))
let c= extract(getInteger(contract,"c"))
let d= extract(getInteger(contract,"d"))

match tx {
case t:DataTransaction =>
let na= extract(getInteger(t.data,"a")) 
let nb= extract(getInteger(t.data,"b"))
let nc= extract(getInteger(t.data,"c"))
let nd= extract(getInteger(t.data,"d"))
   
   nd == 0 || a == 100 - 5
case s:TransferTransaction =>
   ( a + b - c ) * d == 12

case _ => true

}

Also you can write and solve your own contracts using hyperbox.
Regular virtual machine is just a special case of symbolic VM, like cube is a special case of tesseract with 1 zero dimension. So Hyperbox can also be used as IDE for development and testing.

Topic: [FREE] Formal verification tool. Mathematically-proven 100% safe smart-contracts (Read 211 times)