RK87 is a symbolic platform for Solidity smart contracts. User can add assertions and assumptions
into existing Solidity code base to let symbolic engine search for counterexamples or get verified.
RK87 is the only platform that allow user to do symbolic verifier using only Solidity language and some small support directives.
How it works?
RK87 first compiles Solidity source code into symbolic represents, and then Z3 symbolic execution engine will be used to perform analysis. Additional directives can be added to support declarations and verifications.
Please refer to RK87 Documentation for examples and to learn more about all supported directives.
Smart Contracts Massive Hunting for Vulnerabilities
Our paper, Smart Contracts Massive Hunting for Vulnerabilities, at JD-HITB Security Conference Beijing 2018 shows a new approach to finding security bugs in smart contracts using symbolic execution that is not pattern-based. Early results are promising: the tool managed to accurately detect most smart contract security bugs reported in 2018 and has helped us find many unpublished ones. Read more
Monocerus: Dynamic Analysis for Smart Contract
Nguyen Anh Quynh, Monocerus: Dynamic Analysis for Smart Contract, BlackHat Asia 2019. Read more
Detect Abnormal Behaviours in Ethereum Smart Contracts Using Attack Vectors
Blockchain has gradually been popularized by its transparency, fairness, and democracy. This technology has opened the door to the development of Ethereum, a blockchain platform with smart contracts that can hold and automatically transfer tokens. Like a legacy computer program, smart contracts are vulnerable to security bugs. In recent years, many successful attacks on Ethereum network have been recorded, cost victims millions of dollars. In this paper, we classify attack vectors of Ethereum smart contracts, then propose some behaviour-based methods to detect them. To realize the ideas, we implement Abbe, a tool that can not only discover known attacks but also detect zero-day vulnerabilities. Read more