Akıllı sözleşmelerdeki hataları 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 veya üzerini gerektirir. Pip veya docker kullanılarak kurulabilir.

Docker ile 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 docker'dan dosyalar üzerindeki araçları çalıştırabilirsiniz

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

solc-select 0.5.11
cd /home/trufflecon/

Pip ile Manticore

pip3 install --user manticore

solc 0.5.11 sürümü tavsiye edilir.

Bir betik çalıştırma

Python 3 ile bir python betiği ç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 anlamsal farkındalıkla bir durum uzayını araştıran bir program analizi tekniğidir. Bu teknik, yol koşulları (path predicates) olarak adlandırılan matematiksel formüller olarak temsil edilen "program yollarının" keşfine dayanır. Kavramsal olarak, bu teknik yol koşulları üzerinde iki adımda çalışır:

1. Programın girdisindeki 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ımlanan tüm program durumları somut yürütme sırasında tetiklenebildiği için yanlış pozitif sonuç üretmez. Örneğin, analiz bir tam sayı taşması bulursa, bunun yeniden üretilebilir olması garanti edilir.

Yol Koşulu Örneği

DSE'nin nasıl çalıştığına dair bir fikir edinmek için aşağıdaki örneği inceleyin:

1function f(uint a){
2
3  if (a == 65) {
4      // Bir hata mevcut
5  }
6
7}
Kopyala

f() iki yol içerdiğinden, bir DSE iki farklı yol koşulu oluşturacaktır:

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

Her yol koşulu, denklemi çözmeye çalışacak olan ve SMT çözücü (opens in a new tab) olarak adlandırılan bir araca verilebilen matematiksel bir formüldür. Yol 1 için çözücü, yolun a = 65 ile keşfedilebileceğini söyleyecektir. Yol 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ümü üzerinde tam kontrol sağlar. Sonuç olarak, neredeyse her şeye isteğe bağlı kısıtlamalar eklemenize olanak tanır. Bu kontrol, sözleşme üzerinde özellikler oluşturulmasına olanak tanır.

Aşağıdaki örneği inceleyin:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // taşma koruması yok
3  return c;
4}
Kopyala

Burada fonksiyonda keşfedilecek tek bir yol vardır:

• Yol 1: c = a + b

Manticore'u kullanarak taşmayı kontrol edebilir ve yol koşuluna kısıtlamalar ekleyebilirsiniz:

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

a ve b için yukarıdaki yol koşulunun uygulanabilir olduğu bir değerleme bulmak mümkünse bu, bir taşma bulduğunuz anlamına gelir. Örneğin, çözücü a = 10, b = MAXUINT256 girdisini oluşturabilir.

Düzeltilmiş bir sürümü düşünürsek:

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 kontrolü ile 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 içinde c'nin her zaman artacağının bir kanıtıdır.

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

Manticore altında çalıştırma

Manticore API'si ile bir akıllı sözleşmenin nasıl keşfedileceğini göreceğiz. Hedef, aşağıdaki akıllı sözleşmedir: example.sol (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ırma

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ı alırsınız (sıra değişebilir):

1...
2... m.c.manticore:INFO: Oluşturulan test senaryosu No. 0 - STOP
3... m.c.manticore:INFO: Oluşturulan test senaryosu No. 1 - REVERT
4... m.c.manticore:INFO: Oluşturulan test senaryosu No. 2 - RETURN
5... m.c.manticore:INFO: Oluşturulan test senaryosu No. 3 - REVERT
6... m.c.manticore:INFO: Oluşturulan test senaryosu No. 4 - STOP
7... m.c.manticore:INFO: Oluşturulan test senaryosu No. 5 - REVERT
8... m.c.manticore:INFO: Oluşturulan test senaryosu No. 6 - REVERT
9... m.c.manticore:INFO: Sonuçlar: /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 (ör. bir geri döndürmeden sonra) yeni işlemler çalıştırmaz.

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

• global.summary: kapsam ve derleyici uyarıları
• test_XXXXX.summary: kapsam, son talimat, test senaryosu başına hesap bakiyeleri
• test_XXXXX.tx: test senaryosu başına ayrıntılı 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), f'nin 65'ten farklı herhangi bir değerle çağrıldığını belirtir.

Fark edebileceğiniz gibi, Manticore her başarılı veya geri döndürülen işlem için benzersiz bir test senaryosu oluşturur.

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

API aracılığıyla bir akıllı sözleşmeyi yönetme

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

Hesap Oluşturma

Yapmanız gereken ilk şey, aşağıdaki komutlarla yeni bir blokzincir 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# Sözleşmeyi başlat
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

Ham bir işlem m.transaction (opens in a new tab) kullanılarak 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 ya da 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

Veri sembolik ise Manticore, işlem yürütme 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'ye Giriş (opens in a new tab) makalesindeki Yedek Fonksiyon açıklamasını görmek faydalı olacaktır.

Adlandırılmış işlem

Fonksiyonlar adları aracılığıyla yürütülebilir. f(uint var) öğesini sembolik bir değerle, user_account'tan 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 bir işlem tüm fonksiyonları keşfedecektir
• Fonksiyonlar adlarıyla çağrılabilir

Çalışma Alanı

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

1print("Sonuçlar burada: {}".format(m.workspace))
Kopyala

Keşfi Sonlandırma

Keşfi durdurmak için m.finalize() (opens in a new tab) kullanın. Bu yöntem çağrıldıktan ve Manticore keşfedilen her yol için test senaryoları oluşturduktan sonra başka işlem gönderilmemelidir.

Özet: Manticore altında çalıştırma

Önceki tüm adımları bir araya getirdiğimizde ş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("Sonuçlar burada: {}".format(m.workspace))
15m.finalize() # keşfi durdur
Tümünü göster
Kopyala

Yukarıdaki kodun tamamını example_run.py (opens in a new tab) dosyasında bulabilirsiniz

Hata Veren Yolları Alma

Şimdi f() içinde bir istisna oluşturan yollar için belirli girdiler oluşturacağız. Hedef, 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

Durum bilgilerini kullanma

Yürütülen her yolun blokzincirde kendi durumu vardır. Bir durum ya hazırdır ya da sonlandırılmıştır, yani bir THROW veya REVERT talimatına ulaşmıştır:

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

1for state in m.all_states:
2    # durum ile bir şeyler yap
Kopyala

Durum bilgilerine erişebilirsiniz. Örneğin:

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

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

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

Test senaryosu nasıl oluşturulur

Test senaryosu 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 durum üzerinde yineleme yapabilirsiniz
• 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: Hata Veren Yolu Alma

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## Bir yürütmenin REVERT veya INVALID ile bitip bitmediğini kontrol edin
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('Hata bulundu {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
Tümünü göster
Kopyala

Yukarıdaki kodun tamamını example_run.py (opens in a new tab) dosyasında bulabilirsiniz

terminated_state tarafından döndürülen tüm durumların sonucunda REVERT veya INVALID olduğundan çok daha basit bir betik oluşturabileceğimizi unutmayın: bu örnek yalnızca API'nin nasıl yönetileceğini göstermek içindi.

Kısıtlama ekleme

Keşfi nasıl kısıtlayacağımızı göreceğiz. f() belgesinin, fonksiyonun asla a == 65 ile çağrılmadığını belirttiğini varsayacağız, bu nedenle a == 65 ile ilgili herhangi bir hata gerçek bir hata değildir. Hedef, 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ü, kısıtlamaların yönetimini kolaylaştırır ve diğerlerinin yanı sıra şunları sağlar:

• Operators.AND,
• Operators.OR,
• Operators.UGT (işaretsiz büyüktür),
• Operators.UGE (işaretsiz büyük veya eşittir),
• Operators.ULT (işaretsiz küçüktür),
• Operators.ULE (işaretsiz küçük veya eşittir).

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

1from manticore.core.smtlib import Operators
Kopyala

Operators.CONCAT, bir diziyi bir değere 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ğere dönüştürülmesi gerekir:

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

Kısıtlamalar

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

Genel kısıtlama

Genel bir kısıtlama eklemek için m.constrain(constraint) kullanın. Örneğin, sembolik bir adresten bir sözleşme çağırabilir ve bu adresi belirli değerler olacak şekilde kısıtlayabilirsiniz:

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ıtlamayı Kontrol Etme

Bir kısıtlamanın hala uygulanabilir olup olmadığını öğrenmek için solver.check(state.constraints) kullanın. Örneğin, aşağıdakiler symbolic_value değerini 65'ten farklı olacak şekilde kısıtlayacak ve durumun hala uygulanabilir olup olmadığını kontrol edecektir:

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

Özet: Kısıtlama 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## Bir yürütmenin REVERT veya INVALID ile bitip bitmediğini kontrol edin
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # a == 65 olduğu yolu dikkate almıyoruz
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'Hata bulundu, sonuçlar burada: {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'Hata bulunamadı')
Tümünü göster
Kopyala

Yukarıdaki kodun tamamını example_run.py (opens in a new tab) dosyasında bulabilirsiniz

Sayfanın son güncellenmesi: 26 Nisan 2024

l (opens in a new tab)

n (opens in a new tab)

r (opens in a new tab)

+6

Katkıda bulunanları göster