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-fmFormal 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-contractsYou 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-32c849aedaefArchitecture Overview:
https://habrastorage.org/webt/jo/mj/5_/jomj5_tltmq3td9_r-xhyavhhqq.pngYou can use Hyperbox on
http://2.59.42.98/hyperbox/It is free and open-source tool:
http://github.com/scp1001/hyperboxVersion 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).
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.
