EthIR
1.0.0
إطار لتحليل رفيع المستوى من الرمز البريطاني Ethereum. يقوم Ethir ببناء CFG كاملة وصوتية من رمز Ethereum bytecode ويولد تمثيلًا قائمًا على القواعد (RBR) للبرنامج. يمكّن هذا التمثيل رفيع المستوى من تطبيق التحليلات عالية المستوى الحالية لاستنتاج خصائص رمز EVM.
قم بتنزيل مصدر المجلد الذي يحتوي على مستودع ثابت في برنامج التحويل البرمجي للصلابة.
أضفه إلى المسار واختبار أنه تم تثبيته.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
في حال كنت ترغب في تثبيت أحدث إصدار:
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
يتم توفير ثابت ثابت في مصدر المجلد.
أضف OT إلى المسار واختبار أنه تم تثبيته.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
في حال كنت ترغب في تثبيت أحدث إصدار:
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
قم بتنزيل مجلد رمز المصدر.
فك ضغط المجلد وتثبيته.
unzip z3-z3-4.5.0.zip
cd z3-z3-4.5.0
python scripts/mk_make.py --python
cd build
make
sudo make install
استخدم أمر pip install لتثبيت ستة ، طلبات مكتب بيثون.
pip install six
pip install requests
قد تفشل الأوامر المذكورة أعلاه اعتمادًا على إصدار PIP. إذا كان الأمر كذلك ، فقم بتشغيل الأمر التالي بدلاً من الجهاز السابق.
python -m pip install six
python -m pip install requests
للتحقق من الإصدار قم بتشغيل Command pip -V .
لتنفيذ Ethir ، قم بتشغيل أحد الأوامر التالية داخل مجلد إثيري :
./oyente-ethir -s file_name.sol
./oyente-ethir -s file_name.evm -b
./oyente-ethir -s file_name.disasm -disasm
يعرض الأمر ./oyente-ethir -h بعض من أكثر الأشياء ذات الصلة هي:
./oyente-ethir -s filename -cfg
./oyente-ethir -s filename -saco
./oyente-ethir -s filename -d
يتم تخزين جميع الملفات التي تم إنشاؤها بواسطة Ethir أثناء تنفيذها في Directory/TMP/Costabs/.
بمجرد تثبيت Ethir ، لنفترض أننا نريد إنشاء RBR لحظر ملف التفكيك . EVM.Disasm في أمثلة المجلد. أولاً ، علينا أن نذهب إلى دليل Ethir وتنفيذ الأمر ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm
أثناء التنفيذ ، قام Ethir بإنشاء الدليل /TMP/Costabs/ حيث تقوم بتخزين RBR المرتبط بملف blockking.evm.disasm . إذا فحصنا هذا الدليل ، نجد ملفًا يسمى RBR.RBR يحتوي على RBR. إذا فتحنا الملف مع أي محرر مشترك (GEDIT ، EMACs) يمكننا أن نرى RBR تم إنشاؤه. فيما يلي Skecth من RBR تم إنشاؤه لـ blockking.evm.disasm file:
block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
s(0) = 96
s(1) = 64
l(0) = s(0)
s(0) = calldatasize
call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
eq(s(0), 0)
call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
neq(s(0), 0)
call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
s(0) = 224
s(1) = 2
s(0) = s(1)^s(0)
s(1) = 0
s(1) = calldataload
s(0) = s(1)/s(0)
s(1) = 607252836
s(2) = s(0)
call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
إذا قبلنا الأمر ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop فيما يلي رسم تخطيطي لـ RBR مع توضيحات NOPS التي تم إنشاؤها للحظر. evm.disasm :
block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
s(0) = 96
nop(PUSH1)
s(1) = 64
nop(PUSH1)
l(0) = s(0)
nop(MSTORE)
s(0) = calldatasize
nop(CALLDATASIZE)
call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
nop(ISZERO)
nop(PUSH2)
nop(JUMPI)
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
eq(s(0), 0)
call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
neq(s(0), 0)
call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
s(0) = 224
nop(PUSH1)
s(1) = 2
nop(PUSH1)
s(0) = s(1)^s(0)
nop(EXP)
s(1) = 0
nop(PUSH1)
s(1) = calldataload
nop(CALLDATALOAD)
s(0) = s(1)/s(0)
nop(DIV)
s(1) = 607252836
nop(PUSH4)
s(2) = s(0)
nop(DUP2)
call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
nop(EQ)
nop(PUSH2)
nop(JUMPI)
يسمح لنا Ethir أيضًا بتخزين CFG للملف الذي تم تحليله. في هذه الحالة ، يتعين علينا تنفيذ الأمر ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg يقوم Ethir بتخزين CFG في ملف مع امتداد .cfg في الدليل /TMP/Costabs/ .
لاحظ أن الملف قد يحتوي على أكثر من عقد ذكي واحد. في هذه الحالة ، يقوم Ethir بإنشاء ملف واحد لكل عقد RBR0.RBR ، RBR1.RBR ، ... RBRN.RBR.
تحتوي أمثلة المجلد على أمثلة تشغيل لاختبار الأداة. هناك كل من ملفات الصلابة ، EVM وتفكيك.
معظم الأمثلة مثل bloccking.evm.disasm أو Advertisement.sol أو validtoken.sol أو cryptophoenix.sol هي عقود حقيقية تم الحصول عليها من blockchain بينما أخرى مثل loop1.sol و sum.SOL هي أمثلة مخصصة حيث يكون من السهل فهم عملية التوسيع.
SACO هو محلل ثابت للكائنات المتزامنة التي ، قادرة على استنتاج ، من بين خصائص أخرى ، الحدود العليا على عدد تكرار الحلقات. لاحظ أن هذه هي الخطوة الأولى الحاسمة لاستنتاج استهلاك الغاز للعقود الذكية.
يتطابق التمثيل الداخلي لـ SACO مع قواعد RBR التي تم إنشاؤها بواسطة Ethir بعد الترجمات النحوية البسيطة. بفضل هذا ، من الممكن أن يثبت إنهاء الحلقات أن بعض الأمثلة تحتوي على وإنتاج خطية خطي لتلك الحلقات. فيما يلي بعض حدود الحلقة المستخلصة بواسطة SACO لبعض العقود الذكية الواردة في أمثلة المجلد:
| العقد الذكي | مرتبط ب | العقد الذكي | مرتبط ب |
|---|---|---|---|
| حظر | NAT (G8/10)*36+8934493 | cryptophoenix | NAT (G3)*228409344+4113285485 |
| loop1 | NAT (A)*25+234 | illigma | Nat (_numberofreturns)*2628+134 |
| اليانصيب | 159 | Blocksquareseriea | 286 |
| جيوب | 268 | Auctusether | 264 |
| إعلان | Inf | ValidToken | Inf |
ساكو تضفي حداً خطيًا للعقود الذكية الأربعة الأولى الموضحة في الجدول أعلاه. تعتمد حدود العقود الذكية و Cryptophoenix على قيمة أحد حقولها (الثامن والثالث على التوالي). بالنسبة للعقود الذكية Loop1 و illigma ، تعتمد الحدود التي تم الحصول عليها على حجج بعض وظائفها (A و _numberofreturns). في حالة عدم احتواء العقود الذكية على أي حلقة مثل اليانصيب أو Locksquareseriea أو الجيوب أو Auctusether ، فإن Saco تضفي حدًا ثابتًا.
لاحظ أنه بسبب القيود الدقيقة لـ SACO (لا تحتوي على عمليات البت ونموذج للوظيفة SHA3) ، ينسى المحلل المعلومات الخاصة بمتغيرات البتات. بسبب هذا العامل ، لا تستطيع SACO استنتاج وجود بعض العقود الذكية مثل ValidToken أو الإعلان وإرجاع INF .
يمكن تكييف محللون آخرون على مستوى رفيع المستوى يعملون على أشكال وسيطة مثل أنظمة انتقال عدد صحيح أو بنود القرن (على سبيل المثال ، Aprove ، T2 ، HomeMax ، cofloco) بسهولة للعمل على برامج RBR المترجمة التي تنتجها Ethir.
إذا كنت مثيراً للاهتمام في استخدام Ethir بشكل مشترك مع SACO Contact Developmenters من خلال طلب سحب أو مشكلة جديدة.
يمكنك تجربة النموذج الأولي الأول هنا. غاستاب يثبت حدود أعلى من الغاز المتورط في كل معاملة.
