معلومات عامة

التحقق من وقت التشغيل هو طريقة لتحليل وتنفيذ النظام الحسابي مصممة لاستخراج المعلومات من نظام قيد التشغيل لاكتشاف وربما الاستجابة لما إذا كان السلوك الملاحظ يلبي أو ينتهك سمات معينة. يمكن استخدام هذه التقنية لمجموعة متنوعة من الأغراض ، مثل مراقبة سياسة الأمان أو الأمان ، وتصحيح الأخطاء ، والاختبار ، والتحقق ، والتحقق ، وتحليل الأداء ، والأمان من الفشل ، وتعديل السلوك ، والمزيد. يتجنب تعقيدات تقنيات التحقق الرسمية التقليدية من خلال تحليل عدد صغير من مسارات التنفيذ والعمل مباشرة مع النظام الفعلي.

Runtime Verification Inc. هي شركة تركز على الجهاز الظاهري وعمليات تدقيق أمان العقود الذكية باستخدام تقنيات التحقق من وقت التشغيل. تشمل الخدمات التي يقدمونها مراجعات التصميم ومراجعات التعليمات البرمجية وعمليات التدقيق والتحقق الرسمي من العقود والبروتوكولات الذكية.

ما هي المنتجات التي تقدمها شركة Runtime Verification Inc. حاليًا ؟

تقوم شركة Runtime Verification Inc. حاليًا بتطوير ثلاثة منتجات أساسية: RV-Predict هي أداة تحليل وقت تشغيل تنبؤية تركز على الكشف التلقائي عن الأخطاء المتزامنة في البرنامج. RV-Monitor هي منهجية تطوير وأداة إنشاء مكتبة تسمح بمراقبة الخصائص التي يختارها المستخدم وتنفيذها في وقت التشغيل. RV-Match هي أداة تسمح بإجراء التحقق الشامل من وقت التشغيل بشكل رمزي على جميع مسارات البرنامج الممكنة ، مما يثبت أن بعض الخصائص صحيحة لجميع عمليات التنفيذ المحتملة لبرنامج معين.

متى ولماذا يجب استخدام RV-Predict ؟

عندما تكون صحة التزامن مهمة للتطبيقات متعددة الخيوط ، يجب استخدام RV-Predict. RV-Predict قادر على اكتشاف مشكلات التزامن وتنافس البيانات في البرنامج بكفاءة وسلاسة ، وهو سهل التشغيل للغاية ، ولا يتطلب عمومًا أي تكوين. يستخدم RV-Predict أيضًا إمكانات التنبؤ الفريدة لاكتشاف الادعاءات المحتملة ، حتى لو لم تحدث في تتبع التنفيذ لسجلات RV-Predict.

متى ولماذا يجب استخدام RV-Monitor ؟

يسمح RV-Monitor بمراقبة التطبيقات أو الأنظمة المعقدة وإجراء خصائص تنفيذ التتبع عليها. يجب استخدام RV-Monitor طالما توجد مواصفات لإدارة تطوير البرامج ، والالتزام بهذه المواصفات هو ميزة مهمة للبرنامج. يمكن أيضًا استخدام RV-Monitor لمراقبة الامتثال لواجهات برمجة التطبيقات الشائعة ، بما في ذلك واجهات برمجة التطبيقات Android و Java.

متى ولماذا يجب استخدام RV-Match ؟

يمكن لـ RV-Monitor التحقق من الامتثال لخصائص معينة لتنفيذ برنامج معين وفرضه ، بينما يمكن لـ RV-Match إثبات صحة البرنامج في وقت التشغيل ، وبالتالي تحليل آثار التنفيذ على جميع عمليات التنفيذ الممكنة المسارات وجميع المدخلات الممكنة. يوفر RV-Match ضمانات صحة قوية ، ومحاكاة التنفيذ بطريقة رمزية باستخدام الدلالات المحددة رسميًا للغة الهدف. عندما تكون هناك حاجة إلى ضمانات قوية للتحقق الرسمي ، يجب استخدام RV-Match ، ويمكن استخدامه أيضًا مع RV-Monitor للتخلص من مراقبة المناطق التي يمكن أن تثبت أن الخصائص لم يتم انتهاكها مطلقًا.

ما هي التراخيص التي تغطيها منتجات Runtime Verification Inc. ؟

تنقسم المشاريع التي طورتها RV إلى فئتين: المنتجات المسجلة الملكية وتلك المرخصة بموجب ترخيص مفتوح (كجزء من النظام البيئي مفتوح المصدر لـ RV).

تشمل المنتجات المسجلة الملكية جميع المنتجات غير المرخصة صراحةً بموجب ترخيص مفتوح وتستخدم للتقييم والأغراض الأكاديمية / غير التجارية فقط. لا يجوز إنشاء الأعمال المشتقة باستخدام منتجات RV المسجلة الملكية دون إذن مسبق ، وتحتفظ RV بجميع الحقوق في المنتجات المسجلة الملكية. لا يجوز إجراء هندسة عكسية للمنتجات المسجلة الملكية بأي شكل من الأشكال.

تدقيق مشروع Blockchain

شارك Runtime Verification في تدقيق العديد من مشاريع blockchain ، بما في ذلك على سبيل المثال لا الحصر ما يلي:

- التدقيق الأمني للعقود الذكية: وهي توفر عمليات تدقيق منخفضة التكلفة للعقود مثل ERC-20 و ERC-721 و ERC-4626 وما إلى ذلك.

- التدقيق الأمني للبروتوكولات: يشمل بروتوكولات العمليات المتعلقة بالإقراض.

- التحقق الرسمي: يوفر أدوات تحقق رسمية مفتوحة المصدر وأدوات مطور لتقليل تكاليف التدقيق وتمكين التحقق الرسمي المستمر.

تتضمن عمليات تدقيقهم عادةً مراجعات يدوية وعمليات تحقق رسمية لضمان مستويات عالية من أمان وموثوقية التعليمات البرمجية.