Skip to content

Commit

Permalink
Delete useGas cell (#4)
Browse files Browse the repository at this point in the history 
Having this cell in the configuration provides a ripe target for buffer
overflows, which might attempt to set the value of the useGas cell to
false in order to obtain free computation. We are not planning on ever
using it with a value of false, so we delete it.
  • Loading branch information
Dwight Guth authored Apr 11, 2024
1 parent d547f10 commit b758bd2
Show file tree
Hide file tree
Showing 12 changed files with 30 additions and 92 deletions.
3 changes: 1 addition & 2 deletions kevm-pyk/src/kevm_pyk/gst_to_kore.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
from typing import TYPE_CHECKING

from pyk.cli.utils import file_path
from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer
from pyk.kore.prelude import INT, SORT_JSON, SORT_K_ITEM, inj, int_dv, json_to_kore, top_cell_initializer
from pyk.kore.syntax import App, SortApp

from .cli import KEVMCLIArgs
Expand Down Expand Up @@ -39,7 +39,6 @@ def kore_pgm_to_kore(pgm: Pattern, pattern_sort: SortApp, schedule: str, mode: s
'$SCHEDULE': inj(SORT_SCHEDULE, SORT_K_ITEM, _schedule_to_kore(schedule)),
'$MODE': inj(SORT_MODE, SORT_K_ITEM, _mode_to_kore(mode)),
'$CHAINID': inj(INT, SORT_K_ITEM, int_dv(chainid)),
'$USEGAS': inj(BOOL, SORT_K_ITEM, bool_dv(usegas)),
}
return top_cell_initializer(config)

Expand Down
2 changes: 0 additions & 2 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,8 +301,6 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule <k> loadCallState { "code" : (CODE:OpCodes), REST } => #loadProgram #asmOpCodes(CODE) ~> loadCallState { REST } ... </k>
rule <k> loadCallState { "usegas" : (USEGAS:Bool), REST => REST } ... </k> <useGas> _ => USEGAS </useGas>
rule <k> loadCallState { KEY : ((VAL:String) => #parseWord(VAL)), _ } ... </k>
requires KEY in (SetItem("gas") SetItem("gasPrice") SetItem("value"))
Expand Down
33 changes: 7 additions & 26 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,6 @@ In the comments next to each cell, we've marked which component of the YellowPap
<exit-code exit=""> 1 </exit-code>
<mode> $MODE:Mode </mode>
<schedule> $SCHEDULE:Schedule </schedule>
<useGas> $USEGAS:Bool </useGas>
<ethereum>
Expand Down Expand Up @@ -552,7 +551,6 @@ After executing a transaction, it's necessary to have the effect of the substate
<accessedStorage> _ => .Map </accessedStorage>
rule <k> #finalizeTx(false) ... </k>
<useGas> true </useGas>
<schedule> SCHED </schedule>
<gas> GAVAIL => G*(GAVAIL, GLIMIT, REFUND, SCHED) </gas>
<refund> REFUND => 0 </refund>
Expand All @@ -565,7 +563,6 @@ After executing a transaction, it's necessary to have the effect of the substate
requires REFUND =/=Int 0
rule <k> #finalizeTx(false => true) ... </k>
<useGas> true </useGas>
<baseFee> BFEE </baseFee>
<origin> ORG </origin>
<coinbase> MINER </coinbase>
Expand All @@ -592,7 +589,6 @@ After executing a transaction, it's necessary to have the effect of the substate
requires ORG =/=Int MINER
rule <k> #finalizeTx(false => true) ... </k>
<useGas> true </useGas>
<baseFee> BFEE </baseFee>
<origin> ACCT </origin>
<coinbase> ACCT </coinbase>
Expand All @@ -612,14 +608,6 @@ After executing a transaction, it's necessary to have the effect of the substate
...
</message>
rule <k> #finalizeTx(false => true) ... </k>
<useGas> false </useGas>
<txPending> ListItem(MsgId:Int) REST => REST </txPending>
<message>
<msgID> MsgId </msgID>
...
</message>
rule <k> (.K => #deleteAccounts(Set2List(ACCTS))) ~> #finalizeTx(true) ... </k>
<selfDestruct> ACCTS => .Set </selfDestruct>
requires size(ACCTS) >Int 0
Expand Down Expand Up @@ -1319,13 +1307,12 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram BYTES ~> #initVM ~> #precompiled?(ACCTCODE, SCHED) ~> #execute
...
</k>
<useGas> USEGAS:Bool </useGas>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => ARGS </callData>
<callValue> _ => APPVALUE </callValue>
<id> _ => ACCTTO </id>
<gas> GAVAIL:Gas => #if USEGAS #then GCALL:Gas #else GAVAIL:Gas #fi </gas>
<callGas> GCALL:Gas => #if USEGAS #then 0:Gas #else GCALL:Gas #fi </callGas>
<gas> GAVAIL:Gas => GCALL:Gas </gas>
<callGas> GCALL:Gas => 0:Gas </callGas>
<caller> _ => ACCTFROM </caller>
<static> OLDSTATIC:Bool => OLDSTATIC orBool STATIC </static>
<schedule> SCHED </schedule>
Expand Down Expand Up @@ -1446,8 +1433,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
syntax InternalOp ::= "#refund" Gas
| "#setLocalMem" Int Int Bytes
// --------------------------------------------------
rule [refund]: <k> #refund G:Gas => .K ... </k> <gas> GAVAIL => GAVAIL +Gas G </gas> <useGas> true </useGas>
rule [refund.noGas]: <k> #refund _ => .K ... </k> <useGas> false </useGas>
rule [refund]: <k> #refund G:Gas => .K ... </k> <gas> GAVAIL => GAVAIL +Gas G </gas>
rule <k> #setLocalMem START WIDTH WS => .K ... </k>
Expand Down Expand Up @@ -1543,11 +1529,10 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
=> #touchAccounts ACCTFROM ACCTTO ~> #accessAccounts ACCTFROM ACCTTO ~> #loadProgram INITCODE ~> #initVM ~> #execute
...
</k>
<useGas> USEGAS </useGas>
<schedule> SCHED </schedule>
<id> _ => ACCTTO </id>
<gas> GAVAIL => #if USEGAS #then GCALL #else GAVAIL #fi </gas>
<callGas> GCALL => #if USEGAS #then 0 #else GCALL #fi </callGas>
<gas> GAVAIL => GCALL </gas>
<callGas> GCALL => 0 </callGas>
<caller> _ => ACCTFROM </caller>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => .Bytes </callData>
Expand Down Expand Up @@ -1899,9 +1884,6 @@ Overall Gas
~> #access [ OP , AOP ]
...
</k>
<useGas> true </useGas>
rule <k> #gas [ _ , _ ] => .K ... </k> <useGas> false </useGas>
rule <k> #gas [ OP ] => #gasExec(SCHED, OP) ~> #deductGas ... </k>
<schedule> SCHED </schedule>
Expand All @@ -1919,9 +1901,8 @@ Overall Gas
<memoryUsed> MU => MU' </memoryUsed> <schedule> SCHED </schedule>
rule <k> _G:Gas ~> (#deductMemoryGas => #deductGas) ... </k> //Required for verification
rule <k> G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL:Gas </gas> <useGas> true </useGas> requires GAVAIL <Gas G
rule <k> G:Gas ~> #deductGas => .K ... </k> <gas> GAVAIL:Gas => GAVAIL -Gas G </gas> <useGas> true </useGas> requires G <=Gas GAVAIL
rule <k> _:Gas ~> #deductGas => .K ... </k> <useGas> false </useGas>
rule <k> G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL:Gas </gas> requires GAVAIL <Gas G
rule <k> G:Gas ~> #deductGas => .K ... </k> <gas> GAVAIL:Gas => GAVAIL -Gas G </gas> requires G <=Gas GAVAIL
syntax Bool ::= #inStorage ( Map , Account , Int ) [klabel(#inStorage), function, total]
| #inStorageAux1 ( KItem , Int ) [klabel(#inStorageAux1), function, total]
Expand Down
63 changes: 18 additions & 45 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -43,7 +40,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => ( #if USEGAS #then ( GAVAIL -Gas Gbase < SCHED > ) #else GAVAIL #fi ) )
( GAVAIL => ( ( GAVAIL -Gas Gbase < SCHED > ) ) )
</gas>
...
</callState>
Expand All @@ -53,7 +50,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gbase < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gbase < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( 0 : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -65,9 +62,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -81,7 +75,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( ( PCOUNT +Int N ) +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -91,7 +85,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -103,9 +97,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -116,7 +107,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -127,7 +118,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires #stackNeeded(DUP(N)) <=Int #sizeWordStack(WS)
andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -139,9 +130,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -152,7 +140,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -163,7 +151,7 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires #stackNeeded(SWAP(N)) <=Int #sizeWordStack(W0 : WS)
andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) ) <=Int 1024 )
[priority(40)]
Expand All @@ -175,9 +163,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -188,7 +173,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -198,7 +183,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( chop( ( W0 +Int W1 ) ) : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -210,9 +195,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -223,7 +205,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -233,7 +215,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( chop( ( W0 -Int W1 ) ) : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -245,9 +227,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -258,7 +237,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -268,7 +247,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( W0 &Int W1 : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -280,9 +259,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -293,7 +269,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -303,7 +279,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( bool2Word( W0 <Int W1 ) : WS ) <=Int 1024 )
[priority(40)]
Expand All @@ -315,9 +291,6 @@ module EVM-OPTIMIZATIONS
<schedule>
SCHED
</schedule>
<useGas>
USEGAS
</useGas>
<ethereum>
<evm>
<callState>
Expand All @@ -328,7 +301,7 @@ module EVM-OPTIMIZATIONS
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
<gas>
( GAVAIL => #if USEGAS #then ( GAVAIL -Gas Gverylow < SCHED > ) #else GAVAIL #fi )
( GAVAIL => ( GAVAIL -Gas Gverylow < SCHED > ) )
</gas>
...
</callState>
Expand All @@ -338,7 +311,7 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
requires ( Gverylow < SCHED > <=Gas GAVAIL )
andBool ( #sizeWordStack( bool2Word( W1 <Int W0 ) : WS ) <=Int 1024 )
[priority(40)]
Expand Down
3 changes: 1 addition & 2 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,8 +150,7 @@ Here we load the environmental information.
rule <k> loadCallState { "code" : CODE:Bytes, REST } => #loadProgram CODE ~> loadCallState { REST } ... </k>
rule <k> loadCallState { "gas" : GLIMIT:Int, REST => REST } ... </k> <gas> _ => GLIMIT </gas> <useGas> true </useGas>
rule <k> loadCallState { "gas" : _:Int, REST => REST } ... </k> <useGas> false </useGas>
rule <k> loadCallState { "gas" : GLIMIT:Int, REST => REST } ... </k> <gas> _ => GLIMIT </gas>
rule <k> loadCallState { "gasPrice" : GPRICE:Int, REST => REST } ... </k> <gasPrice> _ => GPRICE </gasPrice>
rule <k> loadCallState { "value" : VALUE:Int , REST => REST } ... </k> <callValue> _ => VALUE </callValue>
Expand Down
Loading

0 comments on commit b758bd2

Please sign in to comment.