Akıllı sözleşme açıkları bulmak için Manticore nasıl kullanılır

Bu öğreticinin amacı, akıllı sözleşmelerdeki hataları otomatik olarak bulmak için Manticore'un nasıl kullanılacağını göstermektir.

Kurulum

Manticore >= python 3.6 gerektirir. Pip veya docker kullanılarak kurulabilir.

Docker aracılığıyla Manticore

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

Son komut, geçerli dizininize erişimi olan bir docker'da eth-security-toolbox'ı çalıştırır. Dosyaları ana makinenizden değiştirebilir ve dosyalar üzerindeki araçları docker'dan çalıştırabilirsiniz

Docker'ın içinde şunu çalıştırın:

solc-select 0.5.11
cd /home/trufflecon/

Pip aracılığıyla Manticore

pip3 install --user manticore

solc 0.5.11 tavsiye edilir.

Bir komut dosyası çalıştırma

Python 3 ile bir python komut dosyası çalıştırmak için:

python3 script.py

Dinamik sembolik yürütmeye giriş

Özetle Dinamik Sembolik Yürütme

Dinamik sembolik yürütme (DSE), yüksek derecede semantik farkındalık ile bir durum uzayını araştıran bir program analiz tekniğidir. Bu teknik, path predicates (yol belirteçleri) olarak adlandırılan matematiksel formüller olarak temsil edilen "program yollarının" keşfine dayanır. Kavramsal olarak, bu teknik iki adımda yol belirteçleri üzerinde çalışır:

1. Programın girdisi üzerindeki kısıtlamalar kullanılarak oluşturulurlar.
2. İlişkili yolların yürütülmesine neden olacak program girdileri oluşturmak için kullanılırlar.

Bu yaklaşım, tanımlanmış tüm program durumlarının somut yürütme sırasında tetiklenmesi şeklinde yanlış pozitifler üretmez. Örneğin, analiz bir tamsayı taşması bulursa, bunun tekrarlanabilir olması garanti edilir.

Yol Belirteci Örneği

DSE'nin nasıl çalıştığına dair bir fikir edinmek için aşağıdaki örneği göz önünde bulundurun:

1function f(uint a){
2
3  if (a == 65) {
4      // A bug is present
5  }
6
7}
 Kopyala

f() iki yol içerdiği için, DSE iki farklı yol belirteci inşa eder:

• Path 1: a == 65
• Path 2: Not (a == 65)

Her yol belirteci, denklemi çözmeye çalışacak sözde SMT çözücüsüne(opens in a new tab) verilebilecek matematiksel bir formüldür. Path 1 için, çözücü yolun a = 65 ile keşfedileceğini söyleyecektir. Path 2 için, çözücü a'ya 65'ten farklı herhangi bir değer verebilir, örneğin a = 0.

Özellikleri doğrulama

Manticore, her yolun tüm yürütülmesi üzerinde tam kontrole izin verir. Sonuç olarak, hemen hemen her şeye keyfi kısıtlamalar eklemenize izin verir. Bu kontrol, sözleşmedeki özelliklerin oluşturulmasına izin verir.

Aşağıdaki örneği göz önünde bulundurun:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // no overflow protection
3  return c;
4}
 Kopyala

Burada fonksiyonda keşfedilecek tek bir yol var:

• Path 1: c = a + b

Manticore'u kullanarak taşma olup olmadığını kontrol edebilir ve yol belirtecine kısıtlamalar ekleyebilirsiniz:

• c = a + b AND (c < a OR c < b)

a ve b için yukarıdaki yol belirtecinin uygun olduğu bir değerleme bulmak mümkünse, bir taşma bulmuşsunuz demektir. Örneğin çözücü a = 10 , b = MAXUINT256 girdisini oluşturabilir.

Sabit bir versiyonu düşünürseniz:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
 Kopyala

Taşma denetimiyle ilişkili formül şöyle olacaktır:

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

Bu formül çözülemez; başka bir deyişle bu, safe_add'da c'nin her zaman artacağının ispatıdır.

Bu nedenle DSE, kodunuzdaki keyfi kısıtlamaları doğrulayabilen güçlü bir araçtır.

Manticore altında çalışma

Manticore API ile akıllı bir sözleşmeyi nasıl keşfedeceğimizi göreceğiz. Hedef, aşağıdaki akıllı sözleşme example.sol'dür(opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
Tümünü göster
 Kopyala

Bağımsız bir keşif çalıştırın

Aşağıdaki komutla Manticore'u doğrudan akıllı sözleşme üzerinde çalıştırabilirsiniz (project bir Solidity Dosyası veya bir proje dizini olabilir):

$ manticore project

Bunun gibi test senaryolarının çıktısını alacaksınız (sıra değişebilir):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
Tümünü göster

Ek bilgi olmadan Manticore, sözleşmede yeni yollar keşfetmeyene kadar sözleşmeyi yeni sembolik işlemlerle keşfedecektir. Manticore, başarısız bir işlemden sonra (örneğin: bir geri alma işleminden sonra) yeni işlemler çalıştırmaz.

Manticore, bilgileri bir mcore_* dizininde çıkaracaktır. Diğerlerinin yanı sıra bu dizinde şunları bulacaksınız:

• global.summary: kapsam ve derleme uyarıları
• test_XXXXX.summary: kapsam, son talimat, test durumu başına hesap bakiyeleri
• test_XXXXX.tx: test durumu başına detaylı işlem listesi

Burada Manticore, aşağıdakilere karşılık gelen 7 test senaryosu bulur (dosya adı sırası değişebilir):

Keşif özeti f(!=65), 65'ten farklı herhangi bir değerle çağrılan f'yi ifade eder.

Gördüğünüz üzere, Manticore her başarılı veya geri alınan işlem için benzersiz bir test senaryosu oluşturur.

Eğer hızlı kod keşfi istiyorsanız --quick-mode bayrağını kullanın (hata algılayıcıları, gaz hesaplamalarını vb. devre dışarı bırakır)

API aracılığıyla bir akıllı sözleşmeyi değiştirin

Bu bölüm, Manticore Python API aracılığıyla bir akıllı sözleşmenin nasıl değiştirileceğini açıklar. *.py python uzantılı yeni bir dosya oluşturabilir ve bu dosyaya API komutlarını (temelleri aşağıda anlatılacaktır) ekleyerek gerekli kodu yazabilir ve ardından $ python3 *.py komutu ile çalıştırabilirsiniz. Ayrıca aşağıdaki komutları doğrudan python konsolunda çalıştırabilirsiniz, konsolu çalıştırmak için $ python3 komutunu kullanın.

Hesap oluşturma

Yapmanız gereken ilk şey, aşağıdaki komutlarla yeni bir blok zinciri başlatmaktır:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
 Kopyala

Sözleşme olmayan bir hesap m.create_account(opens in a new tab) kullanılarak oluşturulur:

1user_account = m.create_account(balance=1000)
 Kopyala

Bir Solidity sözleşmesi m.solidity_create_contract(opens in a new tab) kullanılarak dağıtılabilir:

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# Initiate the contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
Tümünü göster
 Kopyala

Özet

• m.create_account(opens in a new tab) ve m.solidity_create_contract(opens in a new tab) ile kullanıcı ve sözleşme hesapları oluşturabilirsiniz.

İşlemleri yürütme

Manticore iki tür işlemi destekler:

• Ham işlem: tüm fonksiyonlar keşfedilir
• Adlandırılmış işlem: yalnızca bir fonksiyon keşfedilir

Ham işlem

Bir ham işlem m.transaction(opens in a new tab) ile yürütülür:

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
 Kopyala

Çağıran, adres, veri veya işlemin değeri somut veya sembolik olabilir:

• m.make_symbolic_value(opens in a new tab) sembolik bir değer oluşturur.
• m.make_symbolic_buffer(size)(opens in a new tab) sembolik bir bayt dizisi oluşturur.

Örneğin:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
 Kopyala

Veriler sembolik ise, Manticore işlemin yürütülmesi sırasında sözleşmenin tüm fonksiyonlarını keşfedecektir. Fonksiyon seçiminin nasıl çalıştığını anlamak için Ethernaut CTF Kullanımı(opens in a new tab) makalesindeki Fallback Function açıklamasına göz atmak faydalı olacaktır.

Adlandırılmış işlem

İşlevler, adları aracılığıyla yürütülebilir. f(uint var) komutunu user_account'tan sembolik bir değerle ve 0 ether ile yürütmek için şunu kullanın:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
 Kopyala

İşlemin value değeri belirtilmemişse, varsayılan olarak 0'dır.

Özet

• Bir işlemin argümanları somut veya sembolik olabilir
• Ham işlem tüm fonksiyonları keşfedecek
• Fonksiyonlar, isimleriyle çağrılabilir

Çalışma Alanı

m.workspace, oluşturulan tüm dosyalar için çıktı dizini olarak kullanılan dizindir:

1print("Results are in {}".format(m.workspace))
 Kopyala

Keşfi Durdurma

Keşfi durdurmak için m.finalize()(opens in a new tab) kullanın. Bu yöntem çağrıldığında ve Manticore keşfedilen yolların her biri için test senaryoları oluşturduğunda başka işlem gönderilmeyecektir.

Özet: Manticore altında çalışma

Önceki tüm adımları bir araya getirerek şunu elde ederiz:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
Tümünü göster
 Kopyala

Yukarıdaki kodların tamamını example_run.py(opens in a new tab) içinde bulabilirsiniz

Atış yollarını alma

Şimdi f() içinde bir istisna belirten yollar için spesifik girdiler oluşturacağız. Hedef hâlâ şu akıllı sözleşmedir example.sol(opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
 Kopyala

Durum bilgisini kullanmak

Yürütülen her yolun kendi blok zinciri durumu vardır. Bir durum ya hazırdır ya da öldürülmüştür, yani bir THROW veya REVERT komutuna ulaştığı anlamına gelir:

• m.ready_states(opens in a new tab): hazır olan durumların listesi (REVERT/INVALID yürütmediler)
• m.killed_states(opens in a new tab): öldürülmüş durumların listesi
• m.all_states(opens in a new tab): tüm durumlar

1for state in m.all_states:
2    # do something with state
 Kopyala

Durum bilgisine erişebilirsiniz. Örneğin:

• state.platform.get_balance(account.address): hesabın bakiyesi
• state.platform.transactions: işlem listesi
• state.platform.transactions[-1].return_data: son işlemden döndürülen veri

Son işlem tarafından döndürülen veriler, ABI.deserialize ile bir değere dönüştürülebilen bir dizidir, örneğin:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
 Kopyala

Test durumu nasıl oluşturulur

Test durumu oluşturmak için m.generate_testcase(state, name)(opens in a new tab) kullanın:

1m.generate_testcase(state, 'BugFound')
 Kopyala

Özet

• m.all_states ile durumu yineleyebilirsiniz
• state.platform.get_balance(account.address) hesabın bakiyesini döndürür
• state.platform.transactions işlemlerin listesini döndürür
• transaction.return_data döndürülen veridir
• m.generate_testcase(state, name) durum için girdiler oluşturur

Özet: Atış Yolunu Almak

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Check if an execution ends with a REVERT or INVALID
15for state in m.terminated_states:
16    last_tx = state.platform.transactions[-1]
17    if last_tx.result in ['REVERT', 'INVALID']:
18        print('Throw found {}'.format(m.workspace))
19        m.generate_testcase(state, 'ThrowFound')
Tümünü göster
 Kopyala

Yukarıdaki kodların tamamını example_run.py(opens in a new tab) içinde bulabilirsiniz

terminated_state tarafından döndürülen tüm durumların sonuçlarında REVERT veya INVALID olduğundan çok daha basit bir komut dosyası oluşturabileceğimizi unutmayın: Bu örnek yalnızca API'nin nasıl değiştirileceğini göstermek içindir.

Kısıtlamalar ekleme

Keşfi nasıl kısıtlayabileceğimizi göreceğiz. f() belgesinin, fonksiyonun hiçbir zaman a == 65 ile çağrılmadığını belirttiği varsayımını yapacağız, bu nedenle a == 65 ile herhangi bir hata gerçek bir hata değildir. Hedef hâlâ aşağıdaki akıllı sözleşmedir example.sol(opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
 Kopyala

Operatörler

Operatörler(opens in a new tab) modülü, sağladığı diğer şeylerin yanı sıra kısıtlamaların değiştirilmesini kolaylaştırır:

• Operators.AND,
• Operators.OR,
• Operators.UGT (unsigned greater than),
• Operators.UGE (unsigned greater than or equal to),
• Operators.ULT (unsigned lower than),
• Operators.ULE (unsigned lower than or equal to).

Modülü içe aktarmak için aşağıdakileri kullanın:

1from manticore.core.smtlib import Operators
 Kopyala

Operators.CONCAT bir diziyi bir değerle birleştirmek için kullanılır. Örneğin, bir işlemin return_data'sının başka bir değere karşı kontrol edilmesi için bir değerle değiştirilmesi gerekir:

1last_return = Operators.CONCAT(256, *last_return)
 Kopyala

Kısıtlamalar

Kısıtlamaları global olarak veya belirli bir durum için kullanabilirsiniz.

Global kısıtlama

Global bir kısıtlama eklemek için m.constrain(constraint) kullanın. Örneğin, sembolik bir adresten bir sözleşmeyi arayabilir ve bu adresi belirli değerlerle sınırlandırabilirsiniz:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
 Kopyala

Durum kısıtlaması

Belirli bir duruma kısıtlama eklemek için state.constrain(constraint)(opens in a new tab) kullanın. Üzerindeki bazı özellikleri kontrol etmek için keşfinden sonra durumu kısıtlamak için kullanılabilir.

Kısıtlamaları kontrol etmek

Eğer bir kısıtlamanın hâlâ mümkün olup olmadığını görmek istiyorsanız solver.check(state.constraints) kullanın. Örneğin, aşağıdakiler symbolic_value'yu 65'ten farklı olacak şekilde kısıtlar ve durumun hâlâ uygulanabilir olup olmadığını kontrol eder:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # state is feasible
 Kopyala

Özet: Kısıtlamalar Ekleme

Önceki koda kısıtlama ekleyerek şunu elde ederiz:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Check if an execution ends with a REVERT or INVALID
20for state in m.terminated_states:
21    last_tx = state.platform.transactions[-1]
22    if last_tx.result in ['REVERT', 'INVALID']:
23        # we do not consider the path were a == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
Tümünü göster
 Kopyala

Yukarıdaki kodların tamamını example_run.py(opens in a new tab) içinde bulabilirsiniz