securify

[تم إهماله] Securify

تم إهمال إصدار Securify ولن يتم دعمه. يرجى استخدام Securify v2.0.

Securify هو ماسح ضوئي للأمان لعقود Ethereum الذكية التي تدعمها مؤسسة Ethereum و Chainecurity. تم إجراء البحث الأساسي وراء Securify في مركز ICE في Eth Zurich.

إنه يتميز بقائمة واسعة من أنماط الأمان الموجودة عادة في العقود الذكية:

• بعض أشكال علة DAO (المعروفة أيضًا باسم إعادة الدخول)
• الأثير مغلق
• مفقود التحقق من صحة المدخلات
• المبلغ المعتمد على طلب المعاملات والمستقبل والنقل
• استثناءات غير معطلة
• تدفق الأثير غير المقيد

من المفترض أن يكون المشروع منصة مفتوحة ترحب بالمساهمات من جميع مجتمع أمن Ethereum. لاقتراح أنماط جديدة ، للتطوع للاختبار أو المساهمة في تطوير أنماط جديدة ، يرجى الاتصال من خلال مجموعة Discord.

ابدء

متطلبات

• Soufflé: https://github.com/souffle-lang/souffle/releases (يجب أن تعمل Securify مع أحدث الحزمة ، يرجى إثارة مشكلة إذا لم تكن كذلك). إذا لم تتمكن من تثبيت Soufflé ، فابحث عن حاوية Docker للحصول على بديل. سوف Securify تعطل بدون ثنائي souffle . اعتبارًا من الكتابة ، لا يتوفر Soufflé على Windows ، لذلك لا ينبغي أن يتم تشغيل Securify على Windows أيضًا.
• جافا 8
• مطلوب solc ثنائي لتكون قادرة على استخدام ملف الصلابة كمدخل. يفترض Securify أنه تم تثبيت الإصدار الصحيح للملف المحدد. solc متاح هنا.

يستخدم

للبناء:

./gradlew jar

لتشغيل Securify على ملف صلابة:

java -jar build/libs/securify.jar -fs src/test/resources/solidity/transaction-reordering.sol

لتشغيل Securify على إخراج فك الإلغاء الذي يوفره البرنامج النصي Pysolc.py (والذي يتطلب py-solc):

java -jar build/libs/securify.jar -co out.json

لتشغيل Securify على بعض EVM ثنائي (المنتج على سبيل المثال بواسطة solc ):

java -jar build/libs/securify.jar -fh src/test/resources/solidity/transaction-reordering.bin.hex

لرؤية القائمة الكاملة للخيارات:

java -jar build/libs/securify.jar -h

لتشغيل الاختبارات (التي تستخدم Junit4):

./gradlew test

غلاف بيثون يساعد على التعامل مع solc و truffle . المتطلبات في ملف المتطلبات. يمكن استخدام Dockerfile كمرجع لإنشاء بيئتك المحلية لاستخدام هذا الغلاف.

عامل ميناء

يجب أن يكون التثبيت بسيطًا بدرجة كافية على مشتقات Debian ، أو أي منصة أخرى تدعمها Soufflé.

للحصول على عرض سريع لا يتطلب Soufflé ، يمكنك استخدام Docker.

بناء صورة Docker:

docker build . -t securify

قم بتشغيل Securify على مثال صغير:

docker run securify

يمكنك تغيير الملفات التي تم تحليلها عن طريق تحديد وحدة تخزين إلى التركيب ، وسيتم معالجة كل ملف *.sol الموجود بواسطة Securify:

docker run -v $( pwd ) /folder_with_solidity_files:/project securify

يجب أن تسمح إضافة علامة --truffle securify بالتشغيل فوق مشروع الكمأة الذي تم فيه تثبيت التبعيات بالفعل (لذا قم npm install قبل أن لزم الأمر). بدون هذا العلم ، يتم تجميع المشروع باستخدام solc . أضف A -h للحصول على القائمة الكاملة للخيارات. على وجه الخصوص ، إذا أراد المستخدم تلقي معلومات التجميع من الكمأة ، فيجب عليه إضافة علامة -v .

إذا أراد المرء الحصول على إخراج JSON ، فإن Docker يدعم علامة --json التي ستقمع الإخراج الجميل وإعادة JSON بدلاً من ذلك. تأكد من إضافة علامة -q إذا لم يكن يجب عرض معلومات التقدم ، مما يؤدي إلى إخراج JSON النقي. تعتمد مؤشرات الخطوط المتطابقة على 0 ، مما يعني أن المباراة مع السطر i تعني أن الخط i+1 th متطابق. على وجه الخصوص ، يحتوي السطر الأول على فهرس 0.

الاختبارات

يمكن إجراء اختبارات النهاية الأساسية إلى النهاية من خلال ملف test.py:

 python3 test . py

يمكن تثبيت المتطلبات باستخدام pipenv:

pipenv install

أو باستخدام pip :

pip install -r requirements.txt

تقارن هذه الاختبارات إخراج JSON الحالي المقدم بواسطة Securify مع بعض الإخراج السابق ، والإبلاغ عن الاختلافات بين الاثنين.

تكامل ترافيس

يمكنك إضافة ما يلي .travis.yml إلى مشروعك لتشغيل Securify على ارتباطات جديدة:

 services:
  - docker

before_install:
  - docker pull chainsecurity/securify

script:
- docker run -v $(pwd):/project chainsecurity/securify

يجب أن يسمح هذا Securify بالتشغيل على مشروع الكمأة الذي تم فيه تثبيت التبعيات بالفعل (لذلك قم npm install قبل أن لزم الأمر).

الإخراج

يتبع الإخراج بشكل فضفاض نمط Clang. يتم الإبلاغ عن التحذيرات ونقاط الضعف فقط. إذا كان المرء يرغب أيضًا في الحصول على معلومات الامتثال ، فيرجى استخدام علم --json في Docker أو -co على java القابل للتنفيذ للحصول على جميع معلومات التحليل بتنسيق JSON.

المساهمة

انظر المساهمة.

انضم إلى خلافنا لمناقشة مع المستخدمين الآخرين.

القيود المعروفة

على الرغم من استخدام Securify بانتظام للمساعدة في عمليات التدقيق في ChainSecurity ، لا يزال هناك أخطاء ، بما في ذلك:

• لا يتم حاليا تحليل الكود في وظيفة الاحتياط. الحل البديل هو تسمية هذه الوظيفة بدلاً من ذلك.
• في بعض الحالات ، يتم إلقاء استثناء StackoverFlowerror ، بسبب كون computeBranches متكررة. في معظم الحالات ، يكفي زيادة حجم المكدس باستخدام خيار -Xss لـ java ، مثل java -Xss1G -jar ...
• لا يتم دعم المكتبات بشكل صحيح
• العقود المجردة (التي لا يمكن الحصول عليها من خلال solc ) لا يتم دعمها

العروض التقديمية والبحث والمدونات حول Securify

• Securify Research Paper المقدمة في ACM CCS'18 في تورنتو ، كندا
• ملخص ورقة البحث Securify في ورقة الصباح
• TechCrunch: سيضمن هذا الماسح الضوئي الذكي أن الرمز المميز الخاص بك هو TIP-TOP
• تحدث في EPFL في لوزان
• تحدث في DevCon3 في كانكون
• تحدث في D10E في دافوس
• يقوم باحثون من Eth Zürich بإصدار ماسح ضوئي مجاني للأمان لعقود Ethereum الذكية
• تحليل الأمن الآلي للعقود الذكية Ethereum
• اكتشاف الخلل تلقائيًا الذي جمدت محافظ التكافؤ

التفاصيل الفنية

يحلل Securify بشكل ثابت رمز EVM للعقد الذكي لاستنتاج المعلومات الدلالية المهمة (بما في ذلك حقائق التحكم في التدفق والبيانات) حول العقد. هذه الخطوة مؤتمتة بالكامل باستخدام Soufflé ، وهو حلال Datalog قابل للتطوير. بعد ذلك ، يتحقق Securify من الحقائق المستخلصة لاكتشاف الانتهاكات الأمنية أو إثبات الامتثال للتعليمات ذات الصلة بالأمن.

تتوفر التفاصيل الفنية الكاملة وراء الماسح الضوئي Securify في ورقة البحث.