diff --git a/README.md b/README.md index 072012a..31348f5 100644 --- a/README.md +++ b/README.md @@ -1,9 +1,12 @@ # Sabre [![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG) -Sabre is a security analysis tool for smart contracts written in Solidity. It uses the [MythX cloud service](https://mythx.io) which detects [a wide range of security issues](https://mythx.io/swc-coverage). +Sabre is a security analysis tool for smart contracts written in Solidity. It uses the [MythX symbolic execution & fuzzing service](https://mythx.io) to: -**Warning: This client is not officially supported by MythX and may not return optimal results. Please use the [MythX command line client](https://github.com/dmuhs/mythx-cli) in production environments .** +- Generically detect [a wide range of security issues](https://mythx.io/swc-coverage); +- Check for assertion violations and produce counter-examples. + +**Warning: This is my own MythX client hobby implementation. Please use the official [MythX command line client](https://github.com/dmuhs/mythx-cli) in production environments .** ## Usage @@ -15,46 +18,270 @@ $ npm install -g sabre-mythx ### Setting up an Account -Sign up for a free account on the [MythX website](https://mythx.io) to generate an API key. Set the `MYTHX_API_KEY` enviroment variable by adding the following to your `.bashrc` or `.bash_profile`): +Sign up for an on the [MythX website](https://mythx.io) to generate an API key. Set the `MYTHX_API_KEY` enviroment variable by adding the following to your `.bashrc` or `.bash_profile`): ``` export MYTHX_API_KEY=eyJhbGciOiJI(...) ``` -### Analyzing a Solidity File +### Generic bug detection Run `sabre analyze [contract-name]` to submit a smart contract for analysis. The default mode is "quick" analysis which returns results after approximately 2 minutes. You'll also get a dashboard link where you can monitor the progress and view the report later. -#### Analysis mode +### Custom property checking + +To check specifically for assertion violations and print counter-examples for any violations found, run the following: ``` ---mode +$ sabre check [contract-name] ``` -MythX integrates various analysis methods including static analysis, input fuzzing and symbolic execution. In the backend, each incoming analysis job is distributed to a number of workers that perform various tasks in parallel. There are two analysis modes, "quick", "standard" and "deep", that differ in the amount of resources dedicated to the analysis. +#### Example 1: Primality test +You're pretty sure that 973013 is a prime number. It ends with a "3" so why wouldn't it be?? -#### Report format ``` ---format +pragma solidity ^0.5.0; + +contract Primality { + + uint256 public largePrime = 973013; + + uint256 x; + uint256 y; + + function setX(uint256 _x) external { + x = _x; + } + + function setY(uint256 _y) external { + y = _y; + } + + function verifyPrime() external view { + require(x > 1 && x < largePrime); + require(y > 1 && y < largePrime); + assert(x*y != largePrime); + } +} ``` -Select the report format. By default, Sabre outputs a verbose text report. Other options `stylish`, `compact`, `table`, `html` and `json`. Note that you can also view reports for past analyses on the [dashboard](http://dashboard.mythx.io). +Surely the assertion in `verifyPrime()` will hold for all possible inputs? -#### Client tool name ``` ---clientToolName +$ sabre check primality.sol +-------------------- +ASSERTION VIOLATION! +/Users/bernhardmueller/Desktop/primality.sol: from 21:8 to 21:33 + +assert(x*y != largePrime) +-------------------- +Call sequence: + + 1: setY(1021) + Sender: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa [ USER ] + Value: 0 + + 2: setX(953) + Sender: 0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe [ CREATOR ] + Value: 0 + + 3: verifyPrimeness() + Sender: 0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe [ CREATOR ] + Value: 0 + ``` -You can [integrate Sabre into your own MythX tool](https://docs.mythx.io/en/latest/building-security-tools/) and become eligible for a share of API revenues. In that case, you'll want to use the `--clientToolName` argument to override the tool id which is used by the API to identify your tool. +Oh no! 1021 x 953 = 973013, better pick a different number 🙄 + +#### Example 2: Integer precision bug + +Source: [Sigma Prime](https://blog.sigmaprime.io/solidity-security.html#precision-vuln) + +Here is a simple contract for buying and selling tokens. What could possibly go wrong? ``` ---debug +pragma solidity ^0.5.0; + +contract FunWithNumbers { + uint constant public tokensPerEth = 10; + uint constant public weiPerEth = 1e18; + mapping(address => uint) public balances; + + function buyTokens() public payable { + uint tokens = msg.value/weiPerEth*tokensPerEth; // convert wei to eth, then multiply by token rate + balances[msg.sender] += tokens; + } + + function sellTokens(uint tokens) public { + require(balances[msg.sender] >= tokens); + uint eth = tokens/tokensPerEth; + balances[msg.sender] -= tokens; + msg.sender.transfer(eth*weiPerEth); + } +} ``` -Dump the API request and reponse when submitting an analysis. +Better safe than sorry! Let's check some [contract invariants](https://gist.github.com/b-mueller/0916c3700c94e94b23dfa9aa650005e8) just to be 1,700% sure that everything works as expected. + +``` +$ sabre check funwithnumbers.sol +-------------------- +ASSERTION VIOLATION! +/Users/bernhardmueller/Desktop/funwithnumbers.sol: from 47:17 to 47:131 + +AssertionFailed("Invariant violation: Sender token balance must increase when contract account balance increases") +-------------------- +Call sequence: + + 1: buyTokens() + Sender: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa3 [ USER ] + Value: 6 + +-------------------- +ASSERTION VIOLATION! +/Users/bernhardmueller/Desktop/funwithnumbers.sol: from 56:17 to 56:131 + +AssertionFailed("Invariant violation: Contract account balance must decrease when sender token balance decreases") +-------------------- +Call sequence: + + 1: buyTokens() + Sender: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa0 [ USER ] + Value: 1000000000000000000 + + 2: sellTokens(6) + Sender: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa0 [ USER ] + Value: 0 +``` + +Um what?? Fractional numbers are rounded down 😲 + +#### Example 3: Arbitrary storage write + +Source: [Ethernaut](https://ethernaut.openzeppelin.com/level/0xe83cf387ddfd13a2db5493d014ba5b328589fb5f) (I made this [a bit more complex](https://gist.github.com/b-mueller/44a995aaf764051963802a061665b446)) + +This [smart contract](https://gist.github.com/b-mueller/44a995aaf764051963802a061665b446) has, and will always have, only one owner. There isn't even a `transferOwnership` function. But... can you be really sure? Don't you at least want to double-check with a high-level, catch-all invariant? + +``` +contract VerifyRegistrar is Registrar { + + modifier checkInvariants { + address old_owner = owner; + _; + assert(owner == old_owner); + } + + function register(bytes32 _name, address _mappedAddress) checkInvariants public { + super.register(_name, _mappedAddress); + } +} +``` + +Let's check just to be 15,000% sure. + + +``` +$ sabre check registrar.sol +✔ Loaded solc v0.4.25 from local cache +✔ Compiled with solc v0.4.25 successfully +✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/e98a345e-7418-4209-ab99-bffdc2535d9b +-------------------- +ASSERTION VIOLATION! +/Users/bernhardmueller/Desktop/registrar.sol: from 40:8 to 40:34 + +assert(owner == old_owner) +-------------------- +Call sequence: + + 1: register(b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00', 0x0000000000000000000000000000000000000000) + Sender: 0xaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa [ USER ] + Value: 0 +``` + +Ooops... better initialize those structs before using them. + +#### Example 4: Pausable token + +Source: [TrailofBits](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise1) + +Smart contracts get hacked all the time so it's always great to have a pause button, even if it's just a [simple token +](https://github.com/crytic/building-secure-contracts/tree/master/program-analysis/echidna/exercises/exercise1). This is even an off-switch if we pause the token and throw away the admin account? Or is it? + +Why not create an instance of the contract that's infinitely paused and check if there's any way to unpause it. + +``` +contract VerifyToken is Token { + + event AssertionFailed(string message); + + constructor() public { + paused(); + owner = address(0x0); // lose ownership + } + + function transfer(address to, uint value) public { + uint256 old_balance = balances[msg.sender]; + + super.transfer(to, value); + + if (balances[msg.sender] != old_balance) { + emit AssertionFailed("Tokens transferred even though this contract instance was infinitely paused!!"); + } + } +} +``` + +Given that this contract is forever paused, it should never be possible to transfer any tokens right? + + +``` +$ sabre check token.sol +✔ Loaded solc v0.5.16 from local cache +✔ Compiled with solc v0.5.16 successfully +✔ Analysis job submitted: https://dashboard.mythx.io/#/console/analyses/8d4b0eb0-69d3-4d82-b6c6-bc90332a292c +-------------------- +ASSERTION VIOLATION! +/Users/bernhardmueller/Desktop/token.sol: from 64:17 to 64:113 + +AssertionFailed("Tokens transferred even though this contract instance was infinitely paused!!") +-------------------- +Call sequence: + + 1: Owner() + Sender: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ] + Value: 0 + + 2: resume() + Sender: 0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef [ ATTACKER ] + Value: 0 + + 3: transfer(0x0008000002400240000200104000104080001000, 614153205830163099331592192) + Sender: 0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe [ CREATOR ] + Value: 0 +``` + +Oh no 😵 Looks like somebody slipped up there when naming the constructor. + +### Analysis mode + +``` +--mode +``` + +MythX integrates various analysis methods including static analysis, input fuzzing and symbolic execution. In the backend, each incoming analysis job is distributed to a number of workers that perform various tasks in parallel. There are two analysis modes, "quick", "standard" and "deep", that differ in the amount of resources dedicated to the analysis. + + +### Report format + +``` +--format +``` + +Select the report format. By default, Sabre outputs a verbose text report. Other options `stylish`, `compact`, `table`, `html` and `json`. Note that you can also view reports for past analyses on the [dashboard](http://dashboard.mythx.io). + ### Other commands @@ -66,3 +293,26 @@ Besides `analyze` the following commands are available. - version Print Sabre Version - apiVersion Print MythX API version ``` + +### Debugging + +``` +--debug +``` + +Dump the API request and reponse when submitting an analysis. + +# How it works + +Some articles and papers explaining the tech behind that runs in [MythX](https://mythx.io): + +- [Finding Vulnerabilities in Smart Contracts (Harvey Basics)](https://medium.com/consensys-diligence/finding-vulnerabilities-in-smart-contracts-175c56affe2) +- [Fuzzing Smart Contracts Using Input Prediction](https://medium.com/consensys-diligence/fuzzing-smart-contracts-using-input-prediction-29b30ba8055c) +- [Fuzzing Smart Contracts Using Multiple Transactions](https://medium.com/consensys-diligence/fuzzing-smart-contracts-using-multiple-transactions-51471e4b3c69) +- [Learning Inputs in Greybox Fuzzing (Arxiv)](https://arxiv.org/pdf/1807.07875.pdf) +- [Targeted Greybox Fuzzing using Lookahead Analysis (Arxiv)](https://arxiv.org/abs/1905.07147) +- [Intro to Symbolic Execution in Mythril](https://medium.com/@joran.honig/introduction-to-mythril-classic-and-symbolic-execution-ef59339f259b) +- [Advances in Smart Contract Vulnerability Detection (DEFCON 27)](https://github.com/b-mueller/smashing-smart-contracts/blob/master/DEFCON27-EVM-Smart-Contracts-Mueller-Luca.pdf) +- [Smashing Smart Contracts (HITB GSEC 2018)](https://conference.hitb.org/hitbsecconf2018ams/materials/D1T2%20-%20Bernhard%20Mueller%20-%20Smashing%20Ethereum%20Smart%20Contracts%20for%20Fun%20and%20ACTUAL%20Profit.pdf) +- [The Tech Behind MythX (high-level)](https://medium.com/consensys-diligence/the-tech-behind-mythx-smart-contract-security-analysis-32c849aedaef) +- [Practical Mutation Testing in Smart Contracts](https://www.researchgate.net/publication/335937116_Practical_Mutation_Testing_for_Smart_Contracts) diff --git a/contracts/Primality.sol b/contracts/Primality.sol new file mode 100644 index 0000000..4fd17af --- /dev/null +++ b/contracts/Primality.sol @@ -0,0 +1,23 @@ +pragma solidity ^0.5.0; + +contract Primality { + + uint256 public largePrime = 973013; + + uint256 x; + uint256 y; + + function setX(uint256 _x) external { + x = _x; + } + + function setY(uint256 _y) external { + y = _y; + } + + function verifyPrime() external view { + require(x > 1 && x < largePrime); + require(y > 1 && y < largePrime); + assert(x*y != largePrime); + } +} diff --git a/lib/client.js b/lib/client.js index 7c3df96..47fd02d 100644 --- a/lib/client.js +++ b/lib/client.js @@ -92,8 +92,8 @@ const authenticate = async (client) => { return await client.login(); }; -const submitDataForAnalysis = async(client, data) => { - return await client.analyze(data); +const submitDataForAnalysis = async(client, data, isCheckProperty = false) => { + return await client.analyze(data, isCheckProperty); }; const getReport = async (client, uuid) => { diff --git a/lib/controllers/analyze.js b/lib/controllers/analyze.js index 1e186a5..28062a2 100644 --- a/lib/controllers/analyze.js +++ b/lib/controllers/analyze.js @@ -137,7 +137,7 @@ module.exports = async (env, args) => { spinner.start(); } - const { uuid } = await client.submitDataForAnalysis(mxClient, data); + const { uuid } = await client.submitDataForAnalysis(mxClient, data, args.isCheckProperty); spinner.succeed( 'Analysis job submitted: ' + @@ -153,11 +153,10 @@ module.exports = async (env, args) => { if (args.mode === 'quick') { initialDelay = 20 * 1000; timeout = 300 * 1000; - } else if (args.mode === 'standard' || args.mode == 'full') { + } else if (args.mode === 'standard' || args.mode === 'full') { initialDelay = 900 * 1000; timeout = 1800 * 1000; - } - else { + } else { initialDelay = 2700 * 1000; timeout = 5400 * 1000; } @@ -203,7 +202,9 @@ module.exports = async (env, args) => { console.log(chalk.green(`✔ No errors/warnings found in ${args._[0]} for contract: ${compiledData.contractName}`)); } else { - const formatter = report.getFormatter(args.format); + // Custom text format for property checking + const format = args.isCheckProperty && args.format === 'text' ? 'propertyCheckText' : args.format; + const formatter = report.getFormatter(format); const output = formatter(uniqueIssues); spinner.stop(); diff --git a/lib/controllers/help.js b/lib/controllers/help.js index 5601153..98e22a0 100644 --- a/lib/controllers/help.js +++ b/lib/controllers/help.js @@ -5,7 +5,8 @@ USAGE: $ sabre COMMANDS: - analyze [options] [contract_name] Analyze the given directory or arguments with MythX + analyze [options] [contract_name] Generically test for ~50 security bugs + check [options] [contract_name] Check for assertion violations list Get a list of submitted analyses. status Get the status of an already submitted analysis version Print version diff --git a/lib/formatters/propertyCheckText.js b/lib/formatters/propertyCheckText.js new file mode 100644 index 0000000..66b4070 --- /dev/null +++ b/lib/formatters/propertyCheckText.js @@ -0,0 +1,166 @@ +const separator = '-'.repeat(20); +const indent = ' '.repeat(4); + +const roles = { + creator: 'CREATOR', + attacker: 'ATTACKER', + other: 'USER' +}; + +const textFormatter = {}; + +textFormatter.strToInt = str => parseInt(str, 10); + +textFormatter.guessAccountRoleByAddress = (address) => { + const prefix = address.toLowerCase().substr(0, 10); + + if (prefix === '0xaffeaffe') { + return roles.creator; + } else if (prefix === '0xdeadbeef') { + return roles.attacker; + } + + return roles.other; +}; + +textFormatter.stringifyValue = (value) => { + const type = typeof value; + + if (type === 'number') { + return String(value); + } else if (type === 'string') { + return value; + } else if (value == null) { + return 'null'; + } + + return JSON.stringify(value); +}; + +textFormatter.formatTestCaseSteps = (steps, /*fnHashes*/) => { + const output = []; + + for (let s = 0, n = 0; s < steps.length; s++) { + const step = steps[s]; + + /** + * Empty address means "contract creation" transaction. + * + * Skip it to not spam. + */ + if (step.address === '') { + continue; + } + + n++; + + const type = textFormatter.guessAccountRoleByAddress(step.origin); + + // const fnHash = step.input.substr(2, 8); + // const fnName = fnHashes[fnHash] || step.name || ''; + // const fnDesc = `${fnName} [ ${fnHash} ]`; + + let decodedInput = 'DECODING FAILED :( RAW CALLDATA: ' + textFormatter.stringifyValue(step.input); + + if ('decodedInput' in step) { + decodedInput = step.decodedInput; + } + + output.push( + indent + `${n}: ${decodedInput}`, + indent + `Sender: ${step.origin} [ ${type} ]`, + indent + `Value: ${parseInt(step.value)}`, + '' + ); + + } + + return output.join('\n').trimRight(); +}; + +textFormatter.formatTestCase = (testCase, fnHashes) => { + const output = []; + + if (testCase.steps) { + const content = textFormatter.formatTestCaseSteps( + testCase.steps, + fnHashes + ); + + if (content) { + output.push('Call sequence:', '', content); + } + } + + return output.length ? output.join('\n') : undefined; +}; + +textFormatter.getCodeSample = (source, src) => { + const [start, length] = src.split(':').map(textFormatter.strToInt); + + return source.substr(start, length); +}; + +textFormatter.formatLocation = message => { + const start = message.line + ':' + message.column; + const finish = message.endLine + ':' + message.endCol; + + return 'from ' + start + ' to ' + finish; +}; + +textFormatter.formatMessage = (message, filePath, sourceCode, fnHashes) => { + const { mythxIssue, mythxTextLocations } = message; + const output = []; + + const code = mythxTextLocations.length + ? textFormatter.getCodeSample( + sourceCode, + mythxTextLocations[0].sourceMap + ) + : undefined; + + output.push( + separator, + 'ASSERTION VIOLATION!', + filePath + ': ' + textFormatter.formatLocation(message), + '', + code || '' + ); + + const testCases = mythxIssue.extra && mythxIssue.extra.testCases; + + if (testCases) { + for (const testCase of testCases) { + const content = textFormatter.formatTestCase(testCase, fnHashes); + + if (content) { + output.push(separator, content); + } + } + } + + return output.join('\n'); +}; + +textFormatter.formatResult = result => { + const { filePath, sourceCode, functionHashes } = result; + + return result.messages + .map( + message => textFormatter.formatMessage( + message, + filePath, + sourceCode, + functionHashes + ) + ) + .join('\n\n'); +}; + +textFormatter.run = results => { + return results + .map(result => textFormatter.formatResult(result)) + .join('\n\n'); +}; + +module.exports = results => textFormatter.run(results); diff --git a/lib/formatters/text.js b/lib/formatters/text.js index 142936c..5cf77ec 100644 --- a/lib/formatters/text.js +++ b/lib/formatters/text.js @@ -69,12 +69,13 @@ textFormatter.formatTestCaseSteps = (steps, fnHashes) => { ); if ('decodedInput' in step) { - output.push(indent + "Decoded Calldata: " + step.decodedInput); - } + output.push(indent + 'Decoded Calldata: ' + step.decodedInput); + } output.push( indent + 'Value: ' + textFormatter.stringifyValue(step.value), - ''); + '' + ); } diff --git a/lib/report.js b/lib/report.js index 292d162..9641301 100644 --- a/lib/report.js +++ b/lib/report.js @@ -14,7 +14,7 @@ const decoder = new SourceMappingDecoder(); * @returns ESLint formatter module */ const getFormatter = (name) => { - const custom = ['text']; + const custom = ['text', 'propertyCheckText']; if (custom.includes(name)) { name = path.join(__dirname, 'formatters/', name + '.js'); @@ -122,7 +122,7 @@ const issue2EsLint = (issue, sourceCode, locations) => { /** * Gets the source index from the issue sourcemap - * + * * @param {object} location - MythX API issue location object * @returns {number} */ @@ -146,7 +146,7 @@ const convertMythXReport2EsIssue = (report, data) => { /** * Filters locations only for source files. * Other location types are not supported to detect code. - * + * * @param {object} location */ const textLocationFilterFn = location => ( diff --git a/sabre.js b/sabre.js index d8dd0a8..2b62cf3 100755 --- a/sabre.js +++ b/sabre.js @@ -2,10 +2,10 @@ const env = { apiKey: process.env.MYTHX_API_KEY, - apiUrl: process.env.MYTHX_API_URL, + apiUrl: process.env.MYTHX_API_URL }; -let { apiUrl, apiKey } = env; +let { apiKey } = env; if (!apiKey) { console.log('Unauthenticated use of MythX has been discontinued. Sign up for a account at https://mythx.io/ and set the MYTHX_API_KEY environment variable.'); @@ -36,6 +36,10 @@ case 'list': case 'analyze': controller = require('./lib/controllers/analyze'); break; +case 'check': + controller = require('./lib/controllers/analyze'); + args.isCheckProperty = true; + break; case 'apiVersion': controller = require('./lib/controllers/api_version'); break;