# Solar reconstruction

[TOC]

Задачи:
- [x] Найти и определить работу функции суммаризации
- [x] Понять вывод vandal, который используется для анализа
- [x] Проверить vandal - правильный ли вывод генерируется
- [ ] Найти и определить функцию синтезации
- [ ] Понять и разработать parallel-eval

## Связь кода с статьей

Соляр предоставляет:
1. Язык запросов, с помощью которого можно выражать уязвимости. Например, запрос для reentrancy может выглядеть следующим образом:

2. Синтезатор атакующих контрактов по данному запросу.

Key ideas:
- attacker typically exploits the vulnerability by making a sequence of transitions
- storage states are preserved across different transitions
- summary of a method soundly models its side-effect over storage variables
- Solar models the executions of a smartcontract as state transitions over registers, memory, and storage

Glossary:
- CFG - control flow graph
- pc - program counter (index of current executable instruction of vm - smth like rip register)
- tod - TOD attack/ front-running
- dao - DAO attack

Атаки заявленные в solar:
- Reentrancy attack
- Time manipulation
- malicious access control
- Security Best Practices
- BatchOverflow Bug (CVE-2018–10299)

Другие инструменты которые реализуют symbolic execution:
- mythril https://github.com/ConsenSys/mythril
- oyente https://github.com/enzymefinance/oyente
- teEther https://github.com/nescio007/teether

Для уменьшения пространства поиска, с помощью rosette оно делится на небольшое количестов

Program state: stack, memory, persistent storage, global properties, pc, (gas)
State transition: Г:s -> Г':v , что значит если успешно выполнить s в состоянии Г, то получим состояние Г' и значение v

R - abstract execution trace (list of events in interest. event = type, list of attrbibutes)

$𝑠@𝜙$: s - изменение состояния, ф - условие при котором изменение будет выполнено

Как solar анализирует контракт:
1. Program -> Intermediate Language
2. Symbolically execute IL code to build trace

Summary construction:
1. 1. Evaluate the method on a program state $Γ_𝑆$ that maps every state variable (i.e., persistent storage location, global property, etc.) to a fresh symbolic variable of the right type.
2. Produce a path condition and symbolic inputs for each instruction that capture every possible way to reach and execute the instruction within the given method.
2. Generate summary using following algorithm:

При генерации summary учитываются только два вида инструкций - transfer и sstore, так как другие инструкции не имеют прямого влияния на state ($Г$)

Summary - сумма изменений state всех transfer и sstore для public метода

В статье solar представлен следуюшим образом:

V - a potential vulnerability expressed as a declarative
specification (expressed in Racket as a boolean predicate
over these state transitions)
Y - union of public methods
K - длина генерируемого эксплойта

> Пояснение насчёт choose*
> Symbolically chooses one of the provided values. The procedure creates n-1 fresh symbolic boolean constants every time it is evaluated, and uses these constants to conditionally select one of the n provided expressions.

Что происходит, по строчкам:
1. -
2. Генерируется набор всех эксплойт-программ (в символическом представлении), длинной K, состоящая из публичных методов контракта
3. Контракт-жертва инициализируется, получаем начальное состояние
4. Символическая эксплойт-программа выполняется на контракте (из изначального состояния), сохраняется полученное состояние
5. Производится поиск конкретного эксплойта соответстующего запросу V
6. -//-

Основные части solar:
1. _interpreter_ (solidity/solidity-interpret.rkt) - implements the semantics from the EVM yellow paper. Интерпретатор не реализует symbolic execution - используется движок символического исполнения rosette. Interpreter выполняет следующие функции:
1. compute the symbolic summaries of the victim’s public methods
2. evaluate symbolic attack programs
2. _translator_ (использует vandal или ./smart_opt). Выполняет следующие функции:
1. convert the stack-based EVM bytecode into its corresponding three-address format in our language

Параллелизм (parallel-driver.rkt? parallel-eval?):
Запрос solve (тяжелый и большой) делится на меньшие запросы, которые могут быть исполнены параллельно и быстро

Так как на 2 строке solar, количество генерируемых программ (при условии что аргументы - символиские) - $N^K$, где N - $|Y|$
Вместо того чтобы решать один запрос solve на 5 строке, мы можем запустить выполнение $N^K$ программ параллельно и убрать - !!! Уточнить на созвоне

### Что есть в коде (по статье):
Синтезация эксплойта: solidity/solidity-interpret.rkt (207-261)
check-intefere (проверка, вмешивается ли переменная в выражение): solidity/solidity-interpret.rkt (104-115)
Генерация суммаризации (инициализация анализатора): solidity/solidity-interpret.rkt (270-344)
Интерпретация суммаризации (выполнение символического представления суммаризации над состоянием): solidity/solidity-interpret.rkt (371-410)
Интерпретация программы (выполнение программы, т.е списка публичных методов, над состоянием): solidity/solidity-interpret.rkt (413-909)
Интерпретация программы (выполнение программы, т.е вектора объектов inst над состоянием): - пустая реализация
Измерение performance cost: - пустая реализация

Входная точка для анализа - init-analyzer
Нужно установить доп.флаги для выполнения:
1. (synth-mode #t) для синтезации атаки (по умолчанию #t)
2. (summary-mode #t) для использования суммаризации (по умолчани #f)

gen-summaries -> for each public method m do: progstate-summary(interpret-program(m))

interpret-program работает правильно, выдаёт состояние машины после интерпретации метода
interpret-program должен сразу создавать суммарзиацию, progstate-summary только извлекает поле summary из machine state

fix#7 не давал генерироваться summary для sstore - для исправления нужно найти pc (предположительно, pc - 0 аргумент)


---
## Доступный код solar:

### Python:

src/
    analysis/
        core_analysis.py
    vandal/
        blockparse.py
        cfg.py
        dataflow.py
        default_config.ini
        evm_cfg.py
        exporter.py
        function.py
        lattice.py
        memtypes.py
        opcodes.py
        patterns.py
        settings.py
        tac_cfg.py

eval_parallel.py - Invokes ./smartscopy in several processes
smart_opt - Vandal EVM Decompiler v0.0.3

### Тесты:

test/
    bin/
    ccs16/
    fuzz-timeout/
    sol/

### Racket:

solidity/
    main.rkt
    optimize.rkt
    solidity-enumerator.rkt
    solidity-interpret.rkt
    solidity-machine.rkt
    solidity-parser.rkt
    solidity-printer.rkt

enumerator.rkt
inst.rkt
machine.rkt - ABS Base class: machine
memory-racket.rkt
memory-rosette.rkt
ops-racket.rkt
ops-rosette.rkt
parser.rkt - define: struct inst, struct pointer, helper functions for random
printer.rkt
queue-racket.rkt
queue-rosette.rkt
simulator-racket.rkt - class: simulator-racket
simulator.rkt - ABS Base class: simulator
simulator-rosette.rkt - rosette, class: simulator-rosette
smartexe.rkt
special.rkt - define "special" type

### Классы:

@startuml
abstract class "simulator" {
    interpret()
    performance-cost()
    +get-constructor()
    +is-valid?()
}

class "simulator-rosette"
class "simulator-racket"

"simulator" <|-- "simulator-rosette"
"simulator" <|-- "simulator-racket"


abstract class "machine" {
    bitwidth
    random-input-bits
    config
    opcodes
    nop-id
    opcode-id-to-class
    classes-info
    argtypes-info
    statetypes-info
    groups-of-opcodes
    max-number-of-args
    vector2scalar
    opcode-pool
    
    progstate-structure()
    +define-instruction-class()
    
    +window-size()
    +get-config()
    +set-config(info)
    +get-opcode-id(opcode)
    +get-opcode-name(id)
    +no-assumption()
    +display-state(x)
    +progstate->vector(x)
    +vector->progstate(x)
    +parse-state-text(str)
    +clean-code(code, prefix)
    +state-eq?(state1, state2, pred)
    +get-state(init, concrete)
    +progstate()
    +inner(x)
    +clone-state(state)
    
    +init-machine-description(opcode-types)
    +define-instruction-class(name, class-opcodes, scalar, vector-width, args, ins, outs, commute, required)
    +check-max-number-of-args(args)
    +filter-statetype(locs, args)
    +all-opcodes-groups(opcodes-groups, args-groups, ins-groups, required)
    +all-opcodes-combinations(opcodes-groups)
    +define-progstate-type(name, get, set, min, max, const, structure)
    +define-arg-type(name, validfunc, progstate)
    +finalize-machine-description()
    +get-arg-range-of-type(type, live, vals)
    +analyze-args-inst(my-inst)
    +get-progstate-ins-outs(opcode-id)
    +get-progstate-at(state, locs, types, args)
}

class printer
class enumerator
class parser

class memory-racket
class memory-rosette

class queue-in-racket
class queue-out-racket

class queue-in-rosette
class queue-out-rosette


class solidity-printer


@enduml

---
### Файлы которых нет:

parallel-driver.rkt - required by solidity/main.rkt
solidity/
    solidity-simulator-racket.rkt - required by solidity/main.rkt
    solidity-simulator-rosette.rkt - required by solidity/main.rkt
    solidity-validator.rkt - required by solidity/main.rkt

### Заметки:
- solidity-simulator-rosette находится в solidity/solidity-interpret.rkt
- solidity-simulator-racket не используется

### Починка solar:
1. smart_opt

Traceback (most recent call last):
  File "/home/ucat/Research/solar/./smart_opt", line 13, in <module>
    import src.vandal.exporter as exporter
ModuleNotFoundError: No module named 'src.vandal'

fix:

touch src/__init__.py
touch src/vandal/__init__.py

2. smart_opt

Traceback (most recent call last):
  File "/home/ucat/Research/solar/./smart_opt", line 196, in <module>
    dataflow.analyse_graph(cfg)
  File "/home/ucat/Research/solar/src/vandal/dataflow.py", line 60, in analyse_graph
    start_clock = time.clock()
AttributeError: module 'time' has no attribute 'clock'

fix:
use python3.6

3. solar

solidity/solidity-interpret.rkt:229:29: gasless: unbound identifier

fix:
remove has-gasless? - not used

4. solar

solidity/solidity-interpret.rkt:231:46: cst: unbound identifier

fix:
- cst есть в комментах, два варианта. Расскоментируем с vul-access
- Вероятно cst контролирует вид атаки на который тестируется контракт

5. solar

solidity/solidity-interpret.rkt:238:46: has-gasless?: unbound identifier

fix:
Вернуть has-gasless, сделать чтобы он возвращал только True

6. solar

solidity/solidity-interpret.rkt:247:17: parallel-eval: unbound identifier

fix:
solidity-interpret.rkt использует parallel-eval
Реализовать parllel-eval самостоятельно

7. solar

solidity/solidity-interpret.rkt:574:79: pc: unbound identifier

fix:
pc ?? ipc ??
possibly one of the arguments - now only dirty fix

8. solar

smartexe.rkt:5:20: cannot open module file
  module path: rosette/query/debug

fix:
this module does not exists, remove file from imports

9. solar

boolector: boolector binary is not available

fix:

yay -S boolector

### Запуск solar:
- Предположительно точка входа - smartexe.rkt
smartexe.rkt запускает "./smart_opt argv[0]"

racket smartexe.rkt test/bin/reentrance.hex

### Запуск smart_opt - работает
An EVM bytecode disassembly decompiler that generates three-address code for program analysis. Use config.ini to set further configuration
options.

Читает байткод из входного файла (по умолчанию stdin), выдаёт Control flow graph в виде JSON

smart_opt использует vandal для построения CFG, после чего запускает анализ графа (CostAnalysis)

Формат данных:
Публичная функция представляется в формате 0xAA-B, AA - адрес начальной инструкции, B - количество аргументов

### Проверка vandal

test/bin/reentrance.hex

Публичные методы которые нашёл vandal:

Методы которые есть в исходнике:

mapping(address => uint) public balances
function donate(address _to) public payable
function balanceOf(address _who) public constant returns (uint balance)
function withdraw(uint _amount) public
function() payable

Т.е. вандал нашёл один лишний метод с одним аргументом

Проверим методы которые он нашёл:
1. 0x63-1 = donate(address _to)

decompiler:

Блок продолжается до 0x174, где происходят присвоения с использованием keccak256

2. 0xa5-1 = balanceOf(address _who)

jump to 0x1c3, return data from storage

3. 0xfc-1 = withdraw(uint _amount)


jump to 0x1db, check if `storage[addr] < argument`, if not -> jump to 0x29c (return), else -> jump 0x223
0x223 -> call `addr` with `arg` eth, change `storage[addr] = storage[addr] - arg`

4. 0x129-1 = mapping balances
5. 0x61-0 = not a function, stop() if no func found by signature

### Генерация суммаризации

sstore, sload, call - три инструкции которые учитываются при анализе

#### jumpi

При интерпретации jumpi интерепретируются блоки pos-succ (условие выполнено) и neg-succ (условие не выполнено)

#### call

Происходит проверка вмешательства (check interfere) с различными перменными storage
По какой-то причине после обработки call анализ блока прерывается. Ниже по блоку происходит работа с storage. т.к. Блок не обработан до конца -> суммаризация функции не генерируется

### parallel-eval
sketch = parallel-eval
query-model sketch ? not uses sketch

get-item method->expr sketch

method->expr is table to translate from (bv method repr) to (struct bv method + args)

get-item - search for a list with first element equal to key in table

# tmp

(&& 
  (! 
    (bveq 
      (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) 
    (bvand 
      (bv #x00000000000000000000000000000000000000000000000000000000000000ff 256) store-var$0))) 
  (! (bveq 
  (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) ...)))

(list
 "summaries:"
 (hash
  (bv #x04 8)
  '()
  
  (bv #x0b 8)
  (list
   (cons
    (bv #x0000000000000000000000000000000000000000000000000000000000000271 256)
    (store-sum
     (bv #x0000000000000000000000000000000000000000000000000000000000000000 256)
     (bvor (ite (bveq (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) arg$3) (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) (bv #x0000000000000000000000000000000000000000000000000000000000000001 256)) (bvand ...)))))
     
  (bv #x0f 8)
  (list
   (cons
    (bv #x00000000000000000000000000000000000000000000000000000000000002b8 256)
    (store-sum
     (app sha3-app (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) (bv #x0000000000000000000000000000000000000000000000000000000000000040 256))
     arg$4)))
     
  (bv #x07 8)
  (list
   (cons
    (bv #x00000000000000000000000000000000000000000000000000000000000001d5 256)
    (store-sum
     (app sha3-app (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) (bv #x0000000000000000000000000000000000000000000000000000000000000040 256))
     (bvadd store-var$1 (bvneg (bvmul arg$1 arg$2)))))
   (cons
    (bv #x000000000000000000000000000000000000000000000000000000000000022d 256)
    (call-sum
     152
     (bvmul (bv #x00000000000000000000000000000000000000000000000000000000000008fc 256) (ite (bveq (bv #x0000000000000000000000000000000000000000000000000000000000000000 256) arg$2) (bv #x0000000000000000000000000000000000000000000000000000000000000001 256) (bv #x0000000000000000000000000000000000000000000000000000000000000000 256)))
     (bvand (bv #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff 256) var$219)
     arg$2)))))