JoranHonig

pragma solidity ^0.6.0;

///#invariant unchecked_sum(_balances) == _totalSupply;
///#if_succeeds unchecked_sum(_balances) == old(unchecked_sum(_balances)) || msg.sig == bytes4(0x00000000);
contract AnnotatedToken {
  uint256 private _totalSupply;
  mapping (address => uint256) private _balances;
  mapping (address => mapping (address => uint256)) private _allowances;

  constructor() public {

JoranHonig

👷 What I work on

• tree-sitter-solidity
• Vertigo
• Mythril

⬅ Shift Left

• IBM Research - Relative cost of fixing defects
• BCM - What is shift left?

🔧 Early & Mid Stage | Analysis Tools

JoranHonig

# ~/.tmuxinator/sample.yml
# This is an example tmuxinator configuration that makes it easy to run a bunch of ganache instances in parallel
# The benefit of using tmux here is that we are easily able to view the output stream of the different instances

name: 2 ganache windows
root: ~/

windows:
  - editor:
      layout: tiled

JoranHonig

module.exports = {
  networks: {
    vertigo_test_network_1: {
      host: "127.0.0.1",
      port: 8545,
      network_id: "*"
    },
    vertigo_test_network_2: {
      host: "127.0.0.1",
      port: 8546,

JoranHonig

function max(uint256 a, uint256 b) internal pure returns (uint256) {
    return a >= b ? a : b;
}

function mutated_max(uint256 a, uint256 b) internal pure returns (uint256) {
    return a > b ? a : b;
}

JoranHonig

<   =>  >=
>   =>  <=
<=  =>  >
>=  =>  <
!=  =>  ==
==  =>  !=

JoranHonig

Keybase proof

I hereby claim:

• I am JoranHonig on github.
• I am joranhonig (https://keybase.io/joranhonig) on keybase.
• I have a public key whose fingerprint is D482 2663 9FC1 C6FD 20D5 F3DC A099 79F8 BB62 9E73

To claim this, I am signing this object:

JoranHonig

for state in states:
  # Let's filter all the states that are not return statements
  if state.currently_executing != 6:
    continue
  # We want the result to be 10, let's formulate that as a constraint
  result_constraint = (state.result == 10)
  
  # If it is possible to satisfy both the path constraints (these are the constraints collected on each branch)
  # and the result constraint then there must be an input that makes the function return 10
  if is_possible(result_constraint and state.constraints):

JoranHonig

function execute(uint256 input) public (uint256){
   uint memory result = 0;
   if (input > 10) {
      result += 10;
   }
   return result;
}

JoranHonig

let print_list f l =
  print_char '[';
  begin
    match l with
      [] -> ()
    | hd :: tl ->
      print_string (f hd);
      List.iter (fun x -> print_string (", " ^ (f x))) tl
  end;