git clone
https://github.com/ConsenSys/mythril-classic.git
cd mythril-classic
docker build -t myth .
COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin
docker run -v $(pwd):/tmp \
-w /tmp myth:latest \
-v4 \
--verbose-report \
-x contracts/flattened.sol
docker run -v $(pwd):/tmp \
-w /tmp myth:latest \
--solc-args="--allow-paths
/tmp/node_modules/zeppelin-solidity/
zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \
-v4 \
--verbose-report \
-x contracts/Booking.sol
docker run -v $(pwd):/tmp -w /tmp myth:latest -x
contracts/flattened.sol:Booking -v4 --verbose-report
mythril.laser.ethereum.svm [WARNING]:
No contract was created during the execution of contract creation
Increase the resources for creation execution (--max-depth or --create-timeout)
The analysis was completed successfully. No issues were detected.
1. Define the set of input variables. They will serve as symbolic variables, all other
variables will be treated as concrete values.
2. These variables and each operation which may affect a symbolic variable value
should be logged to a trace file, as well as path conditions or any error that occurs.
3. Choose an set of input variables to begin with.
4. Execute the native contract code and save the trace file.
5. Symbolically re-execute the program on the trace, generating a set of symbolic
constraints (including path conditions)for future analysis.
6. Exclude the last path condition from the “already analyzed” ones to analyze
a new execution path next time. If there is no such path condition, the algorithm
terminates.
7. Analyze the path condition: generate a new input for all path conditions to fix them.
If there is no such input, return to step 6 and try the next execution path.
8. Go to step 4.
The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available,
the program counter pc ∈ P256, the memory contents, the active number of words in memory
(counting continuously from position 0), and the stack contents.
The memory contents μm are a series of zeroes of size 256.
function Booking(
string _description,
string _fileUrl,
bytes32 _fileHash,
uint256 _price,
uint256 _cancellationFee,
uint256 _rentDateStart,
uint256 _rentDateEnd,
uint256 _noCancelPeriod,
uint256 _acceptObjectPeriod
) public payable {
require(_price > 0);
require(_price > _cancellationFee);
require(_rentDateStart > getCurrentTime());
require(_rentDateEnd > _rentDateStart);
require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd);
require(_rentDateStart > _noCancelPeriod);
m_description = _description;
m_fileUrl = _fileUrl;
m_fileHash = _fileHash;
m_price = _price;
m_cancellationFee = _cancellationFee;
m_rentDateStart = _rentDateStart;
m_rentDateEnd = _rentDateEnd;
m_noCancelPeriod = _noCancelPeriod;
m_acceptObjectPeriod = _acceptObjectPeriod;
}
function Booking(
) public payable {
m_description = "My very long booking text about hotel and beautiful sea view!";
m_fileUrl = "https://ether-airbnb.bam/some-url/";
m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7;
m_price = 1000000000000000000; // 1 ETH
m_cancellationFee = 100000000000000000; // 0.1 ETH
m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day
m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days
m_acceptObjectPeriod = 3600 * 8; // 8 hours
m_noCancelPeriod = 3600 * 24; // 1 day
require(m_price > 0);
require(m_price > m_cancellationFee);
require(m_rentDateStart > 1550664800);
require(m_rentDateEnd > m_rentDateStart);
require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd);
require(m_rentDateStart > m_noCancelPeriod);
}
mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states
mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............
==== Dependence on predictable environment variable ====
SWC ID: 116
Severity: Low
Contract: Booking
Function name: fallback
PC address: 566
Estimated Gas Usage: 17908 - 61696
Sending of Ether depends on a predictable variable.
The contract sends Ether depending on the values of the following variables:
- block.timestamp
Note that the values of variables like coinbase, gaslimit, block number and timestamp
are predictable and/or can be manipulated by a malicious miner.
Do not use them for random number generation or to make critical decisions.
--------------------
In file: contracts/flattened.sol:142
msg.sender.transfer(msg.value-m_price)
require(m_rentDateStart > getCurrentTime());
function getCurrentTime() public view returns (uint256) {
- return now;
+ return getCurrentTimeInner();
}
+ function getCurrentTimeInner() internal returns (uint256) {
+ return now;
+ }
function collectTaxes() external onlyState(State.PAID) {
msg.sender.transfer(address(this).balance / 5);
}
==== Unprotected Ether Withdrawal ====
SWC ID: 105
Severity: High
Contract: Booking
Function name: collectTaxes()
PC address: 2492
Estimated Gas Usage: 2135 - 2746
Anyone can withdraw ETH from the contract account.
Arbitrary senders other than the contract creator can withdraw ETH from the contract
account without previously having sent a equivalent amount of ETH to it.
This is likely to be a vulnerability.
--------------------
In file: contracts/flattened.sol:149
msg.sender.transfer(address(this).balance / 5)
--------------------
--------------------
Transaction Sequence:
{
"2": {
"calldata": "0x",
"call_value": "0xde0b6b3a7640000",
"caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
},
"3": {
"calldata": "0x01b613a5",
"call_value": "0x0",
"caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
}
}
- function collectTaxes() external onlyState(State.PAID){
+ function collectTaxes() external onlyState(State.RENT) {