Permalink
Browse files

wip

  • Loading branch information...
yzhang90 committed Jan 11, 2019
1 parent 83f9e19 commit 50259d2d769bd001fe006e848bfc89f0260f7141
Showing with 83 additions and 37 deletions.
  1. +2 −2 gnosis-imap/Makefile
  2. +67 −31 gnosis-imap/gnosis-imap-spec.ini
  3. +14 −4 gnosis/verification.k
@@ -84,10 +84,10 @@ $(SPECS_DIR)/$(SPEC_GROUP)/encodeTransactionData-public-2-spec.k: $(TMPLS) $(SPE
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) encodeTransactionData-public-2 encodeTransactionData-internal-trusted encodeTransactionData-public-2 > $@

$(SPECS_DIR)/$(SPEC_GROUP)/execTransaction-checkSigs1-gas1-safetxgas0-gasprice0-call1-to-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) execTransaction-checkSigs1-gas1-safetxgas0-gasprice0-call1-to encodeTransactionData-internal-trusted checkSignatures_dummy execTransaction-checkSigs1-gas1-safetxgas0-gasprice0-call1-to > $@
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) execTransaction-checkSigs1-gas1-safetxgas0-gasprice0-call1-to encodeTransactionData-internal-trusted checkSignatures_trusted-success execTransaction-checkSigs1-gas1-safetxgas0-gasprice0-call1-to > $@

$(SPECS_DIR)/$(SPEC_GROUP)/execTransaction-checkSigs1-gas1-safetxgas1-call1-to-gasprice1-send1-origin-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) execTransaction-checkSigs1-gas1-safetxgas1-call1-to-gasprice1-send1-origin encodeTransactionData-internal-trusted checkSignatures_dummy handlePayment-send-success-origin-trusted execTransaction-checkSigs1-gas1-safetxgas1-call1-to-gasprice1-send1-origin > $@
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) execTransaction-checkSigs1-gas1-safetxgas1-call1-to-gasprice1-send1-origin encodeTransactionData-internal-trusted checkSignatures_trusted-success handlePayment-send-success-origin-trusted execTransaction-checkSigs1-gas1-safetxgas1-call1-to-gasprice1-send1-origin > $@

# Identical execution path with execution path of encodeTransactionData-public, so no point to activate it.
$(SPECS_DIR)/$(SPEC_GROUP)/getTransactionHash-1-spec.k: $(TMPLS) $(SPEC_INI)
@@ -529,8 +529,7 @@ gas: #gas(INITGAS, NONMEMGAS, MEMGAS) => #gas(INITGAS, NONMEMGAS +Int #callGas(B
andBool #callFailure(CALL_PC, #REFUND_RECEIVER)


; dummy spec to see how localMem is changed
[checkSignatures_dummy]
[checkSignatures_trusted]
k: #execute ~> _
output: _ => _
statusCode: _ => _
@@ -539,57 +538,92 @@ this: #PROXY_ID
msg_sender: MSG_SENDER
callData: _
callValue: 0
memoryUsed: MU => FINAL_MEM_USAGE
log: _
refund: _
coinbase: _
pc: 18250 => 19453
pc: {PC_FUN_START} => {PC_FUN_END}
gas: #gas(INITGAS,
NONMEMGAS,
MEMGAS => MEMGAS +Int (Cmem(BYZANTIUM, FINAL_MEM_USAGE) -Int Cmem(BYZANTIUM, MU)) )
wordStack: 1 /* CONSUME_HASH */ : SIGS_LOC : TX_DATA_LOC : TX_DATA_HASH : RETURN_LOC : WS
=> RETURN_LOC : 1 /* return value */ : WS
localMem: M1 => storeRange(storeRange(M1,
NEXT_LOC, 96, _),
64, 32, #buf(32, NEXT_LOC +Int 96))
NONMEMGAS => NONMEMGAS +Int #checkSigsGasNonMem,
MEMGAS => MEMGAS +Int (Cmem(BYZANTIUM, FINAL_MEM_USAGE) -Int Cmem(BYZANTIUM, MU)))
memoryUsed: MU => FINAL_MEM_USAGE
wordStack:
; parameters
{CONSUME_HASH} : SIGS_LOC : TX_DATA_LOC : TX_DATA_HASH :
; return address
RETURN_LOC : WS
=>
{WORD_STACK_RHS}
localMem: M1 =>
storeRange(storeRange(storeRange(storeRange(storeRange(M2,
TX_DATA_LOC , 32 , #buf(32, TX_DATA_LEN)),
TX_DATA_LOC +Int 32, TX_DATA_LEN, TX_DATA_BUF),
SIGS_LOC , 32 , #buf(32, SIGS_LEN)),
SIGS_LOC +Int 32 , SIGS_LEN , SIGS_BUF),
64 , 32 , #buf(32, #checkSigsNextLoc))
proxy_storage:
S:IMap
+requires:
; elements
andBool THRESHOLD ==Int select(S, #hashedLocation({COMPILER}, {THRESHOLD}, .IntList))
andBool FINAL_MEM_USAGE ==Int #checkSigsFinalMemUsed(MU)
andBool THRESHOLD ==Int select(S, #hashedLocation({COMPILER}, {THRESHOLD}, .IntList))
andBool TX_DATA_LEN ==Int #asWord(selectRange(M1, TX_DATA_LOC, 32))
andBool SIGS_LEN ==Int #asWord(selectRange(M1, SIGS_LOC, 32))

andBool TX_DATA_BUF ==K selectRange(M1, TX_DATA_LOC +Int 32, TX_DATA_LEN)
andBool SIGS_BUF ==K selectRange(M1, SIGS_LOC +Int 32, SIGS_LEN)

; no overflow
andBool #rangeUInt(256, THRESHOLD *Int 65)

; ranges
andBool #range(0 <= #sizeWordStack(WS) <= 1000 -Int 12)

andBool #range(0 <= CD < 1023)
; bool consumeHash: assumed to be true
; bool consumeHash
andBool #range(0 <= {CONSUME_HASH} <= 1)
; bytes memory signatures
andBool #rangeUInt(256, SIGS_LOC)
; bytes memory data
andBool #rangeUInt(256, TX_DATA_LOC)
; bytes32 dataHash
andBool #rangeUInt(256, TX_DATA_HASH)
; andBool #range(0 <= #sizeWordStack(WS) <= 990)
andBool #rangeUInt(256, THRESHOLD)
andBool #rangeUInt(256, NEXT_LOC)
andBool #rangeUInt(256, TX_DATA_LEN)
andBool #rangeUInt(256, SIGS_LEN)
andBool #rangeAddress(MSG_SENDER)

; practical bounds for localMem address
andBool #range(128 <= SIGS_LOC < 2 ^Int 32)
andBool #range(128 <= TX_DATA_LOC < 2 ^Int 32)
; rough bounds for lengths related to localMem address
andBool TX_DATA_LEN <Int 2 ^Int 16
andBool SIGS_LEN <Int 2 ^Int 16
andBool THRESHOLD <Int 2 ^Int 32

; invariants
; no overlap between data and sigatures
andBool TX_DATA_LOC +Int 32 +Int TX_DATA_LEN <=Int SIGS_LOC

; contract invariants
andBool 1 <=Int THRESHOLD
+ensures:
andBool #rangeUInt(256, #checkSigsNextLoc)
andBool #range(128 <= #checkSigsNextLoc < 2 ^Int 32)
andBool #range(SIGS_LOC +Int 32 +Int #ceil32(SIGS_LEN) <= #checkSigsNextLoc < 2 ^Int 32)

+attribute: [trusted, matching(#gas)]

andBool TX_DATA_LEN ==Int #asWord(selectRange(M1, TX_DATA_LOC, 32))
andBool SIGS_LEN ==Int #asWord(selectRange(M1, SIGS_LOC, 32))
andBool NEXT_LOC ==Int #asWord(selectRange(M1, 64, 32))
CONSUME_HASH: 1

andBool TX_DATA_BUF ==K selectRange(M1, TX_DATA_LOC, TX_DATA_LEN)
andBool SIGS_BUF ==K selectRange(M1, SIGS_LOC, SIGS_LEN)
andBool FINAL_MEM_USAGE ==Int #memoryUsageUpdate(MU, NEXT_LOC, 96)
PC_FUN_START: 18250
PC_FUN_END: 19453

andBool #checkSigsSuccess
+attribute: [trusted, matching(#gas)]
[checkSignatures_trusted-success]
+requires:
; enough signatures
andBool THRESHOLD *Int 65 <=Int SIGS_LEN
; valid signatures
andBool #enoughValidSigs
WORD_STACK_RHS: RETURN_LOC : 1 : WS


; internal
@@ -660,9 +694,9 @@ MEM_RHS: M2
andBool #rangeAddress(MSG_SENDER)

; practical bounds for localMem address
andBool #range(96 <= SIGS_LOC < 2 ^Int 32)
andBool #range(96 <= TX_DATA_LOC < 2 ^Int 32)
andBool #range(96 <= NEXT_LOC < 2 ^Int 32)
andBool #range(128 <= SIGS_LOC < 2 ^Int 32)
andBool #range(128 <= TX_DATA_LOC < 2 ^Int 32)
andBool #range(128 <= NEXT_LOC < 2 ^Int 32)
; rough bounds for lengths related to localMem address
andBool TX_DATA_LEN <Int 2 ^Int 16
andBool SIGS_LEN <Int 2 ^Int 16
@@ -699,7 +733,6 @@ DATA_BUF: #buf(TX_DATA_LEN, TX_DATA)
andBool #fii({SIGS_BUF}, TX_DATA_HASH, {DATA_BUF}, S, MSG_SENDER) >=Int THRESHOLD
WORD_STACK_RHS: RETURN_LOC : 1 : WS


[checkSignatures-failure]
WORD_STACK_RHS: RETURN_LOC : 0 : WS

@@ -1108,12 +1141,15 @@ proxy_origstorage: store(M2, #hashedLocation({COMPILER}, {NONCE}, .IntList),

[execTransaction-checkSigs1]
+requires:
andBool #checkSigsSuccess
; enough signatures
andBool THRESHOLD *Int 65 <=Int SIGS_LEN
; valid signatures
andBool #enoughValidSigs

[execTransaction-checkSigs1-gas1]
+requires:
// gasleft() >= safeTxGas
andBool SAFE_TX_GAS <=Int #gas(INITGAS, 9 *Int (DATA_LEN up/Int 32) +Int 3 *Int (SIGS_LEN up/Int 32) +Int Csstore(BYZANTIUM, NONCE +Int 1, NONCE, ORIG_NONCE) +Int 2903, Cmem(BYZANTIUM, #memoryUsageUpdate(5, #ceil32(DATA_LEN) +Int #ceil32(SIGS_LEN) +Int 674, 96)))
andBool SAFE_TX_GAS <=Int #gas(INITGAS, 9 *Int (DATA_LEN up/Int 32) +Int 3 *Int (SIGS_LEN up/Int 32) +Int #checkSigsGasNonMem +Int Csstore(BYZANTIUM, NONCE +Int 1, NONCE, ORIG_NONCE) +Int 2903, Cmem(BYZANTIUM, #checkSigsFinalMemUsed(#memoryUsageUpdate(5, #ceil32(DATA_LEN) +Int 674 +Int SIGS_LEN, 32))))

[execTransaction-checkSigs1-gas1-safetxgas0-gasprice0]
+requires:
@@ -1162,7 +1198,7 @@ proxy_bal: PROXY_BAL => PROXY_BAL -Int VALUE -Int TOTAL_AMOUNT
origin_bal: ORIGIN_BAL => ORIGIN_BAL +Int TOTAL_AMOUNT
+requires:
andBool START_GAS ==Int #gas(INITGAS, 990, 9)
andBool GAS_LEFT ==Int #gas(INITGAS, 12 *Int (DATA_LEN up/Int 32) +Int 3 *Int (SIGS_LEN up/Int 32) +Int Csstore(BYZANTIUM, NONCE +Int 1, NONCE, ORIG_NONCE) +Int #callGas(BYZANTIUM, SAFE_TX_GAS, #EXEC_ACCT_TO, VALUE, true) +Int 3499, Cmem(BYZANTIUM, #memoryUsageUpdate(5, #ceil32(DATA_LEN) +Int #ceil32(SIGS_LEN) +Int 802 +Int DATA_LEN, 32)))
andBool GAS_LEFT ==Int #gas(INITGAS, 12 *Int (DATA_LEN up/Int 32) +Int 3 *Int (SIGS_LEN up/Int 32) +Int #checkSigsGasNonMem +Int Csstore(BYZANTIUM, NONCE +Int 1, NONCE, ORIG_NONCE) +Int #callGas(BYZANTIUM, SAFE_TX_GAS, #EXEC_ACCT_TO, VALUE, true) +Int 3499, Cmem(BYZANTIUM, #memoryUsageUpdate(#checkSigsFinalMemUsed(#memoryUsageUpdate(5, #ceil32(DATA_LEN) +Int 674 +Int SIGS_LEN, 32)), #checkSigsNextLoc +Int 32 +Int DATA_LEN, 32)))
andBool TOTAL_GAS ==Int (START_GAS -Int GAS_LEFT) +Int DATA_GAS
andBool TOTAL_AMOUNT ==Int TOTAL_GAS *Int GAS_PRICE
; TODO: Can this be inferred by z3 by adding lemmas about #gas?
@@ -282,7 +282,7 @@ module VERIFICATION

rule I1 *Int A +Int I2 *Int A => (I1 +Int I2) *Int A

rule I1 *Int A +Int B +Int C +Int I2 *Int A => (I1 +Int I2) *Int A +Int B +Int C
rule I1 *Int A +Int B +Int C +Int D +Int I2 *Int A => (I1 +Int I2) *Int A +Int B +Int C +Int D

// TODO: move to builtin
rule N -Int N => 0
@@ -318,9 +318,19 @@ module VERIFICATION
// Gnosis
// ########################

// TODO: Replace with actual constraint
syntax Bool ::= "#checkSigsSuccess" [function]
// ----------------------------------------------
// checkSignatures is only called once in the executeTransaction, we implicitly assumed the arguments of the following functions
// have additional arguments of checkSignatures.
syntax Bool ::= "#enoughValidSigs" [function]
// ---------------------------------------------

syntax Int ::= "#checkSigsGasNonMem" [function]
// ------------------------------------------------

syntax Int ::= #checkSigsFinalMemUsed ( Int ) [function] // previous memory used
// ----------------------------------------------------------------------------------

syntax Int ::= "#checkSigsNextLoc" [function, smtlib(checkSigsNextLoc)] // previous memory used
// -------------------------------------------------------------------------------------------------

syntax Int ::= #loopGas ( Int , Int ) [function] // startPC, endPC
// --------------------------------------------------------------------

0 comments on commit 50259d2

Please sign in to comment.