Oyente

This is our next official release of Oyente since our OneNorth release. There are some improvements and new features in this new release as the following:
- Any security bugs that are detected are now mapped correctly to the source code
- Some issues from the previous release (solver not working correctly in some circumstances, some opcodes were not implemented correctly) are now fixed
- Users can now work with multiple contracts concurrently in a single file, or import other files
- False positive cases on assertion failures have been resolved
- Additional EVM code coverage, now Oyente will tell you how many instructions are covered after the analysis.
- Additional cases are now considered as vulnerable to the callstack attack
- Greatly improved UI for the web

Hello!

Its been awhile since our KentRidge release, here are some fresh updates in this new Oyente release ([what is Oyente?](https://medium.com/melonport-blog/oyente-beta-release-announcement-dd573cac1dff)).

What's in this release:

- Allowing checking assertion of any kind in Solidity (thanks to leonardoalt for his awesome PR 144). Now you can check if the assertion of any invalid condition in your smart contract is reachable with Oyente, thus preventing potential bugs! For example, one can simply check if

assert (postSendBalance + postRecBalance != preSendBalance + preRecBalance)

is reachable in their `transfer` function to guarantee that the transfer works correctly. This is a powerful feature and will be discussed more on our future blog post.

- Easy install via `pip` (thanks to beaugunderson and his PR 137 )
- Optimizing reentrancy detection function (thanks to luongnt95 and his PR 153)
- Many other optimizations here and there, including improving documentation and fixing reported bugs, done by luongnt95.

Get the new version

Now you can simply do:


$ pip install oyente

or compile from source by following the instructions in our README.

We thank the community for sending PRs, report issues to make Oyente better. The road to Changi, our stable release, is getting closer.

Cheers!

-- The Oyente Team

This is our first official release of Oyente. Since the time of publication of the paper, the following was improved
- more robust handling of different EVM opcodes with support of new opcodes like
- unit tests
- support newer versions of evm, solc and z3
- more options for constraining symbolic execution such as LOOP_LIMIT and DEPTH_LIMIT
- take in environmental information as input and work with external blockchains to speed up the symbolic execution
- better formatting, logging and documentation
- web interface for analyzing contracts