Catching weird security bugs in Solidity smart contracts with global invariant checks

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);
}
}
modifier checkInvariants {    // Save old state    uint sender_balance_old = balances[msg.sender];    // Execute the function body
_;
// MythX AssertionFailed event if (--- this should never occur ---) {
emit AssertionFailed("Some error message");
}
// Solidity assertion assert(--- this should always hold ---);
}
contract VerifyFunWithNumbers is FunWithNumbers {

uint contract_balance_old;

constructor() public {
contract_balance_old = address(this).balance;
}

event AssertionFailed(string message);

modifier checkInvariants {
uint sender_balance_old = balances[msg.sender];

_;

if (address(this).balance > contract_balance_old && balances[msg.sender] <= sender_balance_old) {
emit AssertionFailed("Invariant violation: Sender token balance must increase when contract account balance increases");
}
if (balances[msg.sender] > sender_balance_old && contract_balance_old >= address(this).balance) {
emit AssertionFailed("Invariant violation: Contract account balance must increase when sender token balance increases");
}
if (address(this).balance < contract_balance_old && balances[msg.sender] >= sender_balance_old) {
emit AssertionFailed("Invariant violation: Sender token balance must decrease when contract account balance decreases");
}
if (balances[msg.sender] < sender_balance_old && address(this).balance >= contract_balance_old) {
emit AssertionFailed("Invariant violation: Contract account balance must decrease when sender token balance decreases");
}

contract_balance_old = address(this).balance;
}
function buyTokens() public payable checkInvariants {
super.buyTokens();
}

function sellTokens(uint tokens) public checkInvariants {
super.sellTokens(tokens);
}
}
User buys tokens for 6 Wei. 6/10 hets rounded to zero so no tokens are added to the user’s balance.
User buys a large amount of tokens, then sells 6 tokens. 6/10 is rounded to 0 so no Ether is paid.
pragma solidity ^0.5.0;contract Pwnable {
address public owner;
uint[] private bonusCodes;

constructor() public {
bonusCodes = new uint[](0);
owner = msg.sender;
}

function PushBonusCode(uint c) public {
bonusCodes.push(c);
}

function PopBonusCode() public {
require(0 <= bonusCodes.length);
bonusCodes.length--;
}

function UpdateBonusCodeAt(uint idx, uint c) public {
require(idx < bonusCodes.length);
bonusCodes[idx] = c;
}
}
assert(owner == old_owner || msg.sender == old_owner);
contract VerifyPwnable is Pwnable {    modifier checkInvariants {
address old_owner = owner;
_; assert(msg.sender == old_owner || owner == old_owner);
}

function PushBonusCode(uint c) public checkInvariants {
super.PushBonusCode(c);
}
function PopBonusCode() public checkInvariants {
super.PopBonusCode();
}
function UpdateBonusCodeAt(uint idx, uint c) public checkInvariants {
super.UpdateBonusCodeAt(idx, c);
}
}

TL;DR

You might also like:

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store