Permalink
Browse files

checkSignatures-v0 failure and exception cases

  • Loading branch information...
yzhang90 committed Jan 10, 2019
1 parent f3391eb commit 83f9e1971d436c62e7a8a9520cbf2775b848a61e
Showing with 90 additions and 1 deletion.
  1. +12 −0 gnosis-imap/Makefile
  2. +75 −0 gnosis-imap/gnosis-imap-spec.ini
  3. +1 −1 gnosis/abstract-semantics.k
  4. +2 −0 gnosis/verification.k
@@ -28,12 +28,15 @@ SPEC_NAMES_GNOSIS_SAFE:=encodeTransactionData-public-1 \
checkSignatures-loop-body-success-v0 \
checkSignatures-loop-body-success-v1-owner \
checkSignatures-loop-body-success-v1-not-owner \
checkSignatures-loop-body-failure-v0-1 \
checkSignatures-loop-body-failure-v0-2 \
checkSignatures-loop-body-failure-v1-owner \
checkSignatures-loop-body-failure-v1-not-owner-approved \
checkSignatures-loop-body-failure-v1-not-owner-not-approved \
checkSignatures-loop-body-success-v_else \
checkSignatures-loop-body-failure-v_else-ecrecEmpty \
checkSignatures-loop-body-failure-v_else-not-ecrecEmpty \
checkSignatures-loop-body-exception-v0 \
execTransaction-checkSigs1-gas1-safetxgas0-gasprice0-call1-to \
execTransaction-checkSigs1-gas1-safetxgas1-call1-to-gasprice1-send1-origin

@@ -118,6 +121,12 @@ $(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-success-v1-owner-spec.k: $(
$(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-success-v1-not-owner-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) checkSignatures-loop-body-success-v1-not-owner signatureSplit-trusted checkSignatures-loop-body-success-v1-not-owner > $@

$(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-failure-v0-1-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) checkSignatures-loop-body-failure-v0-1 signatureSplit-trusted copy-trusted-data copy-trusted-contractSig checkSignatures-loop-body-failure-v0-1 > $@

$(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-failure-v0-2-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) checkSignatures-loop-body-failure-v0-2 signatureSplit-trusted copy-trusted-data copy-trusted-contractSig checkSignatures-loop-body-failure-v0-2 > $@

$(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-failure-v1-owner-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) checkSignatures-loop-body-failure-v1-owner signatureSplit-trusted checkSignatures-loop-body-failure-v1-owner > $@

@@ -135,3 +144,6 @@ $(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-failure-v_else-ecrecEmpty-s

$(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-failure-v_else-not-ecrecEmpty-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) checkSignatures-loop-body-failure-v_else-not-ecrecEmpty signatureSplit-trusted checkSignatures-loop-body-failure-v_else-not-ecrecEmpty > $@

$(SPECS_DIR)/$(SPEC_GROUP)/checkSignatures-loop-body-exception-v0-spec.k: $(TMPLS) $(SPEC_INI)
python3 $(RESOURCES)/gen-spec.py $(TMPLS) $(SPEC_INI) checkSignatures-loop-body-exception-v0 signatureSplit-trusted copy-trusted-data copy-trusted-contractSig checkSignatures-loop-body-exception-v0 > $@
@@ -928,6 +928,46 @@ pc: {PC_LOOP_HEAD} +Int 1 => {PC_FUN_END}
EVAL: false
attribute: [trusted, matching(#gas,storeRange,#buf)]

[checkSignatures-loop-body-failure-v0]
+requires:
; v == 0
andBool #sigV({SIGS_BUF}, I) ==Int 0
andBool #rangeUInt(256, #sigS({SIGS_BUF}, I))
andBool #rangeUInt(256, SIGS_LOC +Int #sigS({SIGS_BUF}, I))
; TODO: what if SIGS_LOC +Int S_I +Int 32 overflows? It will read content before the content of signature.
andBool #rangeUInt(256, {DYNAMIC_START})
; read CONTRACT_SIG_LEN
andBool SIGS_LOC +Int 32 <=Int {DYNAMIC_START}
andBool {DYNAMIC_START} +Int 32 <=Int SIGS_LOC +Int 32 +Int SIGS_LEN
; read CONTRACT_SIG
andBool SIGS_LOC +Int 32 <=Int {DYNAMIC_START} +Int 32
andBool {DYNAMIC_START} +Int 32 +Int {CONTRACT_SIG_LEN} <=Int SIGS_LOC +Int 32 +Int SIGS_LEN
; read 64
andBool 96 <Int NEXT_LOC +Int #ceil32(TX_DATA_LEN) +Int 132 +Int {CONTRACT_SIG_LEN}
; read TX_DATA_LEN
andBool TX_DATA_LOC +Int 32 <Int {TRAILING_ZERO_START}
; read TX_DATA
andBool TX_DATA_LOC +Int 32 +Int TX_DATA_LEN <Int {TRAILING_ZERO_START}
; read SIGS_LEN
andBool SIGS_LOC +Int 32 <Int {TRAILING_ZERO_START}
; read SIGS
andBool SIGS_LOC +Int 32 +Int SIGS_LEN <Int {TRAILING_ZERO_START}
andBool 0 <Int #extCodeSize({CURRENT_OWNER})
andBool #callSuccess(18677, {CURRENT_OWNER})
dynamic_start: SIGS_LOC +Int #sigS({SIGS_BUF}, I) +Int 32
contract_sig_len: #asWord(#bufSeg({SIGS_BUF}, #sigS({SIGS_BUF}, I), 32))
trailing_zero_start: NEXT_LOC +Int #ceil32(TX_DATA_LEN) +Int 132 +Int {CONTRACT_SIG_LEN}

[checkSignatures-loop-body-failure-v0-1]
+requires:
andBool #callResult(18677, {CURRENT_OWNER}) ==K 0

[checkSignatures-loop-body-failure-v0-2]
+requires:
andBool #callResult(18677, {CURRENT_OWNER}) ==K 1
andBool ( {CURRENT_OWNER} <=Int LAST_OWNER
orBool {INIT_CURRENT_OWNER} ==Int 0 )

[checkSignatures-loop-body-failure-v1]
+requires:
; v == 1
@@ -973,6 +1013,41 @@ refund: _ => _
andBool ( {CURRENT_OWNER} <=Int LAST_OWNER
orBool {INIT_CURRENT_OWNER} ==Int 0 )


[checkSignatures-loop-body-exception-v0]
k: (#execute => #halt) ~> _
statusCode: _ => EVMC_REVERT
WORD_STACK_RHS: _
pc: {PC_LOOP_HEAD} => 18693
+requires:
; v == 0
andBool #sigV({SIGS_BUF}, I) ==Int 0
andBool #rangeUInt(256, #sigS({SIGS_BUF}, I))
andBool #rangeUInt(256, SIGS_LOC +Int #sigS({SIGS_BUF}, I))
; TODO: what if SIGS_LOC +Int S_I +Int 32 overflows? It will read content before the content of signature.
andBool #rangeUInt(256, {DYNAMIC_START})
; read CONTRACT_SIG_LEN
andBool SIGS_LOC +Int 32 <=Int {DYNAMIC_START}
andBool {DYNAMIC_START} +Int 32 <=Int SIGS_LOC +Int 32 +Int SIGS_LEN
; read CONTRACT_SIG
andBool SIGS_LOC +Int 32 <=Int {DYNAMIC_START} +Int 32
andBool {DYNAMIC_START} +Int 32 +Int {CONTRACT_SIG_LEN} <=Int SIGS_LOC +Int 32 +Int SIGS_LEN
; read 64
andBool 96 <Int NEXT_LOC +Int #ceil32(TX_DATA_LEN) +Int 132 +Int {CONTRACT_SIG_LEN}
; read TX_DATA_LEN
andBool TX_DATA_LOC +Int 32 <Int {TRAILING_ZERO_START}
; read TX_DATA
andBool TX_DATA_LOC +Int 32 +Int TX_DATA_LEN <Int {TRAILING_ZERO_START}
; read SIGS_LEN
andBool SIGS_LOC +Int 32 <Int {TRAILING_ZERO_START}
; read SIGS
andBool SIGS_LOC +Int 32 +Int SIGS_LEN <Int {TRAILING_ZERO_START}
andBool 0 <Int #extCodeSize({CURRENT_OWNER})
andBool #callFailure(18677, {CURRENT_OWNER})
dynamic_start: SIGS_LOC +Int #sigS({SIGS_BUF}, I) +Int 32
contract_sig_len: #asWord(#bufSeg({SIGS_BUF}, #sigS({SIGS_BUF}, I), 32))
trailing_zero_start: NEXT_LOC +Int #ceil32(TX_DATA_LEN) +Int 132 +Int {CONTRACT_SIG_LEN}

[execTransaction]
k: (#execute => #halt) ~> _
callStack: _
@@ -106,7 +106,7 @@ module ABSTRACT-SEMANTICS
rule <k> #exec[CALL] => . ... </k>
<output> _ => _ </output>
<schedule> SCHED </schedule>
<wordStack> GASCAP : ACCTTO : VALUE : ARGSTART : ARGWIDTH : RETSTART : 0 : WS => 0 : WS </wordStack>
<wordStack> GASCAP : ACCTTO : VALUE : ARGSTART : ARGWIDTH : RETSTART : REWIDTH : WS => 0 : WS </wordStack>
<pc> PCC </pc>
<gas> #gas(INITGAS, NONMEM, MEM) => #gas(INITGAS, NONMEM +Int #callGas(SCHED, GASCAP, ACCTTO, VALUE, false), MEM) </gas>
<previousGas> _ => #gas(INITGAS, NONMEM, MEM) </previousGas>
@@ -163,6 +163,8 @@ module VERIFICATION

rule #sizeWordStack(selectRange(_, _, WIDTH), SIZE) => SIZE +Int WIDTH

rule #take(#sizeWordStack(WS, 0), WS) => WS


// ########################
// Range

0 comments on commit 83f9e19

Please sign in to comment.