Bitcoin Forum
July 02, 2024, 07:46:31 PM *
News: Latest Bitcoin Core release: 27.0 [Torrent]
 
   Home   Help Search Login Register More  
Pages: [1]
  Print  
Author Topic: [FREE] Formal verification tool. Mathematically-proven 100% safe smart-contracts  (Read 188 times)
scp1001 (OP)
Newbie
*
Offline Offline

Activity: 3
Merit: 1


View Profile
May 04, 2019, 08:48:58 PM
Last edit: May 05, 2019, 06:46:51 AM by scp1001
 #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.
scp1001 (OP)
Newbie
*
Offline Offline

Activity: 3
Merit: 1


View Profile
May 05, 2019, 07:40:38 PM
Last edit: May 06, 2019, 12:45:01 AM by scp1001
 #2

This publication going viral  Smiley
Reposts on twitter:

https://twitter.com/globalwork365 (42k followers)
https://twitter.com/Megacoin_Fan (14k followers)
https://twitter.com/wavesfullnode (3k followers)
https://twitter.com/Ballooonknots (2k followers)
https://twitter.com/jayeshmthakur (1k followers)
https://twitter.com/piggy135764 (900 followers)
https://twitter.com/cryptotechie (415 followers)
https://twitter.com/RFipple (180 followers)
https://twitter.com/Robert87980191 (133 followers)
https://twitter.com/kumalic007 (64 followers)
https://twitter.com/wishlist7 (46 followers)
https://twitter.com/BirdflyAlex (30 followers)
https://twitter.com/Laurentius261 (23 followers)
https://twitter.com/scp10012 (my twitter)
hjort
Newbie
*
Offline Offline

Activity: 1
Merit: 0


View Profile
May 06, 2019, 10:56:18 AM
 #3

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.
Pages: [1]
  Print  
 
Jump to:  

Powered by MySQL Powered by PHP Powered by SMF 1.1.19 | SMF © 2006-2009, Simple Machines Valid XHTML 1.0! Valid CSS!