# sailfish

https://github.com/ucsb-seclab/sailfish

Используется ANGELIC-FLAG для построения модели, которая потом проверяется на SAT

reentrancy.sol интерпретирует путь исполнения, собирая value summary analysis для переменных. После этого, используя наложенные ограниченияна перменные, строится математическая модель и производится её решение.

Функции:
- do-solve(json-obj) - solver, принимает на вход загруженный symex_path.json
- interpret-path(i-scope, i-dest-daddrs, i-entry-daddr, attack?) - принимает scope, адрес назначения и адрес входа (в формате machine-get-saddr) и флаг атаки. Последовательно выполняет блоки начиная с точки входа и до точек выхода.
- machine-get-saddr(r-addr, r-scope) - r-addr@r-scope, преобразует относительные адреса в другой формат
- reg-make-type(r-name, r-type) - создаёт переменную с нужной структурой и сохраняет в register-hash
- interpret-block(i-scope, i-insts, dest?, attack?) - принимает scope, список инструкций, флаг назначения и атаки. Выполняет блок и возвращает адрес следующего блока.
- parse-code - строка инструкции преобразуется в структуру
- interpret-inst(i-scope, i-inst, attack?) - интерпретация инструкции

Глобальные объекты:
- block-hash - Хранилище для блоков - хранит в себе блоки инструкций
- register-hash - Хранилище для регистров - хранит в себе перменные, ANGELIC-FLAG

Последовательность вызова при обработке (single_function_malicious.sol):

flowchart TD
    Start[/Start/] 
    --> load_json(Загрузка JSON объекта из файла)
    -.-> do-solve(["do-solve(json-obj)"])
    --> init_json_struct(Инициализация парсинга json)
    --> set_angelic_flag(ANGELIC-FLAG = True) 
    --> load_global(Загрузка глобальных блоков инструкций __GLOBAL__)
    --> load_global_var(Инициализация глобальных перменных)
    --> global_var_interpret("Для каждой переменной вызывается interpret-path")
    -.-> interpret_path_start
    global_var_interpret
    
    subgraph interpret_block
        direction TB
        interpret_block_start[["interpret-block(i-scope, i-insts, dest?, attack?)"]]
        --> angelic_if_dest(Если dest? == True, ANGELIC-FLAG = True)
    end
    
    subgraph interpret_path
        direction TB
        interpret_path_start[["interpret-path(i-scope, i-dest-daddrs, i-entry-daddr, attack?)"]]
        --> check_entry{{Точка входа - пустая?}}
        -->|Да|interpret_path_fin(Конец функции)
        check_entry -->|Нет|interpret_2("Вызвать interpret-block() для точки входа, если текущий блок - одна из точек выхода, задать dest? = True")
        --> interpret_next{{interpret-block вернул адреса следующего блока?}}
        -->|Да|interpret_rec(Вызываем interpret-path для следующего блока) -.-> interpret_path_start
        interpret_next -->|Нет|interpret_path_fin
        interpret_2 -.-> interpret_block_start
    end
    

## Пометки
global vars:

json-global-vars => (
#hasheq((init . ()) (name . "block") (type . ("struct_block"))) 
#hasheq((init . ("0x6")) (name . "msg") (type . ("struct_msg"))) 
#hasheq((init . ()) (name . "now") (type . ("integer"))) 
#hasheq((init . ()) (name . "tx") (type . ("struct_tx"))) 
#hasheq((init . ("0x7")) (name . "this") (type . ("struct_this"))) 
#hasheq((init . ("0x8")) (name . "msg_sender") (type . ("integer"))) 
#hasheq((init . ()) (name . "addmod") (type . ("function3"))) 
#hasheq((init . ()) (name . "mulmod") (type . ("function3"))) 
#hasheq((init . ()) (name . "keccak") (type . ("function1"))) 
#hasheq((init . ()) (name . "sha256") (type . ("function1"))) 
#hasheq((init . ()) (name . "sha3") (type . ("integer"))) 
#hasheq((init . ()) (name . "ripemd160") (type . ("function1"))) 
#hasheq((init . ()) (name . "ecrecover") (type . ("function4"))) 
#hasheq((init . ()) (name . "blockhash") (type . ("function1"))) 
#hasheq((init . ()) (name . "userBalance") (type . ("array" "integer" "integer"))) 
#hasheq((init . ()) (name . "Reentrancy") (type . ("integer")))
)

У глобальных переменных в JSON есть поле "init" - оно содержит номер глобального блока который инициализирует эту перменную

Инструкция в виде структуры:

msg.sender = 0x6

i-inst => #(struct:inst "struct-assign#rs-rm-li" #("msg" "sender" "0x6"))

u-type??

Final registers example:

#zhash(
("REF_5" . {[TMP_1$1 (ite TMP_1$1 0 userBalance#6$0)] [(! TMP_1$1) zvoid]})
("CLR_11" . balance$0) 
("CLR_7" . 6) 
("CLR_13" . {[TMP_1$1 userBalance#6$0] [(! TMP_1$1) zvoid]}) 
("WRP_0" . (+ balance$0 (- userBalance#6$0))) 
("block_timestamp_swap" . timestamp$0) 
("block" . #zhash(("number" . number$0) 
                  ("timestamp" . timestamp$0) 
                  ("difficulty" . difficulty$0) 
                  ("coinbase" . coinbase$0) 
                  ("gaslimit" . gaslimit$0))) 
("this" . #zhash(("address" . 5) 
                 ("balance" . (+ balance$0 (- userBalance#6$0))))) 
("now" . now$0) 
("CLR_12" . {[TMP_1$1 6] [(! TMP_1$1) zvoid]}) 
("tx" . #zhash(("gasprice" . gasprice$0) 
               ("origin" . origin$0))) 
("Reentrancy" . Reentrancy$0)
("CLR_9" . 6)
("msg_sender" . 4)
("CLR_14" . {[TMP_1$1 6] [(! TMP_1$1) zvoid]})
("sha3" . sha3$0)
("msg" . #zhash(("data" . data$0) 
                ("sig" . sig$0) 
                ("value" . value$0) 
                ("sender" . 6))) 
("CLR_10" . userBalance#6$0) 
("REF_4" . userBalance#6$0) 
("CLR_15" . {[TMP_1$1 6] [(! TMP_1$1) zvoid]}) 
("ANGELIC-FLAG" . TMP_1$1) 
("tmp_now" . tmp_now$0) 
("TMP_1" . TMP_1$1) 
("TMP_3" . {[TMP_1$1 zvoid] [(! TMP_1$1) TMP_3$0]}) 
("tmp_block_timestamp" . tmp_block_timestamp$0) 
("msg_value_swap" . value$0) 
("tmp_msg_value" . tmp_msg_value$0) 
("userBalance" . (vector
                     userBalance#0$0
                     userBalance#1$0
                     userBalance#2$0
                     userBalance#3$0
                     userBalance#4$0
                     userBalance#5$0
                     (ite TMP_1$1 0 userBalance#6$0)
                     userBalance#7$0
                     userBalance#8$0
                     userBalance#9$0)) 
("CLR_16" . {[TMP_1$1 (ite TMP_1$1 0 userBalance#6$0)] [(! TMP_1$1) zvoid]})
("CLR_17" . {[TMP_1$1 6] [(! TMP_1$1) zvoid]})
("CLR_8" . userBalance#6$0) 
("now_swap" . now$0) 
("TMP_2" . (! TMP_1$1)))