Sword-Smith / Sword

Sword — A financial derivative language for the blockchain
MIT License
29 stars 2 forks source link

Test coverage of signed/unsigned/overflow errors #2

Open Sword-Smith opened 3 years ago

Sword-Smith commented 3 years ago

Currently the compiler sometimes treats numbers as uint256 and sometimes as signed "int256". For all arithmetic operations, we should treat the numbers as signed int256 and check for overflow and negative numbers all necessary places.

Sword-Smith commented 3 years ago

The Open Zeppelin implementation of overflow and other arithmetic checks for signed numbers can be found here https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/math/SignedSafeMath.sol

Ulrik-dk commented 3 years ago
  • Check for overflow after all arithmetic operations

  • Change all arithmetic operations to signed operations

Implemented based on

https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/math/SignedSafeMath.sol

In the commit

https://github.com/Sword-Smith/Daggerc2.0/commit/91d5af5fb84b83f0b475d7a1d6520b053763b561

Some of them perform several checks for extremely unlikely edgecases, and some gas could be saved by optimizing for the average case.

These are my attempts at implementing the mentioned library. The instructions are interlaced with the state of the stack. The code in this comment is taken from the commit and the referenced library.

  1. SafeAdd
function add(int256 a, int256 b) internal pure returns (int256) {
    int256 c = a + b;
    require((b >= 0 && c >= a) || (b < 0 && c < a), "SignedSafeMath: addition overflow");

    return c;
}

I contend that (b >= 0 && c >= a) || (b < 0 && c < a) is equivalent to, but less efficient than, b < 0 xnor c < a. require(X) becomes if !X, throw, hence the xor.

a,b
DUP1,
a,a,b
DUP1,
a,a,a,b
DUP4,
b,a,a,a,b
ADD,
c,a,a,b
SLT,
c<a,a,b
PUSH1 0,
0,c<a,a,b
DUP4,
b,0,c<a,a,b
SLT,
b<0,c<a,a,b
XOR,
b<0 xor c<a,a,b
JUMPITO "global_throw",
a,b
ADD
c
  1. SafeSub
function sub(int256 a, int256 b) internal pure returns (int256) {
    int256 c = a - b;
    require((b >= 0 && c <= a) || (b < 0 && c > a), "SignedSafeMath: subtraction overflow");

    return c;
}

With similar reasoning here as with SafeAdd, we get that this is equivalent to: !(!A ^ !B) := !(b < 0 ^ c > a)

a,b
DUP1,
a,a,b
DUP3,
b,a,a,b
DUP2,
a,b,a,a,b
SUB,
c,a,a,b
SGT,
c>a,a,b
PUSH1 0,
0,c>a,a,b
DUP4,
b,0,c>a,a,b
SLT,
b<0,c>a,a,b
XOR,
b<0 xor c>a,a,b
JUMPITO "global_throw",
a,b
SUB
c
  1. SafeDiv

    function div(int256 a, int256 b) internal pure returns (int256) {
    require(b != 0, "SignedSafeMath: division by zero");
    require(!(b == -1 && a == _INT256_MIN), "SignedSafeMath: division overflow");
    
    int256 c = a / b;
    
    return c;
    }
label_skip <- newLabel "skip"
DUP2,
ISZERO,
JUMPITO "global_throw",
DUP1,
PUSH32 (0x80000000, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0),
SUB,
JUMPITO label_skip,
DUP2,
PUSH32 (0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF),
EVM_EQ,
JUMPITO "global_throw",
JUMPDESTFROM label_skip,
SDIV
  1. SafeMul

function mul(int256 a, int256 b) internal pure returns (int256) { // Gas optimization: this is cheaper than requiring 'a' not being zero, but the // benefit is lost if 'b' is also tested. // See: https://github.com/OpenZeppelin/openzeppelin-contracts/pull/522 if (a == 0) { return 0; }

require(!(a == -1 && b == _INT256_MIN), "SignedSafeMath: multiplication overflow");

int256 c = a * b;
require(c / a == b, "SignedSafeMath: multiplication overflow");

return c;

}


```haskell
label_return <- newLabel "return"
label_skip <- newLabel "skip"
label_skip2 <- newLabel "skip"

DUP1,
JUMPITO label_skip,
POP,
POP,
PUSH1 0,
JUMPITO label_return,
JUMPDESTFROM label_skip,
DUP2,
DUP2,
DUP2,
DUP2,
MUL, --c = a*b
DIV,
SUB,
JUMPITO "global_throw",
DUP2,
PUSH32 (0x80000000, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0, 0x0),
SUB,
JUMPITO label_skip2,
DUP1,
PUSH32 (0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF, 0xFFFFFFFF),
EVM_EQ,
JUMPITO "global_throw",
JUMPDESTFROM label_skip2,
MUL,
JUMPDESTFROM label_return
  1. Future work These four different implementations all check some very rare edgecases. Gas can possibly be saved by optimizing for the average case. This is especially obvious in SafeMul, where a jump might save gas eqv. to 4-5 other instructions in execution. This would be more expensive when publishing the code, however, so I am not sure what is best.

EDIT: The decision was made to optimize for execution of the average case, and assume amortization of edge-cases and publication cost.

Ulrik-dk commented 3 years ago
  • Change all comparison operations to signed

Done in this commit: https://github.com/Sword-Smith/Daggerc2.0/commit/fba60c2ce36da03b81efd6931229822cbd3ff8f4

EVM_LT -> SLT EVM_GT -> SGT

Ulrik-dk commented 3 years ago

In order to

  • Verify that all input values are positive when interpreted as int256 (two complement)

I have to figure out where exactly there are inputs to check.

This snippet will global-throw if the top element on the stack is not a natural number.

DUP1,
push 0,
SLT,
ISZERO,
JUMPITO "global_throw"
Sword-Smith commented 3 years ago

In order to

  • Verify that all input values are positive when interpreted as int256 (two complement)

I have to figure out where exactly there are inputs to check.

This snippet will global-throw if the top element on the stack is not a natural number.

DUP1,
push 0,
SLT,
ISZERO,
JUMPITO "global_throw"

The EVM Compiler module produces a jump table. That would probably be a good place to start reasoning about the input validation.

Ulrik-dk commented 3 years ago
  • Verify that all input values are positive when interpreted as int256 (two complement)

Implemented in: https://github.com/Sword-Smith/Daggerc2.0/commit/ea5749a6ae7cce514eee5ce69b79830da4fa64d8

Ulrik-dk commented 3 years ago

i256.min and -1i256 should be constants somewhere / subroutines.

Ulrik-dk commented 3 years ago

We need to use SafeMul other places in the code

Ulrik-dk commented 3 years ago
sshine commented 3 years ago

Why does safeMulShort but not safeMul work in burn?

This problem was caused by multiple calls to runCompiler so that overlapping labels were possible.

It has been fixed by making a single call to runCompiler so that the label counter is re-used between compilations of each Compiler [EvmOpcode]. See EvmCompiler.evmCompile.

Let us leave this issue open to remind us that we want very thorough testing of numeric overflows.