التحقق الرسمي لـ Tezos يمكّن أمان التمويل اللامركزي
تِزُوس، باعتبارها سلسلة كتلة معروفة تعتمد على إثبات الحصة، لا تقتصر ميزاتها على وظيفة الستاكينغ فقط. إن خاصية التحقق الرسمي في تِزُوس تعد أيضاً واحدة من المزايا التقنية الرئيسية لها. هذه الميزة قادرة على تعزيز أمان تطبيقات التمويل اللامركزي بشكل كبير، مما يعزز ثقة المستخدمين في أمان أموال العقود الذكية.
أمان التمويل اللامركزي وطرق التحقق الرسمي
لقد جذب النمو السريع للتمويل اللامركزي اهتمام العديد من المطورين، حيث اجتذبت بعض بروتوكولات التمويل اللامركزي الشهيرة أكثر من مئة مليون دولار من الأموال. ومع ذلك، لا يزال مجال التمويل اللامركزي يواجه تحديًا كبيرًا: مشكلة الأمان.
تكلفة هذه المشكلة ضخمة، وقد أثرت سلبًا على تأثير الشبكة لبعض مشاريع البلوكشين. في الأشهر القليلة الماضية، تعرضت عدة مشاريع التمويل اللامركزي للهجمات، وكانت الخسائر تتراوح بين عشرات الآلاف من الدولارات إلى عشرات الملايين من الدولارات. بعض المشاريع اكتشفت الأخطاء من خلال الفحص الذاتي في الوقت المناسب واتخذت إجراءات التجميد، مما منع المزيد من الخسائر.
بالنسبة لمطوري التمويل اللامركزي الذين يركزون على الأمان، فإن خطة التحقق الرسمي في Tezos يمكن أن تعزز الأمان في الوقت نفسه الذي تمكن فيه تطبيقات التمويل اللامركزي.
في تطبيقات الإنترنت التقليدية، بعد تعرض الخوادم للاختراق، يكفي استعادة بيانات المستخدمين لاستعادة الخسائر. لذلك، يمكن للتطبيقات التقليدية التي تركز على تجربة المستخدم التضحية ببعض الأمان مقابل التكرار السريع. ومع ذلك، في تطبيقات التمويل اللامركزي، بسبب عدم قابلية تغيير blockchain، بمجرد إطلاق العقود الذكية وظهور ثغرات أمنية، ستكون الخسائر التي تتعرض لها المستخدمين كبيرة ولا يمكن استعادتها.
لذلك، تحتاج عملية تطوير تطبيقات التمويل اللامركزي إلى استثمار大量 من الاختبارات والتدقيق المكلف لضمان الأمان، مما يؤثر بدوره على سرعة التكرار وسهولة استخدام المنتج. بالإضافة إلى ذلك، بسبب ارتفاع تكلفة التدقيق الأمني، يجد العديد من المطورين صعوبة في بدء مشاريع تطبيقات التمويل اللامركزي.
نقص المواهب في تطوير blockchain يؤدي إلى ارتفاع تكاليف التدقيق اليدوي. لذلك، أصبح الاعتماد بشكل متزايد على التحقق المدعوم بالآلة اتجاهًا سائدًا، حيث أن طرق التحقق الرسمي تعتبر وسيلة رئيسية لضمان الأمان.
التحقق الرسمي هو استخدام طرق رسمية في الرياضيات لإثبات أو دحض خصائص الخوارزميات، وهناك طريقتان رئيسيتان:
اختبار النموذج: سرد جميع الحالات الممكنة للنظام والتحقق منها واحدة تلو الأخرى، مناسب للتحقق التلقائي الكامل للأنظمة الصغيرة.
التحقق الاستنتاجي: يتم أولاً تصنيف رمز النظام كنموذج رياضي تجريدي، ثم يتم إثبات النظرية، وهو مناسب للأنظمة الكبيرة، ولكن يتطلب من البشر تحويل طرق تشغيل النظام إلى لغة مفهومة من قبل نظام التحقق.
لطالما كانت طرق التحقق الرسمي تُستخدم بشكل أساسي في المجالات الأكاديمية والدفاعية والطيران والفضاء بسبب التكاليف العالية، وهي تُستخدم قليلاً في المجال التجاري. نظرًا للاختلاف الجوهري في بيئة تشغيل تطبيقات الإنترنت التقليدية وتطبيقات blockchain، يجب تعديل عملية تطويرها بشكل مناسب، خاصةً من حيث نسبة الاستثمار في مرحلة التحقق من الأمان.
!
تطبيقات اللغات الوظيفية في مجال السلاسل العامة
لضمان الأمان، تختار العديد من مشاريع البلوكشين لغات وظيفية على مستوى البنية التحتية، أو الآلات الافتراضية، أو لغات العقود الذكية، مثل Ocaml و Haskell و Erlang. تُعرف اللغات الوظيفية بسمعتها الجيدة في مجال الأمان بسبب تعريفاتها الصارمة لأنواع المتغيرات، والتحقق من الترجمة، وأدوات التحقق الرسمي الجيدة (مثل CoQ). غالبًا ما تحتاج الشفرات المكتوبة بلغات إجرائية شائعة إلى إعادة وسمها باستخدام لغات وظيفية لإجراء التحقق الرسمي.
من بين العديد من مشاريع blockchain، فإن Tezos يدعم مجموعة متنوعة من لغات البرمجة للعقود الذكية، بما في ذلك العديد من لغات البرمجة الوظيفية مثل Pascal وOcaml وHaskell، بالإضافة إلى لغة Python المستخدمة على نطاق واسع. بالمقابل، تتطلب بعض المشاريع الأخرى من المطورين تعلم لغات برمجة وظيفية جديدة تمامًا، مما يزيد بلا شك من عتبة الدخول للتطوير.
الخصائص الأمنية للغة ميكلسون
تستخدم Tezos مقاربة مبتكرة في تصميم لغة العقود الذكية. تعتمد العقود الذكية في الأساس على لغة Michelson المستندة إلى Ocaml، بينما يتعامل المطورون فعليًا مع لغات البرمجة عالية المستوى مثل Python، دون الحاجة إلى فهم عميق للغة Michelson نفسها. يجمع هذا الأسلوب بين أمان لغة Michelson وإمكانية تدقيقها، بالإضافة إلى سهولة استخدام اللغات عالية المستوى مثل Python.
تتشابه ميكلسون من الناحية الهيكلية مع EVM الخاص بإيثريوم، مثل كونها لغة مكدسة، واستخدام التخزين على السلسلة، واعتماد نموذج رسوم الغاز، وكونها كاملة تورين. لكن الاختلاف الرئيسي بين ميكلسون و EVM هو:
الأنواع الثابتة: يجب أن تكون جميع البيانات المدخلة إلى عقود Michelson الذكية محددة بوضوح من حيث النوع، مما يتجنب الأخطاء البرمجية المتعلقة بعدم التوافق مع الأنواع.
الحساب الذري: يجب أن يتم تنفيذ عقد ميكلسون الذكي بالكامل قبل استدعاء عقود أخرى، مما يتجنب هجمات إعادة الدخول.
فشل الاستدعاء الواضح: هناك ثلاث حالات فقط لفشل التنفيذ: الفشل الواضح، نفاد الغاز، وتجاوز الكمية، مما يتجنب بعض هجمات التنفيذ الشائعة.
دلالة صارمة: هناك معايير صارمة بشأن حالة الأحرف، والمسافات، والأسطر القصيرة، مما يسهل تدقيق الشيفرة.
تساعد هذه التحسينات Michelson على مقاومة أنواع الهجمات الشائعة على Ethereum بشكل أفضل.
!
حزمة أدوات SmartPy
لا يحتاج مطورو DApp على Tezos إلى إتقان لغة Michelson. يمكنهم استخدام SmartPy SDK المستند إلى Python لتجميع العقود الذكية المكتوبة بلغة Python إلى لغة Michelson. لذلك، يحتاج مطورو DApp فقط إلى معرفة Python للبدء بسهولة.
SmartPy هو مكتبة بايثون، SmartPy.io يسمح للمستخدمين بتنفيذ سكريبتات بايثون في المتصفح. يوفر الموقع الرسمي لـ SmartPy محررًا عبر الإنترنت، حيث يمكن للمطورين كتابة الكود مباشرةً بلغة بايثون وتجميعه إلى عقود ذكية من نوع ميشيلسون، ثم نشرها على الشبكة الرئيسية لـ Tezos. واجهة الاستخدام الخاصة به أكثر بساطة ووضوحًا من محرر Remix عبر الإنترنت الخاص بـ إيثريوم، مما يجعل من السهل جدًا البدء. يأتي SmartPy أيضًا مع بعض قوالب التطوير الجاهزة لسهولة الرجوع إليها والتعلم.
تتضمن واجهة SmartPy.io منطقة كتابة الكود ومنطقة عرض نتائج التنفيذ. يمكن للمطورين بسهولة استخدام Python لكتابة وتحرير كود العقود. يبسط SmartPy عملية التجميع والتنفيذ، حيث يمكن الانتهاء منها فقط بالنقر على زر التنفيذ. تظهر نتائج التنفيذ على الفور على الجانب الأيمن من الشاشة، بما في ذلك مدخلات استدعاء العقد، حالة التخزين، كود Michelson بعد التجميع، وغيرها.
بالإضافة إلى محرر النصوص عبر الإنترنت، يوفر SmartPy أيضًا إصدار سطر الأوامر SmartPyBasic، مما يسمح للمطورين بتجميع وتشغيل كود SmartPy في بيئة محلية. يمكن عرض العقود الذكية الموزعة من خلال SmartPy Contract Explorer، حيث تكون حالة العقد الحالية والعمليات التاريخية واضحة تمامًا.
حالياً، يدعم SmartPy العديد من الميزات الشائعة في Python، مثل المتغيرات المحلية، والتحقق من نوع المتغيرات، ودالة Lambda، وغيرها. يمكن استبدال بعض الميزات غير المدعومة (مثل المصفوفات) باستخدام map. وهذا يعني أنه لا حاجة للاستثمار الكثير من الوقت والجهد في تعلم SmartPy، حيث يمكن للمطورين التركيز على تنفيذ ميزات أفضل.
بالنسبة للمطورين الذين يرغبون في دخول عالم SmartPy، هناك بعض الدورات التدريبية المتاحة للرجوع إليها:
قد تحتوي هذه الصفحة على محتوى من جهات خارجية، يتم تقديمه لأغراض إعلامية فقط (وليس كإقرارات/ضمانات)، ولا ينبغي اعتباره موافقة على آرائه من قبل Gate، ولا بمثابة نصيحة مالية أو مهنية. انظر إلى إخلاء المسؤولية للحصول على التفاصيل.
تكنولوجيا التحقق الرسمي من Tezos تعزز أمان التمويل اللامركزي
التحقق الرسمي لـ Tezos يمكّن أمان التمويل اللامركزي
تِزُوس، باعتبارها سلسلة كتلة معروفة تعتمد على إثبات الحصة، لا تقتصر ميزاتها على وظيفة الستاكينغ فقط. إن خاصية التحقق الرسمي في تِزُوس تعد أيضاً واحدة من المزايا التقنية الرئيسية لها. هذه الميزة قادرة على تعزيز أمان تطبيقات التمويل اللامركزي بشكل كبير، مما يعزز ثقة المستخدمين في أمان أموال العقود الذكية.
أمان التمويل اللامركزي وطرق التحقق الرسمي
لقد جذب النمو السريع للتمويل اللامركزي اهتمام العديد من المطورين، حيث اجتذبت بعض بروتوكولات التمويل اللامركزي الشهيرة أكثر من مئة مليون دولار من الأموال. ومع ذلك، لا يزال مجال التمويل اللامركزي يواجه تحديًا كبيرًا: مشكلة الأمان.
تكلفة هذه المشكلة ضخمة، وقد أثرت سلبًا على تأثير الشبكة لبعض مشاريع البلوكشين. في الأشهر القليلة الماضية، تعرضت عدة مشاريع التمويل اللامركزي للهجمات، وكانت الخسائر تتراوح بين عشرات الآلاف من الدولارات إلى عشرات الملايين من الدولارات. بعض المشاريع اكتشفت الأخطاء من خلال الفحص الذاتي في الوقت المناسب واتخذت إجراءات التجميد، مما منع المزيد من الخسائر.
بالنسبة لمطوري التمويل اللامركزي الذين يركزون على الأمان، فإن خطة التحقق الرسمي في Tezos يمكن أن تعزز الأمان في الوقت نفسه الذي تمكن فيه تطبيقات التمويل اللامركزي.
في تطبيقات الإنترنت التقليدية، بعد تعرض الخوادم للاختراق، يكفي استعادة بيانات المستخدمين لاستعادة الخسائر. لذلك، يمكن للتطبيقات التقليدية التي تركز على تجربة المستخدم التضحية ببعض الأمان مقابل التكرار السريع. ومع ذلك، في تطبيقات التمويل اللامركزي، بسبب عدم قابلية تغيير blockchain، بمجرد إطلاق العقود الذكية وظهور ثغرات أمنية، ستكون الخسائر التي تتعرض لها المستخدمين كبيرة ولا يمكن استعادتها.
لذلك، تحتاج عملية تطوير تطبيقات التمويل اللامركزي إلى استثمار大量 من الاختبارات والتدقيق المكلف لضمان الأمان، مما يؤثر بدوره على سرعة التكرار وسهولة استخدام المنتج. بالإضافة إلى ذلك، بسبب ارتفاع تكلفة التدقيق الأمني، يجد العديد من المطورين صعوبة في بدء مشاريع تطبيقات التمويل اللامركزي.
نقص المواهب في تطوير blockchain يؤدي إلى ارتفاع تكاليف التدقيق اليدوي. لذلك، أصبح الاعتماد بشكل متزايد على التحقق المدعوم بالآلة اتجاهًا سائدًا، حيث أن طرق التحقق الرسمي تعتبر وسيلة رئيسية لضمان الأمان.
التحقق الرسمي هو استخدام طرق رسمية في الرياضيات لإثبات أو دحض خصائص الخوارزميات، وهناك طريقتان رئيسيتان:
اختبار النموذج: سرد جميع الحالات الممكنة للنظام والتحقق منها واحدة تلو الأخرى، مناسب للتحقق التلقائي الكامل للأنظمة الصغيرة.
التحقق الاستنتاجي: يتم أولاً تصنيف رمز النظام كنموذج رياضي تجريدي، ثم يتم إثبات النظرية، وهو مناسب للأنظمة الكبيرة، ولكن يتطلب من البشر تحويل طرق تشغيل النظام إلى لغة مفهومة من قبل نظام التحقق.
لطالما كانت طرق التحقق الرسمي تُستخدم بشكل أساسي في المجالات الأكاديمية والدفاعية والطيران والفضاء بسبب التكاليف العالية، وهي تُستخدم قليلاً في المجال التجاري. نظرًا للاختلاف الجوهري في بيئة تشغيل تطبيقات الإنترنت التقليدية وتطبيقات blockchain، يجب تعديل عملية تطويرها بشكل مناسب، خاصةً من حيث نسبة الاستثمار في مرحلة التحقق من الأمان.
!
تطبيقات اللغات الوظيفية في مجال السلاسل العامة
لضمان الأمان، تختار العديد من مشاريع البلوكشين لغات وظيفية على مستوى البنية التحتية، أو الآلات الافتراضية، أو لغات العقود الذكية، مثل Ocaml و Haskell و Erlang. تُعرف اللغات الوظيفية بسمعتها الجيدة في مجال الأمان بسبب تعريفاتها الصارمة لأنواع المتغيرات، والتحقق من الترجمة، وأدوات التحقق الرسمي الجيدة (مثل CoQ). غالبًا ما تحتاج الشفرات المكتوبة بلغات إجرائية شائعة إلى إعادة وسمها باستخدام لغات وظيفية لإجراء التحقق الرسمي.
من بين العديد من مشاريع blockchain، فإن Tezos يدعم مجموعة متنوعة من لغات البرمجة للعقود الذكية، بما في ذلك العديد من لغات البرمجة الوظيفية مثل Pascal وOcaml وHaskell، بالإضافة إلى لغة Python المستخدمة على نطاق واسع. بالمقابل، تتطلب بعض المشاريع الأخرى من المطورين تعلم لغات برمجة وظيفية جديدة تمامًا، مما يزيد بلا شك من عتبة الدخول للتطوير.
الخصائص الأمنية للغة ميكلسون
تستخدم Tezos مقاربة مبتكرة في تصميم لغة العقود الذكية. تعتمد العقود الذكية في الأساس على لغة Michelson المستندة إلى Ocaml، بينما يتعامل المطورون فعليًا مع لغات البرمجة عالية المستوى مثل Python، دون الحاجة إلى فهم عميق للغة Michelson نفسها. يجمع هذا الأسلوب بين أمان لغة Michelson وإمكانية تدقيقها، بالإضافة إلى سهولة استخدام اللغات عالية المستوى مثل Python.
تتشابه ميكلسون من الناحية الهيكلية مع EVM الخاص بإيثريوم، مثل كونها لغة مكدسة، واستخدام التخزين على السلسلة، واعتماد نموذج رسوم الغاز، وكونها كاملة تورين. لكن الاختلاف الرئيسي بين ميكلسون و EVM هو:
الأنواع الثابتة: يجب أن تكون جميع البيانات المدخلة إلى عقود Michelson الذكية محددة بوضوح من حيث النوع، مما يتجنب الأخطاء البرمجية المتعلقة بعدم التوافق مع الأنواع.
الحساب الذري: يجب أن يتم تنفيذ عقد ميكلسون الذكي بالكامل قبل استدعاء عقود أخرى، مما يتجنب هجمات إعادة الدخول.
فشل الاستدعاء الواضح: هناك ثلاث حالات فقط لفشل التنفيذ: الفشل الواضح، نفاد الغاز، وتجاوز الكمية، مما يتجنب بعض هجمات التنفيذ الشائعة.
دلالة صارمة: هناك معايير صارمة بشأن حالة الأحرف، والمسافات، والأسطر القصيرة، مما يسهل تدقيق الشيفرة.
تساعد هذه التحسينات Michelson على مقاومة أنواع الهجمات الشائعة على Ethereum بشكل أفضل.
!
حزمة أدوات SmartPy
لا يحتاج مطورو DApp على Tezos إلى إتقان لغة Michelson. يمكنهم استخدام SmartPy SDK المستند إلى Python لتجميع العقود الذكية المكتوبة بلغة Python إلى لغة Michelson. لذلك، يحتاج مطورو DApp فقط إلى معرفة Python للبدء بسهولة.
SmartPy هو مكتبة بايثون، SmartPy.io يسمح للمستخدمين بتنفيذ سكريبتات بايثون في المتصفح. يوفر الموقع الرسمي لـ SmartPy محررًا عبر الإنترنت، حيث يمكن للمطورين كتابة الكود مباشرةً بلغة بايثون وتجميعه إلى عقود ذكية من نوع ميشيلسون، ثم نشرها على الشبكة الرئيسية لـ Tezos. واجهة الاستخدام الخاصة به أكثر بساطة ووضوحًا من محرر Remix عبر الإنترنت الخاص بـ إيثريوم، مما يجعل من السهل جدًا البدء. يأتي SmartPy أيضًا مع بعض قوالب التطوير الجاهزة لسهولة الرجوع إليها والتعلم.
تتضمن واجهة SmartPy.io منطقة كتابة الكود ومنطقة عرض نتائج التنفيذ. يمكن للمطورين بسهولة استخدام Python لكتابة وتحرير كود العقود. يبسط SmartPy عملية التجميع والتنفيذ، حيث يمكن الانتهاء منها فقط بالنقر على زر التنفيذ. تظهر نتائج التنفيذ على الفور على الجانب الأيمن من الشاشة، بما في ذلك مدخلات استدعاء العقد، حالة التخزين، كود Michelson بعد التجميع، وغيرها.
بالإضافة إلى محرر النصوص عبر الإنترنت، يوفر SmartPy أيضًا إصدار سطر الأوامر SmartPyBasic، مما يسمح للمطورين بتجميع وتشغيل كود SmartPy في بيئة محلية. يمكن عرض العقود الذكية الموزعة من خلال SmartPy Contract Explorer، حيث تكون حالة العقد الحالية والعمليات التاريخية واضحة تمامًا.
حالياً، يدعم SmartPy العديد من الميزات الشائعة في Python، مثل المتغيرات المحلية، والتحقق من نوع المتغيرات، ودالة Lambda، وغيرها. يمكن استبدال بعض الميزات غير المدعومة (مثل المصفوفات) باستخدام map. وهذا يعني أنه لا حاجة للاستثمار الكثير من الوقت والجهد في تعلم SmartPy، حيث يمكن للمطورين التركيز على تنفيذ ميزات أفضل.
بالنسبة للمطورين الذين يرغبون في دخول عالم SmartPy، هناك بعض الدورات التدريبية المتاحة للرجوع إليها:
!