Woke - testing framework for Ethereum

Username

kevin.kanak@ackeeblockchain.com

Grant Description

Woke is a static analyzer and symbolic execution engine for Solidity written in Python.

Our vision is that Woke will become the standard for static analysis of Solidity smart contracts and will be actively used by the developer community.

Woke also includes extensions to integrated development environments (IDEs) such as VS Code, Atom and others. Our goal is to bring Woke's functionalities directly into IDEs and thus reach the Ethereum developer community and participate in greater security on the blockchain

We have assembled a team that will be dedicated full-time to the development of Woke. The project is currently under active development and we have already started working on the core functionalities.

Woke Github: https://github.com/Ackee-Blockchain/woke Woke 1-pager: https://docs.google.com/presentation/d/e/2PACX-1vSYU_C1Q1utljejLwx7Rnk43Q0baWfWymIGxAHFu-wadJMbxkzggQSlAWhJnYRFsmtGr77k9W95pkCQ/pub?start=true&loop=false&delayms=60000

Overview

Woke is a static analyzer and symbolic execution engine for Solidity written in Python.

Our vision is that Woke will become the standard for static analysis of Solidity smart contracts and will be actively used by the developer community.

Woke also includes extensions to integrated development environments (IDEs) such as VS Code, Atom and others. Our goal is to bring Woke's functionalities directly into IDEs and thus reach the Ethereum developer community and participate in greater security on the blockchain

We have assembled a team that will be dedicated full-time to the development of Woke. The project is currently under active development and we have already started working on the core functionalities.

Woke Github: https://github.com/Ackee-Blockchain/woke Woke 1-pager: https://docs.google.com/presentation/d/e/2PACX-1vSYU_C1Q1utljejLwx7Rnk43Q0baWfWymIGxAHFu-wadJMbxkzggQSlAWhJnYRFsmtGr77k9W95pkCQ/pub?start=true&loop=false&delayms=60000

Value to Synthetix

Existing static analysis tools on the market don't allow smart contract interactions and can't perform symbolic analysis. Some vulnerabilities may go undetected when performing only static analysis and these vulnerabilities can lead to security risks, which is why we added Solidity symbolic execution engine to Woke. We also want to focus on re-entrancy and access control vulnerabilities along with algebraic type checking.

Another limiting factor in building on the Ethereum system is the lack of tools that allow for smooth Solidity development like we are used to from other programming languages. Auto-completion tends to be context-free, type checking is limited or non-existent, and more advanced features require a combination of several different tools.

The main goal of Woke is to address these issues and thus effectively help both developers and auditors.

Compared to existing tools, Woke has several advantages. We don't want Woke to only act as a black box that receives source code as input and outputs a list of found vulnerabilities and hints. Woke allows interaction with the smart contract via the Woke API, so for example developers and auditors can symbolically execute a given function with given arguments. Of course, it is also possible to implement custom vulnerability detectors.

Another difference is that Woke implements the Language Server Protocol (LSP), through which IDE extensions communicate. So developers can benefit from advanced Solidity language support right in their IDE including features like "Find all usages", "Go to the definition" and of course context-aware auto-completion. Also, Woke informs developers while writing the code about found vulnerabilities

Sometimes the code in Solidity can be complicated and cannot be analyzed correctly automatically. We try to keep this in mind as well, and in addition to project-specific config files, we also implement annotation functionality in Solidity code. The developers can write special comments in Solidity code that affect the analysis of Woke.They can be used to check data types more strictly or to hint at some missing information.

Project Implementation Plan

Woke's roadmap

Q2/22 First public release including: Woke console Basic symbolic execution First package of vulnerability detectors VS Code extension Q4/22 Advanced symbolic execution More IDE extensions

Additional Information

At Ackee Blockchain we believe that security on the blockchain is one of the most important aspects for the functioning of the whole blockchain ecosystem and its adoption. That's why we decided to focus on auditing smart contracts and contributing to the Ethereum developer community by hosting a Summer School of Solidity, where we teach how to write code in Solidity and also how to review smart contracts written in Solidity. https://ackeeblockchain.com/summer-school-of-solidity

Our CEO Josef Gattermayer, Ph.D created blockchain course at Czech Technical University in Prague, where our team members teach blockchain technology and smart contract programming to students https://courses.fit.cvut.cz/NIE-BLO/ Our Ethereum Tech Lead Dominik Teiml gave a presentation at the Berlin Ethereum meetup about: Dutch Exchange, a decentralized exchange well suited for blockchain purpose by making us of the Dutch auction mechanism https://www.youtube.com/watch?v=fbSsrUmARRY

Dominik's open source contributions: Formal verification of GNO: https://github.com/runtimeverification/verified-smart-contracts/tree/master/erc20/gno Slither: https://github.com/crytic/slither/commits?author=hacker-DOM Solc-select: https://github.com/crytic/solc-select/commits?author=hacker-DOM Ethereum Yellow Paper: https://github.com/ethereum/yellowpaper/commits?author=hacker-DOM

List of some of Dominik's audits in which he was involved. Him and his colleagues from Trail of Bits found high severity issues in the Uniswap v3 protocol. https://github.com/trailofbits/publications/blob/master/reviews/UniswapV3Core.pdf https://github.com/trailofbits/publications/blob/master/reviews/Opyn-Gamma-Protocol.pdf https://github.com/trailofbits/publications/blob/master/reviews/wXTZ.pdf

Since we have a positive relationship with education, Dominik has uploaded some of his lectures on formal verification to youtube: https://www.youtube.com/watch?v=glVk8KtnstI , https://www.youtube.com/watch?v=psnZXNzixBU

Funding Request

When it comes to grant funding, it would be most helpful for us in the immediate future. We want to allocate $500k to cover the development of Woke for 18 months.

We will cover the most from profits from auditing but we are looking for co-investing.

Grant $20k from the Synthetix would cover 3 months of Woke development and this is what we ask for. According to our roadmap, we will have: Woke console, basic symbolic execution, first package of vulnerability detectors, and VS Code extension

If Synthetix's grant couldn’t cover the whole Woke development, it would be nice to connect us to other possible partners and other funding sources