solidity static analysis
Alpha
تحليل ثابت للتحقق من العقود الذكية للصلابة ، استنادًا إلى https://github.com/shaunazzopardi/solidity-cfg-builder و https://github.com/gordonpace/contractlarva.
تحاول هذه الأداة إثبات خصائص العقود الذكية الصلابة بالكامل ، وعلى النجاح الجزئي ، تعيد العقار المتبقي الذي لا يزال يتعين إثباته للعقد الذكي للصلابة.
نحن نستخدم تمثيلًا للرسم البياني للتدفق لعقد ذكي صلابة في محاولة لإثبات خصائص العقود الذكية بشكل ثابت من خلال الإفراط في التقريب عن تدفق التحكم في العقد الذكي للصلابة (استنادًا إلى مصارف الصلابة-CFG ، وحالتها المتغيرة.
يعتمد هذا جزئيًا على العمل المقدم في وقائع Prepost 2017 ، في سلسلة EPCTS ، ومتوفر على Arxiv.
يتم تمثيل كل وظيفة عقد ذكي كأتمتة تدفق تحكم (CFA) مع تحولات موسومة مع ثلاثة أضعاف: (1) شرط على حالة متغير البرنامج ؛ (2) بيان يحول حالة متغير البرنامج ؛ و (3) حدث خاصية تم تنشيطه عند تنفيذ البيان.
يتم زيادة كل هذا التلقائي من خلال التحولات التجريدية (الموسومة فقط بواسطة حدث خاصية) يتيح حدوث أي حدث أثناء وجوده في حالة أولية أو نهاية للبرنامج. يستخدم هذا كأساس للتحليل داخل المعالجة. كل من هذه الأوتوماتون يفرط على جميع عمليات إعدام العقد الذكي الذي يدعو إلى الوظيفة المقابلة. يسمى هذا Automaton Automaton Automaton Control-Flow (ACFA).
تقوم خوارزمية انتشار التأكيد البسيطة بنشر التأكيدات حول حالة متغير البرنامج (ضمنيًا بالشروط والبيانات) من خلال الحالات الصريحة لـ CFA حتى يتم مواجهة البيانات التي يمكن أن تؤثر على التأكيد. هذا سليم.
يتم تمثيل خاصية كحدث ديناميكي Automaton (DEA) الذي يستخدم التحولات الموسومة مع ثلاثية من: (1) حدث ؛ (2) حارس على حالة متغير الممتلكات ؛ و (3) إجراء على حالة متغير العقار.
يتكون ACFA مع تجريد متغير مع DEA ، ينتج نظام مراقبة مجردة (AMS) مع تحولات الموسومة بأزواج من التحولات CFA و DEA ، أو مع أحد المواضع التي تحتوي على الرمز #. عندما يتم استخدام # بدلاً من انتقال CFA ، فإنه يشير إلى تطابق عملية انتقال مجردة ، بينما بدلاً من انتقال DEA يشير إلى عدم وجود تطابق انتقال DEA.
بعد ذلك ، يتم إنشاء AMS لكل وظيفة من البرنامج مقابل DEA المعطى.
يتم استدعاء SMT Solver ، Z3 ، إلى الطيران أثناء بناء AMS لتحديد ما إذا كان من الممكن أن يتم تنشيط الانتقال المعطى في وقت النقطة في هذا النقطة. بالنظر إلى زوج انتقال CFA-DEA ، نتحقق من أن حارس DEA يمكن أن يثقل صحيحًا على التجريد المتغير لحالة المصدر التي تم تحديثها مع الشرط وبيان انتقال CFA. على الرغم من إعطاء زوج CFA-# ، فإننا نتحقق من أن التجريد المتغير لحالة المصدر المحدثة مع شرط وبيان انتقال CFA لا يتماشى مع نفي انفصال حراس DEA التي ربما يتم تنشيطها في هذه المرحلة (لاحظ أن انتقال DEA الصادر من نفس حالة الديمقراطية قد تأكد من أن يكون لديهم حراس مستثمران بشكل بسيط.
يتم تحليل كل AMS لتحديد أزواج انتقال CFA-DEA ، واستخراج انتقالات إدارة مكافحة المخدرات المستخدمة بهذه الطريقة ، متجاهلة مباريات انتقالات إدارة مكافحة المخدرات مع العنصر النائب. ينتج عن اتحاد انتقالات إدارة مكافحة المخدرات هذه المتبقية من إدارة مكافحة المخدرات الأصلية. يمكن تقليل ذلك في بعض الأحيان من خلال التحليل النشط ل DEA المتبقية.
علاوة على ذلك ، من AMSS ، يمكننا تحديد متى يمكن إزالة حارس انتقال إدارة مكافحة المخدرات (أي تم تغييره إلى صحيح ) ، أي عندما يمكن استخدامه في AMS ، يتم استخدامه دائمًا.
إذا لم يكن لدى المنتج المتبقي أي تحولات ، فقد ثبت أن العقار.
المتطلبات: Cabal v2.4.* (على سبيل المثال ، قم بتثبيت منصة Haskell الكاملة)
التجميع: اتبع التعليمات هنا
بالنسبة للنتائج الصحيحة ، تأكد دائمًا من أن رمز الصلابة يجمع مع مترجم صلابة.
لاستخدام الأداة ، تمرير موقع ملف صلابة العقد الذكي ، وملف خاصية DEA ، والموقع المفضل للإخراج إلى التنفيذ ، على سبيل المثال التنفيذ:
./main "./examples/courierservice.sol" ".
تم ترخيص هذا المشروع بموجب شروط ترخيص Apache 2.0.
