From 630555963952921e48226a10308da2cee4d663a0 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Wed, 8 Jan 2025 21:59:01 +0400 Subject: [PATCH 1/3] Draft for the `allowCalls` implementation --- src/kontrol/kdist/cheatcodes.md | 144 ++++++++++++++++++++++++++++---- 1 file changed, 129 insertions(+), 15 deletions(-) diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index c7c4ffcc9..f38ce8c60 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -76,8 +76,14 @@ module FOUNDRY-CHEAT-CODES false + + + .Account + .List + false + + false - .List .List @@ -963,19 +969,42 @@ We define two new status codes: The `ACCTTO` value is checked for each call while the whitelist restriction is enabled for calls. If the address is not in the whitelist `WLIST` then `KEVM` goes into an error state providing the `ACCTTO` value. -```k +// ```k +// rule [foundry.catchNonWhitelistedCalls]: +// (#call _ ACCTTO _ _ _ _ false +// ~> #popCallStack +// ~> #popWorldState) => #end KONTROL_WHITELISTCALL ... +// +// true +// WLIST +// ... +// +// requires notBool ACCTTO in WLIST +// [priority(40)] +// ``` + rule [foundry.catchNonWhitelistedCalls]: - (#call _ ACCTTO _ _ _ _ false + (#call _ ACCTTO _ _ _ CALLDATA false ~> #popCallStack ~> #popWorldState) => #end KONTROL_WHITELISTCALL ... true - WLIST + + + ACCTTO + ALLOWEDLIST + ALLOWALL + + ... + ... - requires notBool ACCTTO in WLIST + requires notBool ( + ALLOWALL + or + ListItem(CALLDATA) in ALLOWEDLIST + ) [priority(40)] -``` When the storage whitelist restriction is enabled, the `SSTORE` operation will check if the address and the storage index are in the whitelist. If the pair is not present in the whitelist `WLIST` then `KEVM` goes into an error state providing the address and the storage index values. @@ -1003,9 +1032,32 @@ function allowCallsToAddress(address) external; Adds an account address to the whitelist. The execution of the modified KEVM will stop when a call has been made to an address which is not in the whitelist. ```k - rule [foundry.allowCallsToAddress]: - #cheatcode_call SELECTOR ARGS => #loadAccount #asWord(ARGS) ~> #addAddressToWhitelist #asWord(ARGS) ... - requires SELECTOR ==Int selector ( "allowCallsToAddress(address)" ) + rule [foundry.allowAllCallsToAddress]: + #cheatcode_call SELECTOR ARGS + => #loadAccount #asWord(ARGS) + ~> #setAllowedAllCalls #asWord(ARGS) ... + requires SELECTOR ==Int selector("allowCallsToAddress(address)") +``` + +#### `allowCalls` - Add an account address and calldata prefix to a whitelist. + +``` +function allowCalls(address, bytes calldata data) external; +``` + +Adds an account address and calldata prefix to the whitelist. The execution of the modified KEVM will stop when a call has been made to an address and/or with calldata which are not in the whitelist. + +```k + rule [foundry.allowCalls]: + #cheatcode_call SELECTOR ARGS + => #loadAccount #asWord(#range(ARGS, 0, 32)) + ~> #etchAccountIfEmpty #asWord(#range(ARGS, 0, 32)) + ~> #setAllowedCall + #asWord(#range(ARGS, 0, 32)) + #range(ARGS, #asWord(#range(ARGS, 32, 32)) +Int 32, #asWord(#range(ARGS, #asWord(#range(ARGS, 32, 32)), 32))) + ... + + requires SELECTOR ==Int selector ( "allowCalls(address,bytes)" ) ``` #### `allowChangesToStorage` - Add an account address and a storage slot to a whitelist. @@ -1593,12 +1645,12 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa ```k syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)] // ------------------------------------------------------------------------------------- - rule #addAddressToWhitelist ACCT => .K ... - - _ => true - WLIST => WLIST ListItem(ACCT) - ... - + // rule #addAddressToWhitelist ACCT => .K ... + // + // _ => true + // WLIST => WLIST ListItem(ACCT) + // ... + // ``` - `#addStorageSlotToWhitelist` enables the whitelist restriction for storage chagnes and adds a `StorageSlot` item to the whitelist. @@ -1632,6 +1684,67 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa rule #etchAccountIfEmpty _ => .K ... [owise] ``` +- `#setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA` will update the `` mapping for the given account. + +```k + syntax KItem ::= "#setAllowedCall" Account Bytes [symbol(foundry_setAllowedCall)] + syntax KItem ::= "#setAllowedAllCalls" Account [symbol(foundry_setAllowedAllCalls)] + // --------------------------------------------------------------------------------- + rule #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ... + + _ => true + + ALLOWEDACCOUNT + CALLDATALIST => CALLDATALIST ListItem(ALLOWEDCALLDATA) + _ => false + + ... + + + rule #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ... + + _ => true + + ( .Bag + => + ALLOWEDACCOUNT + ListItem(ALLOWEDCALLDATA) + false + + ) + ... + + ... + + + rule #setAllowedAllCalls ALLOWEDACCOUNT => .K ... + + _ => true + + ALLOWEDACCOUNT + _ => .List + _ => true + + ... + + + rule #setAllowedAllCalls ALLOWEDACCOUNT => .K ... + + _ => true + + ( .Bag + => + ALLOWEDACCOUNT + .List + true + + ) + ... + + ... + +``` + - `#setMockCall MOCKADDRESS MOCKCALLDATA MOCKRETURN` will update the `` mapping for the given account. ```k @@ -1745,6 +1858,7 @@ Selectors for **implemented** cheat code functions. rule ( selector ( "prank(address)" ) => 3395723175 ) rule ( selector ( "prank(address,address)" ) => 1206193358 ) rule ( selector ( "allowCallsToAddress(address)" ) => 1850795572 ) + rule ( selector ( "allowCalls(address,bytes)" ) => 1808051021 ) rule ( selector ( "allowChangesToStorage(address,uint256)" ) => 4207417100 ) rule ( selector ( "infiniteGas()" ) => 3986649939 ) rule ( selector ( "setGas(uint256)" ) => 3713137314 ) From 6f33d5382a03d16ff90d6f9c5dababa79198201f Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 10 Jan 2025 16:49:11 +0400 Subject: [PATCH 2/3] Make `AllowedCallCellMap` empty in init cterm --- src/kontrol/prove.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index a9169b5a1..61b9229b6 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1040,6 +1040,7 @@ def _init_cterm( 'ISSTORAGEWHITELISTACTIVE_CELL': FALSE, 'ADDRESSLIST_CELL': list_empty(), 'STORAGESLOTLIST_CELL': list_empty(), + 'ALLOWEDCALLS_CELL': KApply('.AllowedCallCellMap'), 'MOCKCALLS_CELL': KApply('.MockCallCellMap'), 'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'), 'ACTIVETRACING_CELL': TRUE if trace_options.active_tracing else FALSE, From f4a75d78be5efd087c07283d56a3784bd3b8d329 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 10 Jan 2025 20:45:20 +0400 Subject: [PATCH 3/3] `allowedCallsList` refactoring, add `allowedAllCalls` --- src/kontrol/kdist/cheatcodes.md | 96 ++++++--------------------------- src/kontrol/prove.py | 2 +- 2 files changed, 16 insertions(+), 82 deletions(-) diff --git a/src/kontrol/kdist/cheatcodes.md b/src/kontrol/kdist/cheatcodes.md index f38ce8c60..f7137c421 100644 --- a/src/kontrol/kdist/cheatcodes.md +++ b/src/kontrol/kdist/cheatcodes.md @@ -76,13 +76,7 @@ module FOUNDRY-CHEAT-CODES false - - - .Account - .List - false - - + .List false .List @@ -952,6 +946,7 @@ A `StorageSlot` pair is formed from an address and a storage index. ```k syntax StorageSlot ::= "{" Int "|" Int "}" + syntax CallToAddress ::= "{" Int "|" Bytes "}" // ------------------------------------------ ``` @@ -969,42 +964,21 @@ We define two new status codes: The `ACCTTO` value is checked for each call while the whitelist restriction is enabled for calls. If the address is not in the whitelist `WLIST` then `KEVM` goes into an error state providing the `ACCTTO` value. -// ```k -// rule [foundry.catchNonWhitelistedCalls]: -// (#call _ ACCTTO _ _ _ _ false -// ~> #popCallStack -// ~> #popWorldState) => #end KONTROL_WHITELISTCALL ... -// -// true -// WLIST -// ... -// -// requires notBool ACCTTO in WLIST -// [priority(40)] -// ``` - +```k rule [foundry.catchNonWhitelistedCalls]: - (#call _ ACCTTO _ _ _ CALLDATA false + #call _ ACCTTO _ _ _ CALLDATA false + /* ~> #popCallStack - ~> #popWorldState) => #end KONTROL_WHITELISTCALL ... + ~> #popWorldState) + */ => #end KONTROL_WHITELISTCALL ... true - - - ACCTTO - ALLOWEDLIST - ALLOWALL - - ... - + WLIST ... - requires notBool ( - ALLOWALL - or - ListItem(CALLDATA) in ALLOWEDLIST - ) + requires notBool ({ACCTTO|CALLDATA} in WLIST orBool {ACCTTO|b"*"} in WLIST) [priority(40)] +``` When the storage whitelist restriction is enabled, the `SSTORE` operation will check if the address and the storage index are in the whitelist. If the pair is not present in the whitelist `WLIST` then `KEVM` goes into an error state providing the address and the storage index values. @@ -1643,7 +1617,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa - `#addAddressToWhitelist` enables the whitelist restriction for calls and adds an address to the whitelist. ```k - syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)] + // syntax KItem ::= "#addAddressToWhitelist" Int [symbol(foundry_addAddressToWhitelist)] // ------------------------------------------------------------------------------------- // rule #addAddressToWhitelist ACCT => .K ... // @@ -1684,7 +1658,7 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa rule #etchAccountIfEmpty _ => .K ... [owise] ``` -- `#setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA` will update the `` mapping for the given account. +- `#setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA` and `setAllowedAllCalls ALLOWEDACCOUNT` will update the `` list with the given account and calldata. ```k syntax KItem ::= "#setAllowedCall" Account Bytes [symbol(foundry_setAllowedCall)] @@ -1693,54 +1667,14 @@ If the flag is false, it skips comparison, assuming success; otherwise, it compa rule #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ... _ => true - - ALLOWEDACCOUNT - CALLDATALIST => CALLDATALIST ListItem(ALLOWEDCALLDATA) - _ => false - - ... - - - rule #setAllowedCall ALLOWEDACCOUNT ALLOWEDCALLDATA => .K ... - - _ => true - - ( .Bag - => - ALLOWEDACCOUNT - ListItem(ALLOWEDCALLDATA) - false - - ) + ALLOWEDCALLS => ALLOWEDCALLS ListItem({ALLOWEDACCOUNT|ALLOWEDCALLDATA}) ... - - ... - + rule #setAllowedAllCalls ALLOWEDACCOUNT => .K ... _ => true - - ALLOWEDACCOUNT - _ => .List - _ => true - - ... - - - rule #setAllowedAllCalls ALLOWEDACCOUNT => .K ... - - _ => true - - ( .Bag - => - ALLOWEDACCOUNT - .List - true - - ) - ... - + ALLOWEDCALLS => ALLOWEDCALLS ListItem({ALLOWEDACCOUNT|b"*"}) ... ``` diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 61b9229b6..f95707bf6 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1040,7 +1040,7 @@ def _init_cterm( 'ISSTORAGEWHITELISTACTIVE_CELL': FALSE, 'ADDRESSLIST_CELL': list_empty(), 'STORAGESLOTLIST_CELL': list_empty(), - 'ALLOWEDCALLS_CELL': KApply('.AllowedCallCellMap'), + 'ALLOWEDCALLSLIST_CELL': list_empty(), 'MOCKCALLS_CELL': KApply('.MockCallCellMap'), 'MOCKFUNCTIONS_CELL': KApply('.MockFunctionCellMap'), 'ACTIVETRACING_CELL': TRUE if trace_options.active_tracing else FALSE,