Melonport AG in partnership with the Oyente development team today announced the first beta release of Oyente, an ope-source analysis and formal verification tool for Ethereum smart contracts. Oyente can be used for any Ethereum smart contracting language (Solidity, Serpent, LLL, etc.), and its current iteration also has many features specifically geared towards Melon protocol module developers.
Reto Trinkler, CTO and Chairman of Melonport stated:
“We are very pleased to see the development efforts of Oyente come to fruition. We believe analyzing disassembled opcodes from bytecode deployed to the blockchain and checking them against a set of properties is one of the most cost and time-effective ways to reason about smart contract security to date. For the Melon protocol, this translates to a great open-source tool to help ensure quality and security standards in Melon modules.”
Explaining more about the product, Oyente project’s Lead Developer Loi Luu said:
“I am very happy to see the results of our academic efforts getting used in practice to bring value to the Ethereum community. Oyente can be used to detect many common bugs found in smart contacts like reentrancy, transaction ordering dependence and so on. What’s more interesting is that Oyente’s design is modularized, so this allows advanced users to implement and plug in their own detection logic to check self-defined properties in their contracts. I look forward to seeing more contributions from the community to make Oyente even more powerful and useful.”
The Oyente project started as an academic paper released by the National University of Singapore Ph.D. student Luu and a group of his peers. After an initial open source release of Oyente covering 80% of EVM opcodes, funding unfortunately depleted, and the maintenance of the Oyente project was put on hold.
Following Melonport’s 2.5million CHF raise during a contribution period in February 2017, the Melonport team identified the potential of Oyente to greatly augment the Ethereum developer community’s ability to create safe and secure decentralized applications.
Specifically, the Melon protocol module ecosystem’s security and standardization can be greatly improved by the usage of the tool. After an additional six months of hard work by the Oyente and Melonport developer teams, Oyente now covers 100% of EVM opcodes and had a plethora of other useful tools in the works such as ERC20 support.
Mona El Isa, CEO of Melonport said:
“While formal verification is not a magical bullet for smart contract security, we’re very proud to be able to fund and share this open source symbolic execution tool with both our own module developers and the Ethereum community as a whole.”
Following this new release of Oyente, the developer team intends to continue adding new features to the tool, which may include functionality for the analysis of ERC20 and token contracts. For example, the team aims to detect if some function accidentally prints more tokens than expected in an ERC20 contract due to imprecise coding logic.