Akıllı sözleşmelerdeki hataları bulmak için Manticore nasıl kullanılır

Bu eğitimin 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 aracılığıyla 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, eth-security-toolbox'ı mevcut dizininize erişimi olan bir Docker içinde çalıştırır. Dosyaları ana makinenizden değiştirebilir ve araçları Docker'daki dosyalar üzerinde çalıştırabilirsiniz

Docker 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 önerilir.

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ş

Kısaca Dinamik Sembolik Yürütme

Dinamik sembolik yürütme (DSE), bir durum uzayını yüksek derecede anlamsal farkındalıkla keşfeden bir program analiz tekniğidir. Bu teknik, path predicates adı verilen matematiksel formüller olarak temsil edilen "program yollarının" keşfine dayanır. Kavramsal olarak, bu teknik yol yüklemleri (path predicates) üzerinde iki adımda ç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ımlanan tüm program durumlarının somut yürütme sırasında tetiklenebilmesi anlamında hiçbir yanlış pozitif (false positive) üretmez. Örneğin, analiz bir tam sayı taşması (integer overflow) bulursa, bunun yeniden üretilebilir olması garanti edilir.

Yol Yüklemi Örneği

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

function f(uint a){

  if (a == 65) {
      // Bir hata mevcut
  }

}

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

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

Her yol yüklemi, denklemi çözmeye çalışacak olan SMT çözücü (opens in a new tab) adı verilen bir araca verilebilecek matematiksel bir formüldür. Path 1 için çözücü, yolun a = 65 ile keşfedilebileceğini söyleyecektir. Path 2 için çözücü, a değerine 65 dışında herhangi bir değer verebilir, örneğin a = 0.

Özellikleri doğrulama

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

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

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

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

• Yol 1: c = a + b

Manticore kullanarak taşma olup olmadığını kontrol edebilir ve yol yüklemine kısıtlamalar ekleyebilirsiniz:

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

Yukarıdaki yol yükleminin uygulanabilir olduğu bir a ve b değerlemesi bulmak mümkünse, bu bir taşma bulduğunuz anlamına gelir. Örneğin çözücü, a = 10 , b = MAXUINT256 girdisini üretebilir.

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

function safe_add(uint a, uint b) returns(uint c){
  c = a + b;
  require(c>=a);
  require(c>=b);
  return c;
}

Taşma kontrolü ile ilişkili formül şu şekilde 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 değerinin her zaman artacağının bir kanıtıdır.

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

Manticore altında çalıştırma

Manticore API 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):

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

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

...
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 0 - STOP
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 1 - REVERT
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 2 - RETURN
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 3 - REVERT
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 4 - STOP
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 5 - REVERT
... m.c.manticore:INFO: Oluşturulan test senaryosu No. 6 - REVERT
... m.c.manticore:INFO: Sonuçlar şurada: /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

Ek bilgi olmadan Manticore, sözleşme üzerinde yeni yollar keşfetmeyene kadar sözleşmeyi yeni sembolik işlemlerle keşfedecektir. Manticore, başarısız olan bir işlemden sonra (örneğin: bir geri al (revert) 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 derleyici uyarıları
• test_XXXXX.summary: kapsam, son talimat, test senaryosu başına hesap bakiyeleri
• test_XXXXX.tx: test senaryosu başına işlemlerin ayrıntılı listesi

Burada Manticore, şunlara 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 alınan işlem için benzersiz bir test senaryosu oluşturur.

Hızlı kod keşfi istiyorsanız --quick-mode bayrağını kullanın (hata dedektörlerini, Gaz hesaplamasını vb. devre dışı bırakır)

API aracılığıyla bir akıllı sözleşmeyi manipüle etme

Bu bölüm, Manticore Python API aracılığıyla bir akıllı sözleşmenin nasıl manipüle edileceğinin ayrıntılarını açıklar. Python uzantılı *.py yeni bir dosya oluşturabilir ve API komutlarını (temelleri aşağıda açıklanacaktır) bu dosyaya ekleyerek gerekli kodu yazabilir ve ardından $ python3 *.py komutuyla çalıştırabilirsiniz. Ayrıca aşağıdaki komutları doğrudan Python konsolunda da 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:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1000)

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

source_code = '''
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}
'''
# Initiate the contract
contract_account = m.solidity_create_contract(source_code, owner=user_account)

Özet

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

İşlemleri yürütme

Manticore iki tür işlemi destekler:

• Ham işlem: tüm fonksiyonlar keşfedilir
• İsimlendirilmiş işlem: yalnızca bir fonksiyon keşfedilir

Ham işlem

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

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

İşlemin çağırıcısı, adresi, verisi veya 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:

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              value=symbolic_value)

Veri sembolikse, Manticore işlem yürütmesi 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 Uygulaması (opens in a new tab) makalesindeki Geri Dönüş Fonksiyonu (Fallback Function) açıklamasını görmek faydalı olacaktır.

İsimlendirilmiş işlem

Fonksiyonlar isimleri aracılığıyla yürütülebilir. f(uint var) fonksiyonunu sembolik bir değerle, user_account üzerinden ve 0 Ether ile yürütmek için şunu kullanın:

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

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

Özet

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

Çalışma Alanı

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

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

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 sonra başka işlem gönderilmemelidir ve Manticore keşfedilen her yol için test senaryoları oluşturur.

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

Önceki tüm adımları bir araya getirdiğimizde şunu elde ederiz:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

print("Results are in {}".format(m.workspace))
m.finalize() # keşfi durdur

Yukarıdaki tüm kodları example_run.py (opens in a new tab) içinde bulabilirsiniz

Hata fırlatan yolları alma

Şimdi f() içinde bir istisna (exception) oluşturan yollar için belirli girdiler üreteceğiz. Hedef hala aşağıdaki akıllı sözleşmedir example.sol (opens in a new tab):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Durum bilgisini kullanma

Yürütülen her yolun kendi Blokzincir durumu vardır. Bir durum ya hazırdır ya da sonlandırılmıştır (killed), 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ılan durumların listesi
• m.all_states (opens in a new tab): tüm durumlar

for state in m.all_states:
    # durumla bir şeyler yap

Durum bilgisine 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 bir dizidir ve örneğin ABI.deserialize ile bir değere dönüştürülebilir:

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

Test senaryosu nasıl oluşturulur

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

m.generate_testcase(state, 'BugFound')

Özet

• m.all_states ile durumlar ü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 Fırlatan Yolu Alma

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

## Bir yürütmenin GERİ AL veya GEÇERSİZ ile sonlanıp sonlanmadığını kontrol et
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.format(m.workspace))
        m.generate_testcase(state, 'ThrowFound')

Yukarıdaki tüm kodları example_run.py (opens in a new tab) içinde bulabilirsiniz

Not: terminated_state tarafından döndürülen tüm durumların sonucunda REVERT veya INVALID olduğundan çok daha basit bir betik oluşturabilirdik: bu örnek yalnızca API'nin nasıl manipüle edileceğini göstermek amacıyla verilmiştir.

Kısıtlamalar ekleme

Keşfi nasıl kısıtlayacağımızı göreceğiz. f() belgelerinin, 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 hala aşağıdaki akıllı sözleşmedir example.sol (opens in a new tab):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

Operatörler

Operators (opens in a new tab) modülü, kısıtlamaların manipülasyonunu kolaylaştırır, 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:

from manticore.core.smtlib import Operators

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 edilebilmesi için bir değere dönüştürülmesi gerekir:

last_return = Operators.CONCAT(256, *last_return)

Kısıtlamalar

Kısıtlamaları küresel olarak veya belirli bir durum için kullanabilirsiniz.

Küresel kısıtlama

Küresel 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:

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

Durum kısıtlaması

Belirli bir duruma kısıtlama eklemek için state.constrain(constraint) (opens in a new tab) kullanın. Keşfinden sonra durum üzerinde bazı özellikleri kontrol etmek amacıyla 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ğıdaki kod symbolic_value değerini 65'ten farklı olacak şekilde kısıtlayacak ve durumun hala uygulanabilir olup olmadığını kontrol edecektir:

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

Özet: Kısıtlamalar Ekleme

Önceki koda kısıtlama eklediğimizde şunu elde ederiz:

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib.solver import Z3Solver

solver = Z3Solver.instance()

m = ManticoreEVM()

with open("example.sol") as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

no_bug_found = True

## Bir yürütmenin GERİ AL veya GEÇERSİZ ile sonlanıp sonlanmadığını kontrol et
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        # a == 65 olduğu yolu dikkate almıyoruz
        condition = symbolic_var != 65
        if m.generate_testcase(state, name="BugFound", only_if=condition):
            print(f'Bug found, results are in {m.workspace}')
            no_bug_found = False

if no_bug_found:
    print(f'No bug found')

Yukarıdaki tüm kodları example_run.py (opens in a new tab) içinde bulabilirsiniz