Verification (WIP)

Owned by sterzi
Last updated: Jul 31, 2019
2 min read

This page is for adding research, methods and frameworks for Smart Contracts Verification.

1.

Ethereum is a framework for cryptocurrencies which uses blockchain technology to provide an open global computing platform, called the Ethereum Virtual Machine (EVM). EVM executes bytecode on a simple stack machine. Programmers do not usually write EVM code; instead, they can program in a JavaScript-like language, called Solidity, that compiles to bytecode. Since the main purpose of EVM is to execute smart contracts that manage and transfer digital assets (called Ether ), security is of paramount importance. However, writing secure smart contracts can be extremely difficult: due to the openness of Ethereum, both programs and pseudonymous users can call into the public methods of other programs, leading to potentially dangerous compositions of trusted and untrusted code. This risk was recently illustrated by an attack on TheDAO contract that exploited subtle details of the EVM semantics to transfer
roughly $50M worth of Ether into the control of an attacker. In this paper, we outline a framework to analyze and verify both the runtime safety and the functional correctness of Ethereum contracts by translation to F# , a functional programming language aimed at program verification. [1]

Ref1: Formal Verification of Smart Contracts - http://delivery.acm.org/10.1145/3000000/2993611/p91-bhargavan.pdf?ip=79.103.143.114&id=2993611&acc=OA&key=4D4702B0C3E38B35%2E4D4702B0C3E38B35%2E4D4702B0C3E38B35%2EB7370FA72C089961&__acm__=1560061804_eacbf9bf1eef5530d0b182afd9b0a89a 


2. ZEUS verification for Hyperledger Fabric and Ethereum Smart Contracts

abstract—A smart contract is hard to patch for bugs once it is deployed, irrespective of the money it holds. A recent bug caused losses worth around $50 million of cryptocurrency. We present ZEUS—a framework to verify the correctness and validate the fairness of smart contracts. We consider correctness as adherence to safe programming practices, while fairness is adherence to agreed upon higher-level business logic. ZEUSleverages both abstract interpretation and symbolic model checking, along with the power of constrained horn clauses to quickly verify contracts for safety. We have built a prototype of ZEUSfor Ethereumand Fabric blockchain platforms and evaluated it with over22.4K smart contracts. Our evaluation indicates that about 94.6%of contracts (containing cryptocurrency worth more than $0.5billion) are vulnerable. ZEUSis sound with zero false negatives and has a low false-positive rate, with an order of magnitude improvement in analysis time as compared to prior art.

Ref1: ZEUS: Analyzing Safety of Smart Contracts - http://pages.cpsc.ucalgary.ca/~joel.reardon/blockchain/readings/ndss2018_09-1_Kalra_paper.pdf