Formal Verification of Ethereum Smart Contracts

New automated security verifier for Ethereum has been released
07 July 2017   846
Blockchain

Distributed database that is used to maintain a continuously growing list of records, called blocks

Switzerland based Software Reliability Lab developing automated analysis and synthesis techniques for smart contracts has launched the first automated system for formal verification of smart contracts - Securify.

Securify verifier for Ethereum Securify verifier for Ethereum

The main advantages of Securify over other solutions is that it provides:

  • Automation, to enable all users to verify contracts
  • Guarantees, to avoid reporting vulnerable contracts are safe
  • Extensibility, to capture new security vulnerability that are regularly discovered

Securify is capable to pinpoint the instructions that may cause security issues and therefore provides practical and useful guidelines to contract developers.

Ethereum

Is an open-source blockchain-based distributed computing platform featuring smart contract functionality, which facilitates online contractual agreements 

As the developers argue, existing solutions based on executing the contract "check only a subset of the possible paths and can therefore miss critical security problems. Further, approaches based on interactive-theorem provers can provide strong guarantees, for all paths, but they cannot be easily automated or easily extended. In contrast, Securify combines the best of both worlds: it analyzes all paths while being fully automated".

Securify verifier for Ethereum in working process  Securify verifier in working process 

The brand new verifier has already received positive feedback in social media. Sergio Demian Lerner, cryptocurrency security consultant from the first open-source smart contract platform RSK, shared on Twitter:

Pilot customer access to Securify has been already offered to users. It's also possible to sign up for the full release of Securify and future updates

Wyoming Passed Bill Exempting Utility Tokens from Securities Laws

The Wyoming House of Representatives has unanimously approved a bill exempting utility tokens from securities laws  
20 February 2018   71

On Monday, House Bill (HB) 70 passed the House 60 to 0 and will now head to the Senate. The bill exempts utility tokens from securities laws. This will attracts ICO’s launches to the state and will make the state a favorable environment for blockchain startups.

According to the bill, the utility token must meet three conditions:

  1. The token’s issuer must not market it as an investment;

  2. The token must be exchangeable for goods and services, for example, startups must have a working product or service at the time the tokens are issued;

  3. The token’s issuer must not actively make efforts to create a secondary market for the token by entering into a repurchase agreement or agreeing to locate buyers for the token.

It is important to note that there are four more cryptocurrency and blockchain-related bills currently moving through the Wyoming legislature.

HB 19 passed the House of Representatives on Monday and is now awaiting introduction in the Senate. The bill exempts cryptocurrency from the state’s money transmitter act.

HB 101 has passed its second reading in the House and, if it passes its final hearing, will then go to the Senate. This bill will allow companies to create and use blockchains for the purpose of storing records and conducting inter-office communication.

HB 126 has just passed its second reading in the House. It will allow the creation of series LLCs.

Senate File (SF) 111 passed a vote to introduce on Friday and is now headed to a committee hearing. This bill will exempt cryptocurrency assets from state property taxes.