اسمارٹ کنٹریکٹس کی باضابطہ تصدیق

اسمارٹ کنٹریکٹس غیر مرکزی، بھروسے کے بغیر، اور مضبوط ایپلیکیشنز بنانا ممکن بنا رہے ہیں جو صارفین کے لئے نئے استعمال کے معاملات متعارف کراتے ہیں اور قدر کو غیر مقفل کرتے ہیں۔ چونکہ اسمارٹ کنٹریکٹس بڑی مقدار میں قدر کو سنبھالتے ہیں، سیکیورٹی ڈیولپرز کے لیے ایک اہم غور و فکر ہے۔

باضابطہ تصدیق اسمارٹ کنٹریکٹ سیکیورٹی کو بہتر بنانے کے لیے تجویز کردہ تکنیکوں میں سے ایک ہے۔ باضابطہ تصدیق، جو پروگراموں کی وضاحت، ڈیزائننگ اور تصدیق کے لیے باضابطہ طریقےopens in a new tab استعمال کرتی ہے، سالوں سے اہم ہارڈویئر اور سافٹ ویئر سسٹمز کی درستگی کو یقینی بنانے کے لیے استعمال کی جا رہی ہے۔

جب اسمارٹ کنٹریکٹس میں لاگو کیا جاتا ہے، تو باضابطہ تصدیق یہ ثابت کر سکتی ہے کہ کنٹریکٹ کی کاروباری منطق پہلے سے طے شدہ تفصیلات پر پورا اترتی ہے۔ کنٹریکٹ کوڈ کی درستگی کا اندازہ لگانے کے دیگر طریقوں، جیسے ٹیسٹنگ، کے مقابلے میں، باضابطہ تصدیق مضبوط ضمانتیں دیتی ہے کہ ایک اسمارٹ کنٹریکٹ فعال طور پر درست ہے۔

باضابطہ تصدیق کیا ہے؟

باضابطہ تصدیق اس عمل سے مراد ہے جس میں ایک سسٹم کی درستگی کا جائزہ ایک باضابطہ تفصیلات کے حوالے سے لیا جاتا ہے۔ آسان الفاظ میں، باضابطہ تصدیق ہمیں یہ جانچنے کی اجازت دیتی ہے کہ آیا کسی سسٹم کا رویہ کچھ تقاضوں کو پورا کرتا ہے (یعنی، یہ وہی کرتا ہے جو ہم چاہتے ہیں)۔

سسٹم کے متوقع رویے (اس معاملے میں ایک اسمارٹ کنٹریکٹ) باضابطہ ماڈلنگ کا استعمال کرتے ہوئے بیان کیے جاتے ہیں، جبکہ تفصیلات کی زبانیں باضابطہ خصوصیات کی تخلیق کو ممکن بناتی ہیں۔ باضابطہ تصدیق کی تکنیکیں پھر یہ تصدیق کر سکتی ہیں کہ کنٹریکٹ کا نفاذ اس کی تفصیلات کے مطابق ہے اور سابقہ کی درستگی کا ریاضیاتی ثبوت حاصل کر سکتی ہیں۔ جب کوئی کنٹریکٹ اپنی تفصیلات کو پورا کرتا ہے، تو اسے “فعال طور پر درست”، “ڈیزائن کے لحاظ سے درست”، یا “تعمیر کے لحاظ سے درست” کے طور پر بیان کیا جاتا ہے۔

باضابطہ ماڈل کیا ہے؟

کمپیوٹر سائنس میں، ایک باضابطہ ماڈلopens in a new tab ایک حسابی عمل کی ریاضیاتی تفصیل ہے۔ پروگراموں کو ریاضیاتی افعال (مساوات) میں خلاصہ کیا جاتا ہے، جس میں ماڈل یہ بیان کرتا ہے کہ ان پٹ دیے جانے پر فنکشنز کے آؤٹ پٹ کا حساب کیسے لگایا جاتا ہے۔

باضابطہ ماڈل خلاصہ کی ایک سطح فراہم کرتے ہیں جس پر کسی پروگرام کے رویے کا تجزیہ کیا جا سکتا ہے۔ باضابطہ ماڈلز کا وجود ایک باضابطہ تفصیلات کی تخلیق کی اجازت دیتا ہے، جو زیر بحث ماڈل کی مطلوبہ خصوصیات کو بیان کرتی ہے۔

باضابطہ تصدیق کے لیے اسمارٹ کنٹریکٹس کی ماڈلنگ کے لیے مختلف تکنیکیں استعمال کی جاتی ہیں۔ مثال کے طور پر، کچھ ماڈلز ایک اسمارٹ کنٹریکٹ کے اعلیٰ سطحی رویے کے بارے میں استدلال کرنے کے لیے استعمال ہوتے ہیں۔ یہ ماڈلنگ تکنیکیں اسمارٹ کنٹریکٹس پر بلیک باکس کا نظریہ لاگو کرتی ہیں، انہیں ایسے سسٹمز کے طور پر دیکھتی ہیں جو ان پٹ قبول کرتے ہیں اور ان ان پٹس کی بنیاد پر حساب کتاب کرتے ہیں۔

اعلیٰ سطحی ماڈلز اسمارٹ کنٹریکٹس اور بیرونی ایجنٹوں کے درمیان تعلق پر توجہ مرکوز کرتے ہیں، جیسے کہ بیرونی ملکیت والے اکاؤنٹس (EOAs)، کنٹریکٹ اکاؤنٹس، اور بلاک چین ماحول۔ ایسے ماڈل خصوصیات کی تعریف کے لیے مفید ہیں جو یہ بتاتی ہیں کہ کسی کنٹریکٹ کو کچھ صارف کے تعاملات کے جواب میں کیسا برتاؤ کرنا چاہیے۔

اس کے برعکس، دیگر باضابطہ ماڈل ایک اسمارٹ کنٹریکٹ کے نچلے درجے کے رویے پر توجہ مرکوز کرتے ہیں۔ اگرچہ اعلیٰ سطحی ماڈل کنٹریکٹ کی فعالیت کے بارے میں استدلال میں مدد کر سکتے ہیں، وہ نفاذ کے اندرونی کاموں کے بارے میں تفصیلات حاصل کرنے میں ناکام ہو سکتے ہیں۔ نچلے درجے کے ماڈل پروگرام کے تجزیے پر وائٹ باکس کا نظریہ لاگو کرتے ہیں اور اسمارٹ کنٹریکٹ ایپلیکیشنز کی نچلے درجے کی نمائندگیوں پر انحصار کرتے ہیں، جیسے پروگرام ٹریس اور کنٹرول فلو گرافسopens in a new tab، تاکہ کنٹریکٹ کے نفاذ سے متعلق خصوصیات کے بارے میں استدلال کیا جا سکے۔

نچلے درجے کے ماڈلز کو مثالی سمجھا جاتا ہے کیونکہ وہ ایتھریم کے ایگزیکیوشن ماحول (یعنی، EVM) میں ایک اسمارٹ کنٹریکٹ کے اصل نفاذ کی نمائندگی کرتے ہیں۔ نچلے درجے کی ماڈلنگ تکنیکیں اسمارٹ کنٹریکٹس میں اہم حفاظتی خصوصیات قائم کرنے اور ممکنہ کمزوریوں کا پتہ لگانے میں خاص طور پر مفید ہیں۔

باضابطہ تفصیلات کیا ہے؟

تفصیلات صرف ایک تکنیکی ضرورت ہے جسے ایک خاص سسٹم کو پورا کرنا ضروری ہے۔ پروگرامنگ میں، تفصیلات کسی پروگرام کے نفاذ کے بارے میں عمومی خیالات کی نمائندگی کرتی ہیں (یعنی، پروگرام کو کیا کرنا چاہیے)۔

اسمارٹ کنٹریکٹس کے تناظر میں، باضابطہ تفصیلات سے مراد خصوصیات ہیں—ان ضروریات کی باضابطہ تفصیلات جنہیں کنٹریکٹ کو پورا کرنا ضروری ہے۔ ایسی خصوصیات کو "غیر متغیرات" کے طور پر بیان کیا جاتا ہے اور کنٹریکٹ کے نفاذ کے بارے میں منطقی دعووں کی نمائندگی کرتی ہیں جنہیں ہر ممکن صورت حال میں، بغیر کسی استثناء کے، سچ رہنا چاہیے۔

اس طرح، ہم باضابطہ تفصیلات کو ایک باضابطہ زبان میں لکھے گئے بیانات کے مجموعے کے طور پر سوچ سکتے ہیں جو ایک اسمارٹ کنٹریکٹ کے مطلوبہ نفاذ کو بیان کرتے ہیں۔ تفصیلات ایک کنٹریکٹ کی خصوصیات کا احاطہ کرتی ہیں اور یہ بتاتی ہیں کہ کنٹریکٹ کو مختلف حالات میں کیسا برتاؤ کرنا چاہیے۔ باضابطہ تصدیق کا مقصد یہ معلوم کرنا ہے کہ آیا ایک اسمارٹ کنٹریکٹ ان خصوصیات (غیر متغیرات) کا مالک ہے اور یہ کہ نفاذ کے دوران ان خصوصیات کی خلاف ورزی نہیں ہوتی ہے۔

اسمارٹ کنٹریکٹس کے محفوظ نفاذ کو تیار کرنے میں باضابطہ تفصیلات بہت اہم ہیں۔ وہ کنٹریکٹس جو غیر متغیرات کو نافذ کرنے میں ناکام رہتے ہیں یا جن کی خصوصیات کی نفاذ کے دوران خلاف ورزی ہوتی ہے، ان کمزوریوں کا شکار ہوتے ہیں جو فعالیت کو نقصان پہنچا سکتی ہیں یا بدنیتی پر مبنی استحصال کا سبب بن سکتی ہیں۔

اسمارٹ کنٹریکٹس کے لئے باضابطہ تفصیلات کی اقسام

باضابطہ تفصیلات پروگرام کے نفاذ کی درستگی کے بارے میں ریاضیاتی استدلال کو ممکن بناتی ہیں۔ باضابطہ ماڈلز کی طرح، باضابطہ تفصیلات یا تو اعلیٰ سطحی خصوصیات یا کنٹریکٹ کے نفاذ کے نچلے درجے کے رویے کو حاصل کر سکتی ہیں۔

باضابطہ تفصیلات پروگرام منطقopens in a new tab کے عناصر کا استعمال کرتے ہوئے حاصل کی جاتی ہیں، جو کسی پروگرام کی خصوصیات کے بارے میں باضابطہ استدلال کی اجازت دیتی ہیں۔ ایک پروگرام منطق کے باضابطہ اصول ہوتے ہیں جو کسی پروگرام کے متوقع رویے کو (ریاضیاتی زبان میں) ظاہر کرتے ہیں۔ باضابطہ تفصیلات بنانے میں مختلف پروگرام منطق استعمال کی جاتی ہیں، بشمول ریچ ایبلٹی منطقopens in a new tab، ٹیمپورل منطقopens in a new tab، اور ہوئر منطقopens in a new tab۔

اسمارٹ کنٹریکٹس کے لئے باضابطہ تفصیلات کو وسیع پیمانے پر یا تو اعلیٰ سطحی یا نچلے درجے کی تفصیلات کے طور پر درجہ بندی کیا جا سکتا ہے۔ اس سے قطع نظر کہ تفصیلات کس زمرے سے تعلق رکھتی ہے، اسے تجزیہ کے تحت سسٹم کی خاصیت کو مناسب اور غیر مبہم طور پر بیان کرنا چاہیے۔

اعلیٰ سطحی تفصیلات

جیسا کہ نام سے ظاہر ہے، ایک اعلیٰ سطحی تفصیلات (جسے "ماڈل پر مبنی تفصیلات" بھی کہا جاتا ہے) ایک پروگرام کے اعلیٰ سطحی رویے کو بیان کرتی ہے۔ اعلیٰ سطحی تفصیلات ایک اسمارٹ کنٹریکٹ کو فائنائٹ اسٹیٹ مشینopens in a new tab (FSM) کے طور پر ماڈل کرتی ہیں، جو آپریشنز انجام دے کر ریاستوں کے درمیان منتقل ہو سکتی ہے، جبکہ ٹیمپورل منطق کا استعمال FSM ماڈل کے لیے باضابطہ خصوصیات کی تعریف کے لیے کیا جاتا ہے۔

ٹیمپورل منطقopens in a new tab "وقت کے لحاظ سے اہل تجاویز کے بارے میں استدلال کے اصول ہیں (مثلاً، "میں ہمیشہ بھوکا رہتا ہوں" یا "میں بالآخر بھوکا ہو جاؤں گا")۔" جب باضابطہ تصدیق پر لاگو کیا جاتا ہے، تو ٹیمپورل منطق کا استعمال اسٹیٹ مشینوں کے طور پر ماڈل کیے گئے سسٹمز کے صحیح رویے کے بارے میں دعوے کرنے کے لیے کیا جاتا ہے۔ خاص طور پر، ایک ٹیمپورل منطق مستقبل کی ان حالتوں کو بیان کرتی ہے جن میں ایک اسمارٹ کنٹریکٹ ہو سکتا ہے اور یہ کہ وہ حالتوں کے درمیان کیسے منتقل ہوتا ہے۔

اعلیٰ سطحی تفصیلات عام طور پر اسمارٹ کنٹریکٹس کے لیے دو اہم ٹیمپورل خصوصیات کو حاصل کرتی ہیں: حفاظت اور لائیونیس۔ حفاظتی خصوصیات اس خیال کی نمائندگی کرتی ہیں کہ "کچھ بھی برا کبھی نہیں ہوتا" اور عام طور پر غیر متغیر ہونے کا اظہار کرتی ہیں۔ ایک حفاظتی خصوصیت عمومی سافٹ ویئر کی ضروریات کی وضاحت کر سکتی ہے، جیسے ڈیڈ لاکopens in a new tab سے آزادی، یا کنٹریکٹس کے لیے ڈومین-مخصوص خصوصیات کا اظہار کر سکتی ہے (مثلاً، فنکشنز کے لیے رسائی کنٹرول پر غیر متغیر، ریاستی متغیرات کی قابل قبول قدریں، یا ٹوکن ٹرانسفر کے لیے شرائط)۔

مثال کے طور پر یہ حفاظتی ضرورت لیں جو ERC-20 ٹوکن کنٹریکٹس میں transfer() یا transferFrom() کے استعمال کے لیے شرائط کا احاطہ کرتی ہے: "ایک بھیجنے والے کا بیلنس بھیجے جانے والے ٹوکنز کی درخواست کردہ رقم سے کبھی کم نہیں ہوتا ہے۔"۔ کنٹریکٹ کے ایک غیر متغیر کی اس قدرتی زبان کی تفصیل کو ایک باضابطہ (ریاضیاتی) تفصیلات میں ترجمہ کیا جا سکتا ہے، جس کی پھر سختی سے درستگی کی جانچ کی جا سکتی ہے۔

لائیونیس خصوصیات اس بات پر زور دیتی ہیں کہ "کچھ اچھا بالآخر ہوتا ہے" اور کنٹریکٹ کی مختلف حالتوں میں ترقی کرنے کی صلاحیت سے متعلق ہیں۔ لائیونیس کی خاصیت کی ایک مثال "لیکویڈیٹی" ہے، جو ایک کنٹریکٹ کی درخواست پر صارفین کو اپنے بیلنس منتقل کرنے کی صلاحیت سے مراد ہے۔ اگر اس خاصیت کی خلاف ورزی کی جاتی ہے، تو صارف کنٹریکٹ میں محفوظ اثاثے واپس نہیں لے پائیں گے، جیسا کہ پیریٹی والیٹ کے واقعےopens in a new tab میں ہوا تھا۔

نچلے درجے کی تفصیلات

اعلیٰ سطحی تفصیلات ایک کنٹریکٹ کے فائنائٹ-اسٹیٹ ماڈل کو نقطہ آغاز کے طور پر لیتی ہیں اور اس ماڈل کی مطلوبہ خصوصیات کی وضاحت کرتی ہیں۔ اس کے برعکس، نچلے درجے کی تفصیلات (جنہیں "پراپرٹی پر مبنی تفصیلات" بھی کہا جاتا ہے) اکثر پروگراموں (اسمارٹ کنٹریکٹس) کو ریاضیاتی افعال کے مجموعے پر مشتمل نظام کے طور پر ماڈل کرتی ہیں اور ایسے نظاموں کے صحیح رویے کو بیان کرتی ہیں۔

آسان الفاظ میں، نچلے درجے کی تفصیلات پروگرام ٹریس کا تجزیہ کرتی ہیں اور ان ٹریسز پر ایک اسمارٹ کنٹریکٹ کی خصوصیات کی وضاحت کرنے کی کوشش کرتی ہیں۔ ٹریس سے مراد فنکشن کے نفاذ کی ترتیب ہے جو ایک اسمارٹ کنٹریکٹ کی حالت کو تبدیل کرتی ہے؛ لہذا، نچلے درجے کی تفصیلات کنٹریکٹ کے اندرونی نفاذ کے لیے ضروریات کی وضاحت میں مدد کرتی ہیں۔

نچلے درجے کی باضابطہ تفصیلات ہوئر-اسٹائل خصوصیات یا نفاذ کے راستوں پر غیر متغیرات کے طور پر دی جا سکتی ہیں۔

ہوئر-اسٹائل خصوصیات

ہوئر منطقopens in a new tab پروگراموں کی درستگی کے بارے میں استدلال کے لیے باضابطہ اصولوں کا ایک سیٹ فراہم کرتی ہے، بشمول اسمارٹ کنٹریکٹس۔ ایک ہوئر-اسٹائل خاصیت کو ہوئر ٹرپل {P}c{Q} سے ظاہر کیا جاتا ہے، جہاں c ایک پروگرام ہے اور P اور Q c (یعنی، پروگرام) کی حالت پر پیشین گوئیاں ہیں، جنہیں باضابطہ طور پر بالترتیب پری کنڈیشنز اور پوسٹ کنڈیشنز کے طور پر بیان کیا گیا ہے۔

ایک پری کنڈیشن ایک پیشین گوئی ہے جو کسی فنکشن کے صحیح نفاذ کے لیے درکار شرائط کو بیان کرتی ہے؛ کنٹریکٹ میں کال کرنے والے صارفین کو اس ضرورت کو پورا کرنا ضروری ہے۔ ایک پوسٹ کنڈیشن ایک پیشین گوئی ہے جو اس حالت کو بیان کرتی ہے جسے ایک فنکشن صحیح طریقے سے نافذ ہونے پر قائم کرتا ہے؛ صارفین فنکشن میں کال کرنے کے بعد اس حالت کے سچ ہونے کی توقع کر سکتے ہیں۔ ہوئر منطق میں ایک غیر متغیر ایک پیشین گوئی ہے جو کسی فنکشن کے نفاذ سے محفوظ رہتی ہے (یعنی، یہ تبدیل نہیں ہوتی)۔

ہوئر-اسٹائل تفصیلات یا تو جزوی درستگی یا کل درستگی کی ضمانت دے سکتی ہیں۔ کنٹریکٹ فنکشن کا نفاذ "جزوی طور پر درست" ہے اگر فنکشن کے نافذ ہونے سے پہلے پری کنڈیشن سچ ثابت ہو، اور اگر نفاذ ختم ہو جائے تو پوسٹ کنڈیشن بھی سچ ہو۔ کل درستگی کا ثبوت اس وقت حاصل ہوتا ہے جب فنکشن کے نفاذ سے پہلے ایک پری کنڈیشن سچ ہو، نفاذ کے ختم ہونے کی ضمانت ہو اور جب ایسا ہوتا ہے تو پوسٹ کنڈیشن سچ ثابت ہوتی ہے۔

کل درستگی کا ثبوت حاصل کرنا مشکل ہے کیونکہ کچھ نفاذ ختم ہونے سے پہلے تاخیر کر سکتے ہیں، یا کبھی ختم ہی نہیں ہوتے۔ اس کے باوجود، یہ سوال کہ آیا نفاذ ختم ہوتا ہے، قابل بحث ہے کیونکہ ایتھریم کا گیس میکانزم لامحدود پروگرام لوپس کو روکتا ہے (نفاذ یا تو کامیابی سے ختم ہو جاتا ہے یا 'آؤٹ آف گیس' کی خرابی کی وجہ سے ختم ہو جاتا ہے)۔

ہوئر منطق کا استعمال کرتے ہوئے بنائی گئی اسمارٹ کنٹریکٹ کی تفصیلات میں ایک کنٹریکٹ میں فنکشنز اور لوپس کے نفاذ کے لیے پری کنڈیشنز، پوسٹ کنڈیشنز، اور غیر متغیرات کی تعریف کی جائے گی۔ پری کنڈیشنز میں اکثر کسی فنکشن میں غلط ان پٹ کا امکان شامل ہوتا ہے، جبکہ پوسٹ کنڈیشنز ایسے ان پٹس پر متوقع ردعمل کو بیان کرتی ہیں (مثلاً، ایک مخصوص استثناء پھینکنا)۔ اس طریقے سے ہوئر-اسٹائل خصوصیات کنٹریکٹ کے نفاذ کی درستگی کو یقینی بنانے میں مؤثر ہیں۔

بہت سے باضابطہ تصدیقی فریم ورک فنکشنز کی معنوی درستگی کو ثابت کرنے کے لیے ہوئر-اسٹائل تفصیلات کا استعمال کرتے ہیں۔ سولیڈیٹی میں require اور assert بیانات کا استعمال کرکے ہوئر-اسٹائل خصوصیات (بطور دعوے) کو براہ راست کنٹریکٹ کوڈ میں شامل کرنا بھی ممکن ہے۔

require بیانات ایک پری کنڈیشن یا غیر متغیر کا اظہار کرتے ہیں اور اکثر صارف کے ان پٹ کی توثیق کے لیے استعمال ہوتے ہیں، جبکہ assert حفاظت کے لیے ضروری ایک پوسٹ کنڈیشن کو حاصل کرتا ہے۔ مثال کے طور پر، فنکشنز کے لیے مناسب رسائی کنٹرول (حفاظتی خاصیت کی ایک مثال) کال کرنے والے اکاؤنٹ کی شناخت پر پری کنڈیشن چیک کے طور پر require کا استعمال کرکے حاصل کیا جا سکتا ہے۔ اسی طرح، ایک کنٹریکٹ میں ریاستی متغیرات کی قابل قبول قدروں پر ایک غیر متغیر (مثلاً، گردش میں ٹوکنز کی کل تعداد) کو assert کا استعمال کرکے خلاف ورزی سے بچایا جا سکتا ہے تاکہ فنکشن کے نفاذ کے بعد کنٹریکٹ کی حالت کی تصدیق کی جا سکے۔

ٹریس-سطح کی خصوصیات

ٹریس پر مبنی تفصیلات ان کارروائیوں کو بیان کرتی ہیں جو ایک کنٹریکٹ کو مختلف حالتوں کے درمیان منتقل کرتی ہیں اور ان کارروائیوں کے درمیان تعلقات کو۔ جیسا کہ پہلے وضاحت کی گئی ہے، ٹریس کارروائیوں کی ترتیب ہیں جو ایک کنٹریکٹ کی حالت کو ایک خاص طریقے سے تبدیل کرتی ہیں۔

یہ نقطہ نظر اسمارٹ کنٹریکٹس کے ماڈل پر انحصار کرتا ہے جو اسٹیٹ-ٹرانزیشن سسٹمز کے طور پر ہیں جن میں کچھ پہلے سے طے شدہ حالتیں ہیں (ریاستی متغیرات کے ذریعہ بیان کردہ) اور ساتھ ہی پہلے سے طے شدہ ٹرانزیشنز کا ایک سیٹ ہے (کنٹریکٹ فنکشنز کے ذریعہ بیان کردہ)۔ مزید برآں، ایک کنٹرول فلو گرافopens in a new tab (CFG)، جو کسی پروگرام کے نفاذ کے بہاؤ کی ایک گرافیکل نمائندگی ہے، اکثر کنٹریکٹ کی آپریشنل سیمانٹکس کو بیان کرنے کے لیے استعمال ہوتا ہے۔ یہاں، ہر ٹریس کو کنٹرول فلو گراف پر ایک راستے کے طور پر ظاہر کیا جاتا ہے۔

بنیادی طور پر، ٹریس-سطح کی تفصیلات اسمارٹ کنٹریکٹس میں اندرونی نفاذ کے نمونوں کے بارے میں استدلال کرنے کے لیے استعمال ہوتی ہیں۔ ٹریس-سطح کی تفصیلات بنا کر، ہم ایک اسمارٹ کنٹریکٹ کے لیے قابل قبول نفاذ کے راستے (یعنی، ریاستی منتقلی) پر زور دیتے ہیں۔ علامتی نفاذ جیسی تکنیکوں کا استعمال کرتے ہوئے، ہم باضابطہ طور پر تصدیق کر سکتے ہیں کہ نفاذ کبھی بھی ایسے راستے پر نہیں چلتا جو باضابطہ ماڈل میں بیان نہیں کیا گیا ہے۔

آئیے ایک DAO کنٹریکٹ کی مثال استعمال کرتے ہیں جس میں ٹریس-سطح کی خصوصیات کو بیان کرنے کے لیے کچھ عوامی طور پر قابل رسائی فنکشنز ہیں۔ یہاں، ہم فرض کرتے ہیں کہ DAO کنٹریکٹ صارفین کو درج ذیل کارروائیاں کرنے کی اجازت دیتا ہے:

فنڈز جمع کروائیں
فنڈز جمع کروانے کے بعد کسی تجویز پر ووٹ دیں
اگر وہ کسی تجویز پر ووٹ نہیں دیتے ہیں تو رقم کی واپسی کا دعویٰ کریں

مثال کے طور پر ٹریس-سطح کی خصوصیات یہ ہو سکتی ہیں "وہ صارفین جو فنڈز جمع نہیں کرواتے وہ کسی تجویز پر ووٹ نہیں دے سکتے" یا "وہ صارفین جو کسی تجویز پر ووٹ نہیں دیتے انہیں ہمیشہ رقم کی واپسی کا دعویٰ کرنے کے قابل ہونا چاہئے"۔ دونوں خصوصیات نفاذ کی ترجیحی ترتیبوں پر زور دیتی ہیں (ووٹنگ فنڈز جمع کروانے سے پہلے نہیں ہو سکتی اور کسی تجویز پر ووٹ دینے کے بعد رقم کی واپسی کا دعویٰ نہیں کیا جا سکتا)۔

اسمارٹ کنٹریکٹس کی باضابطہ تصدیق کے لیے تکنیکیں

ماڈل چیکنگ

ماڈل چیکنگ ایک باضابطہ تصدیقی تکنیک ہے جس میں ایک الگورتھم ایک اسمارٹ کنٹریکٹ کے باضابطہ ماڈل کو اس کی تفصیلات کے خلاف چیک کرتا ہے۔ ماڈل چیکنگ میں اسمارٹ کنٹریکٹس کو اکثر اسٹیٹ-ٹرانزیشن سسٹمز کے طور پر ظاہر کیا جاتا ہے، جبکہ قابل اجازت کنٹریکٹ کی حالتوں پر خصوصیات کو ٹیمپورل منطق کا استعمال کرتے ہوئے بیان کیا جاتا ہے۔

ماڈل چیکنگ کے لیے ایک سسٹم (یعنی، ایک کنٹریکٹ) کی ایک خلاصہ ریاضیاتی نمائندگی بنانے کی ضرورت ہوتی ہے اور اس سسٹم کی خصوصیات کو تجاویزی منطقopens in a new tab پر مبنی فارمولوں کا استعمال کرتے ہوئے ظاہر کرنے کی ضرورت ہوتی ہے۔ یہ ماڈل چیکنگ الگورتھم کے کام کو آسان بناتا ہے، یعنی یہ ثابت کرنا کہ ایک ریاضیاتی ماڈل دیے گئے منطقی فارمولے کو پورا کرتا ہے۔

باضابطہ تصدیق میں ماڈل چیکنگ بنیادی طور پر ان وقتی خصوصیات کا جائزہ لینے کے لیے استعمال کی جاتی ہے جو وقت کے ساتھ ساتھ کنٹریکٹ کے رویے کو بیان کرتی ہیں۔ اسمارٹ کنٹریکٹس کے لیے وقتی خصوصیات میں حفاظت اور لائیونیس شامل ہیں، جن کی ہم نے پہلے وضاحت کی تھی۔

مثال کے طور پر، رسائی کنٹرول سے متعلق ایک حفاظتی خاصیت (مثلاً، صرف کنٹریکٹ کا مالک ہی selfdestruct کو کال کر سکتا ہے) کو باضابطہ منطق میں لکھا جا سکتا ہے۔ اس کے بعد، ماڈل چیکنگ الگورتھم یہ تصدیق کر سکتا ہے کہ آیا کنٹریکٹ اس باضابطہ تفصیلات کو پورا کرتا ہے۔

ماڈل چیکنگ اسٹیٹ اسپیس ایکسپلوریشن کا استعمال کرتی ہے، جس میں ایک اسمارٹ کنٹریکٹ کی تمام ممکنہ حالتوں کی تعمیر اور ان قابل رسائی حالتوں کو تلاش کرنے کی کوشش شامل ہے جو خاصیت کی خلاف ورزیوں کا باعث بنتی ہیں۔ تاہم، یہ لامحدود تعداد میں حالتوں کا باعث بن سکتا ہے (جسے "اسٹیٹ ایکسپلوژن پرابلم" کہا جاتا ہے)، اس لیے ماڈل چیکرز اسمارٹ کنٹریکٹس کے موثر تجزیے کو ممکن بنانے کے لیے خلاصہ تکنیکوں پر انحصار کرتے ہیں۔

تھیورم کی تصدیق

تھیورم کی تصدیق پروگراموں، بشمول اسمارٹ کنٹریکٹس، کی درستگی کے بارے میں ریاضیاتی طور پر استدلال کرنے کا ایک طریقہ ہے۔ اس میں کنٹریکٹ کے سسٹم کے ماڈل اور اس کی تفصیلات کو ریاضیاتی فارمولوں (منطقی بیانات) میں تبدیل کرنا شامل ہے۔

تھیورم کی تصدیق کا مقصد ان بیانات کے درمیان منطقی مساوات کی تصدیق کرنا ہے۔ "منطقی مساوات" (جسے "منطقی دو طرفہ مضمرات" بھی کہا جاتا ہے) دو بیانات کے درمیان ایک قسم کا رشتہ ہے جس کے تحت پہلا بیان سچ ہوتا ہے اگر اور صرف اگر دوسرا بیان سچ ہو۔

کنٹریکٹ کے ماڈل اور اس کی خاصیت کے بارے میں بیانات کے درمیان مطلوبہ رشتہ (منطقی مساوات) کو ایک قابل ثبوت بیان (جسے تھیورم کہا جاتا ہے) کے طور پر وضع کیا جاتا ہے۔ استدلال کے ایک باضابطہ نظام کا استعمال کرتے ہوئے، خودکار تھیورم پروور تھیورم کی صداقت کی تصدیق کر سکتا ہے۔ دوسرے الفاظ میں، ایک تھیورم پروور حتمی طور پر یہ ثابت کر سکتا ہے کہ ایک اسمارٹ کنٹریکٹ کا ماڈل اس کی تفصیلات سے بالکل میل کھاتا ہے۔

جبکہ ماڈل چیکنگ کنٹریکٹس کو محدود حالتوں کے ساتھ ٹرانزیشن سسٹم کے طور پر ماڈل کرتی ہے، تھیورم کی تصدیق لامحدود-حالت والے نظاموں کے تجزیے کو سنبھال سکتی ہے۔ تاہم، اس کا مطلب یہ ہے کہ ایک خودکار تھیورم پروور ہمیشہ یہ نہیں جان سکتا کہ آیا کوئی منطقی مسئلہ "فیصلہ کن" ہے یا نہیں۔

نتیجتاً، درستگی کے ثبوت حاصل کرنے میں تھیورم پروور کی رہنمائی کے لیے اکثر انسانی مدد کی ضرورت پڑتی ہے۔ تھیورم کی تصدیق میں انسانی کوششوں کا استعمال اسے ماڈل چیکنگ سے زیادہ مہنگا بناتا ہے، جو کہ مکمل طور پر خودکار ہے۔

علامتی نفاذ

علامتی نفاذ ایک اسمارٹ کنٹریکٹ کا تجزیہ کرنے کا ایک طریقہ ہے جس میں فنکشنز کو ٹھوس اقدار (مثلاً، x == 5) کی بجائے علامتی اقدار (مثلاً، x > 5) کا استعمال کرتے ہوئے نافذ کیا جاتا ہے۔ ایک باضابطہ تصدیقی تکنیک کے طور پر، علامتی نفاذ کا استعمال کنٹریکٹ کے کوڈ میں ٹریس-سطح کی خصوصیات کے بارے میں باضابطہ طور پر استدلال کرنے کے لیے کیا جاتا ہے۔

علامتی نفاذ ایک نفاذ کے ٹریس کو علامتی ان پٹ اقدار پر ایک ریاضیاتی فارمولے کے طور پر ظاہر کرتا ہے، جسے بصورت دیگر پاتھ پریڈیکیٹ کہا جاتا ہے۔ ایک SMT سالورopens in a new tab کا استعمال یہ جانچنے کے لیے کیا جاتا ہے کہ آیا کوئی پاتھ پریڈیکیٹ "اطمینان بخش" ہے (یعنی، کیا کوئی ایسی قدر موجود ہے جو فارمولے کو پورا کر سکتی ہے)۔ اگر ایک کمزور راستہ اطمینان بخش ہے، تو SMT سالور ایک ٹھوس قدر پیدا کرے گا جو نفاذ کو اس راستے کی طرف لے جاتا ہے۔

فرض کریں کہ ایک اسمارٹ کنٹریکٹ کا فنکشن ان پٹ کے طور پر ایک uint قدر (x) لیتا ہے اور جب x 5 سے زیادہ اور 10 سے کم ہو تو واپس ہو جاتا ہے۔ x کے لیے ایک ایسی قدر تلاش کرنے کے لیے جو خرابی کو متحرک کرتی ہو، ایک عام ٹیسٹنگ طریقہ کار کا استعمال کرتے ہوئے درجنوں ٹیسٹ کیسز (یا اس سے زیادہ) سے گزرنا پڑے گا بغیر اس یقین دہانی کے کہ واقعی خرابی کو متحرک کرنے والا ان پٹ مل جائے گا۔

اس کے برعکس، ایک علامتی نفاذ کا ٹول فنکشن کو علامتی قدر کے ساتھ نافذ کرے گا: X > 5 ∧ X < 10 (یعنی، x 5 سے بڑا ہے اور x 10 سے کم ہے)۔ اس کے بعد متعلقہ پاتھ پریڈیکیٹ x = X > 5 ∧ X < 10 کو حل کرنے کے لیے ایک SMT سالور کو دیا جائے گا۔ اگر کوئی خاص قدر فارمولہ x = X > 5 ∧ X < 10 کو پورا کرتی ہے، تو SMT سالور اس کا حساب لگائے گا—مثال کے طور پر، سالور x کے لیے 7 کی قدر پیدا کر سکتا ہے۔

چونکہ علامتی نفاذ کسی پروگرام کے ان پٹس پر انحصار کرتا ہے، اور تمام قابل رسائی حالتوں کو دریافت کرنے کے لیے ان پٹس کا سیٹ ممکنہ طور پر لامحدود ہے، یہ اب بھی ٹیسٹنگ کی ایک شکل ہے۔ تاہم، جیسا کہ مثال میں دکھایا گیا ہے، علامتی نفاذ ان پٹس کو تلاش کرنے کے لیے باقاعدہ ٹیسٹنگ سے زیادہ موثر ہے جو خاصیت کی خلاف ورزیوں کو متحرک کرتے ہیں۔

مزید برآں، علامتی نفاذ دیگر پراپرٹی پر مبنی تکنیکوں (مثلاً، فزنگ) کے مقابلے میں کم غلط مثبت پیدا کرتا ہے جو کسی فنکشن کے لیے تصادفی طور پر ان پٹ تیار کرتی ہیں۔ اگر علامتی نفاذ کے دوران کسی خرابی کی حالت کو متحرک کیا جاتا ہے، تو خرابی کو متحرک کرنے والی ایک ٹھوس قدر پیدا کرنا اور مسئلے کو دوبارہ پیش کرنا ممکن ہے۔

علامتی نفاذ درستگی کا کچھ حد تک ریاضیاتی ثبوت بھی فراہم کر سکتا ہے۔ اوور فلو سے تحفظ کے ساتھ کنٹریکٹ فنکشن کی درج ذیل مثال پر غور کریں:

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  return z;
8}

ایک نفاذ کا ٹریس جو ایک انٹیجر اوور فلو کا باعث بنتا ہے اسے فارمولہ پورا کرنے کی ضرورت ہوگی: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) اس طرح کے فارمولے کو حل کرنے کا امکان نہیں ہے، لہذا یہ اس بات کا ریاضیاتی ثبوت فراہم کرتا ہے کہ فنکشن safe_add کبھی بھی اوور فلو نہیں ہوتا ہے۔

اسمارٹ کنٹریکٹس کے لیے باضابطہ تصدیق کیوں استعمال کریں؟

قابل اعتمادی کی ضرورت

باضابطہ تصدیق کا استعمال حفاظت کے لیے اہم نظاموں کی درستگی کا اندازہ لگانے کے لیے کیا جاتا ہے جن کی ناکامی کے تباہ کن نتائج ہو سکتے ہیں، جیسے موت، چوٹ، یا مالی بربادی۔ اسمارٹ کنٹریکٹس اعلیٰ قدر والی ایپلی کیشنز ہیں جو بہت بڑی مقدار میں قدر کو کنٹرول کرتی ہیں، اور ڈیزائن میں معمولی غلطیاں صارفین کے لیے ناقابل تلافی نقصاناتopens in a new tab کا باعث بن سکتی ہیں۔ تاہم، تعیناتی سے پہلے کسی کنٹریکٹ کی باضابطہ تصدیق کرنے سے اس بات کی ضمانت بڑھ سکتی ہے کہ یہ بلاک چین پر چلنے کے بعد توقع کے مطابق کام کرے گا۔

کسی بھی اسمارٹ کنٹریکٹ میں قابل اعتمادی ایک انتہائی مطلوبہ خوبی ہے، خاص طور پر اس لیے کہ ایتھریم ورچوئل مشین (EVM) میں تعینات کوڈ عام طور پر ناقابل تغیر ہوتا ہے۔ چونکہ لانچ کے بعد اپ گریڈ آسانی سے دستیاب نہیں ہوتے، کنٹریکٹس کی قابل اعتمادی کی ضمانت دینے کی ضرورت باضابطہ تصدیق کو ضروری بناتی ہے۔ باضابطہ تصدیق مشکل مسائل کا پتہ لگانے کے قابل ہے، جیسے انٹیجر انڈر فلو اور اوور فلو، ری-اینٹرینسی، اور خراب گیس کی اصلاح، جو آڈیٹرز اور ٹیسٹرز سے بچ سکتے ہیں۔

فعالیاتی درستگی کو ثابت کریں

پروگرام کی جانچ یہ ثابت کرنے کا سب سے عام طریقہ ہے کہ ایک اسمارٹ کنٹریکٹ کچھ ضروریات کو پورا کرتا ہے۔ اس میں ایک کنٹریکٹ کو اس ڈیٹا کے نمونے کے ساتھ نافذ کرنا شامل ہے جسے اسے سنبھالنے کی توقع ہے اور اس کے رویے کا تجزیہ کرنا۔ اگر کنٹریکٹ نمونے کے ڈیٹا کے لیے متوقع نتائج واپس کرتا ہے، تو ڈیولپرز کے پاس اس کی درستگی کا معروضی ثبوت ہوتا ہے۔

تاہم، یہ نقطہ نظر ان ان پٹ اقدار کے لیے درست نفاذ کو ثابت نہیں کر سکتا جو نمونے کا حصہ نہیں ہیں۔ لہذا، کسی کنٹریکٹ کی جانچ کیڑوں کا پتہ لگانے میں مدد کر سکتی ہے (یعنی، اگر کچھ کوڈ پاتھ نفاذ کے دوران مطلوبہ نتائج واپس کرنے میں ناکام ہو جاتے ہیں)، لیکن یہ حتمی طور پر کیڑوں کی عدم موجودگی کو ثابت نہیں کر سکتی۔

اس کے برعکس، باضابطہ تصدیق باضابطہ طور پر یہ ثابت کر سکتی ہے کہ ایک اسمارٹ کنٹریکٹ لامحدود حد تک نفاذ کے لیے ضروریات کو پورا کرتا ہے بغیر کنٹریکٹ کو چلائے۔ اس کے لیے ایک باضابطہ تفصیلات بنانے کی ضرورت ہوتی ہے جو کنٹریکٹ کے صحیح رویوں کو ٹھیک ٹھیک بیان کرتی ہے اور کنٹریکٹ کے نظام کا ایک باضابطہ (ریاضیاتی) ماڈل تیار کرتی ہے۔ پھر ہم کنٹریکٹ کے ماڈل اور اس کی تفصیلات کے درمیان مطابقت کی جانچ کے لیے ایک باضابطہ ثبوت کے طریقہ کار کی پیروی کر سکتے ہیں۔

باضابطہ تصدیق کے ساتھ، یہ سوال کہ آیا کنٹریکٹ کی کاروباری منطق ضروریات کو پورا کرتی ہے، ایک ریاضیاتی تجویز ہے جسے ثابت یا رد کیا جا سکتا ہے۔ باضابطہ طور پر ایک تجویز کو ثابت کرکے، ہم محدود تعداد میں اقدامات کے ساتھ لامحدود تعداد میں ٹیسٹ کیسز کی تصدیق کر سکتے ہیں۔ اس طریقے سے باضابطہ تصدیق کے پاس یہ ثابت کرنے کے بہتر امکانات ہیں کہ ایک کنٹریکٹ ایک تفصیلات کے حوالے سے فعالیاتی طور پر درست ہے۔

مثالی تصدیقی اہداف

ایک تصدیقی ہدف اس نظام کو بیان کرتا ہے جس کی باضابطہ تصدیق کی جانی ہے۔ باضابطہ تصدیق کا بہترین استعمال "ایمبیڈڈ سسٹمز" (سافٹ ویئر کے چھوٹے، سادہ ٹکڑے جو ایک بڑے نظام کا حصہ بنتے ہیں) میں ہوتا ہے۔ وہ خصوصی ڈومینز کے لیے بھی مثالی ہیں جن کے اصول کم ہوتے ہیں، کیونکہ اس سے ڈومین-مخصوص خصوصیات کی تصدیق کے لیے ٹولز میں ترمیم کرنا آسان ہو جاتا ہے۔

اسمارٹ کنٹریکٹس — کم از کم، کچھ حد تک — دونوں ضروریات کو پورا کرتے ہیں۔ مثال کے طور پر، ایتھریم کنٹریکٹس کا چھوٹا سائز انہیں باضابطہ تصدیق کے لیے موزوں بناتا ہے۔ اسی طرح، EVM سادہ اصولوں کی پیروی کرتا ہے، جو EVM میں چلنے والے پروگراموں کے لیے معنوی خصوصیات کی وضاحت اور تصدیق کو آسان بناتا ہے۔

تیز تر ترقیاتی سائیکل

باضابطہ تصدیق کی تکنیکیں، جیسے ماڈل چیکنگ اور علامتی نفاذ، عام طور پر اسمارٹ کنٹریکٹ کوڈ کے باقاعدہ تجزیے (جانچ یا آڈٹ کے دوران کیے جانے والے) سے زیادہ موثر ہیں۔ اس کی وجہ یہ ہے کہ باضابطہ تصدیق دعووں کی جانچ کے لیے علامتی اقدار پر انحصار کرتی ہے ("کیا ہوگا اگر کوئی صارف n ایتھر نکالنے کی کوشش کرے؟") جانچ کے برعکس جو ٹھوس اقدار کا استعمال کرتی ہے ("کیا ہوگا اگر کوئی صارف 5 ایتھر نکالنے کی کوشش کرے؟")۔

علامتی ان پٹ متغیرات ٹھوس اقدار کی متعدد کلاسوں کا احاطہ کر سکتے ہیں، لہذا باضابطہ تصدیق کے طریقے کم وقت میں زیادہ کوڈ کوریج کا وعدہ کرتے ہیں۔ جب موثر طریقے سے استعمال کیا جائے تو، باضابطہ تصدیق ڈیولپرز کے لیے ترقیاتی سائیکل کو تیز کر سکتی ہے۔

باضابطہ تصدیق مہنگی ڈیزائن کی غلطیوں کو کم کرکے غیر مرکزی ایپلی کیشنز (dapps) بنانے کے عمل کو بھی بہتر بناتی ہے۔ کمزوریوں کو ٹھیک کرنے کے لیے کنٹریکٹس کو اپ گریڈ کرنے (جہاں ممکن ہو) کے لیے کوڈ بیسز کی وسیع پیمانے پر دوبارہ تحریر اور ترقی پر زیادہ محنت کی ضرورت ہوتی ہے۔ باضابطہ تصدیق کنٹریکٹ کے نفاذ میں بہت سی غلطیوں کا پتہ لگا سکتی ہے جو ٹیسٹرز اور آڈیٹرز سے بچ سکتی ہیں اور کنٹریکٹ کو تعینات کرنے سے پہلے ان مسائل کو ٹھیک کرنے کا کافی موقع فراہم کرتی ہے۔

باضابطہ تصدیق کے نقصانات

دستی مزدوری کی لاگت

باضابطہ تصدیق، خاص طور پر نیم خودکار تصدیق جس میں ایک انسان درستگی کے ثبوت حاصل کرنے کے لیے پروور کی رہنمائی کرتا ہے، کافی دستی مزدوری کی ضرورت ہوتی ہے۔ مزید برآں، باضابطہ تفصیلات بنانا ایک پیچیدہ سرگرمی ہے جس کے لیے اعلیٰ سطح کی مہارت کی ضرورت ہوتی ہے۔

یہ عوامل (کوشش اور مہارت) باضابطہ تصدیق کو کنٹریکٹس میں درستگی کا اندازہ لگانے کے معمول کے طریقوں، جیسے جانچ اور آڈٹ، کے مقابلے میں زیادہ مطالبہ کرنے والا اور مہنگا بناتے ہیں۔ اس کے باوجود، ایک مکمل تصدیقی آڈٹ کی قیمت ادا کرنا عملی ہے، اسمارٹ کنٹریکٹ کے نفاذ میں غلطیوں کی لاگت کو دیکھتے ہوئے۔

غلط منفی

باضابطہ تصدیق صرف یہ جانچ سکتی ہے کہ آیا اسمارٹ کنٹریکٹ کا نفاذ باضابطہ تفصیلات سے میل کھاتا ہے۔ اس طرح، یہ یقینی بنانا ضروری ہے کہ تفصیلات ایک اسمارٹ کنٹریکٹ کے متوقع رویوں کو صحیح طریقے سے بیان کرے۔

اگر تفصیلات خراب طریقے سے لکھی گئی ہیں، تو خصوصیات کی خلاف ورزیوں — جو کمزور نفاذ کی طرف اشارہ کرتی ہیں — کا باضابطہ تصدیقی آڈٹ کے ذریعے پتہ نہیں لگایا جا سکتا۔ اس معاملے میں، ایک ڈیولپر غلطی سے یہ فرض کر سکتا ہے کہ کنٹریکٹ بگ سے پاک ہے۔

کارکردگی کے مسائل

باضابطہ تصدیق میں کارکردگی کے متعدد مسائل کا سامنا کرنا پڑتا ہے۔ مثال کے طور پر، ماڈل چیکنگ اور علامتی جانچ کے دوران بالترتیب سامنے آنے والے اسٹیٹ اور پاتھ ایکسپلوژن کے مسائل، تصدیقی طریقہ کار کو متاثر کر سکتے ہیں۔ اس کے علاوہ، باضابطہ تصدیق کے ٹولز اکثر اپنی بنیادی تہہ میں SMT سالورز اور دیگر رکاوٹ حل کرنے والے استعمال کرتے ہیں، اور یہ سالورز کمپیوٹیشنل طور پر انتہائی شدید طریقہ کار پر انحصار کرتے ہیں۔

اس کے علاوہ، پروگرام کی تصدیق کرنے والوں کے لیے یہ ہمیشہ ممکن نہیں ہوتا کہ وہ یہ تعین کر سکیں کہ آیا کوئی خاصیت (جسے منطقی فارمولے کے طور پر بیان کیا گیا ہے) پوری کی جا سکتی ہے یا نہیں ( "فیصلہ کرنے کا مسئلہopens in a new tab") کیونکہ ایک پروگرام کبھی ختم نہیں ہو سکتا۔ اس طرح، کسی کنٹریکٹ کے لیے کچھ خصوصیات کو ثابت کرنا ناممکن ہو سکتا ہے چاہے وہ اچھی طرح سے بیان کیا گیا ہو۔

ایتھریم اسمارٹ کنٹریکٹس کے لیے باضابطہ تصدیق کے ٹولز

باضابطہ تفصیلات بنانے کے لیے تفصیلات کی زبانیں

Act: Act اسٹوریج اپ ڈیٹس، پری/پوسٹ کنڈیشنز اور کنٹریکٹ انویرینٹس کی تفصیلات کی اجازت دیتا ہے۔ اس کے ٹول سویٹ میں پروف بیک اینڈز بھی ہیں جو Coq, SMT سالورز، یا hevm کے ذریعے بہت سی خصوصیات کو ثابت کرنے کے قابل ہیں۔

Scribble - Scribble اسکربل تفصیلات کی زبان میں کوڈ تشریحات کو ٹھوس دعووں میں تبدیل کرتا ہے جو تفصیلات کی جانچ کرتے ہیں۔

دستاویزاتopens in a new tab

Dafny - Dafny ایک تصدیق کے لیے تیار پروگرامنگ زبان ہے جو کوڈ کی درستگی کے بارے میں استدلال کرنے اور اسے ثابت کرنے کے لیے اعلیٰ سطحی تشریحات پر انحصار کرتی ہے۔

GitHubopens in a new tab

درستگی کی جانچ کے لیے پروگرام کی تصدیق کرنے والے

Certora Prover - Certora Prover اسمارٹ کنٹریکٹس میں کوڈ کی درستگی کی جانچ کے لیے ایک خودکار باضابطہ تصدیقی ٹول ہے۔ تفصیلات CVL (Certora Verification Language) میں لکھی جاتی ہیں، جس میں جامد تجزیہ اور رکاوٹ حل کرنے کے امتزاج کا استعمال کرتے ہوئے خاصیت کی خلاف ورزیوں کا پتہ لگایا جاتا ہے۔

Solidity SMTChecker - Solidity کا SMTChecker SMT (Satisfiability Modulo Theories) اور Horn solving پر مبنی ایک بلٹ ان ماڈل چیکر ہے۔ یہ تصدیق کرتا ہے کہ آیا کنٹریکٹ کا سورس کوڈ تالیف کے دوران تفصیلات سے میل کھاتا ہے اور جامد طور پر حفاظتی خصوصیات کی خلاف ورزیوں کی جانچ کرتا ہے۔

GitHubopens in a new tab

solc-verify - solc-verify سولیڈیٹی کمپائلر کا ایک توسیعی ورژن ہے جو تشریحات اور ماڈیولر پروگرام کی تصدیق کا استعمال کرتے ہوئے سولیڈیٹی کوڈ پر خودکار باضابطہ تصدیق انجام دے سکتا ہے۔

GitHubopens in a new tab

KEVM - KEVM ایتھریم ورچوئل مشین (EVM) کی ایک باضابطہ سیمانٹکس ہے جو K فریم ورک میں لکھی گئی ہے۔ KEVM قابل عمل ہے اور رسائی کی منطق کا استعمال کرتے ہوئے کچھ خاصیت سے متعلق دعووں کو ثابت کر سکتا ہے۔

تھیورم کی تصدیق کے لیے منطقی فریم ورک

Isabelle - Isabelle/HOL ایک پروف اسسٹنٹ ہے جو ریاضیاتی فارمولوں کو باضابطہ زبان میں ظاہر کرنے کی اجازت دیتا ہے اور ان فارمولوں کو ثابت کرنے کے لیے ٹولز فراہم کرتا ہے۔ مرکزی اطلاق ریاضیاتی ثبوتوں کی رسمی شکل دینا ہے اور خاص طور پر باضابطہ تصدیق، جس میں کمپیوٹر ہارڈ ویئر یا سافٹ ویئر کی درستگی کو ثابت کرنا اور کمپیوٹر زبانوں اور پروٹوکولز کی خصوصیات کو ثابت کرنا شامل ہے۔

Rocq - Rocq ایک انٹرایکٹو تھیورم پروور ہے جو آپ کو تھیورمز کا استعمال کرتے ہوئے پروگراموں کی تعریف کرنے اور درستگی کے مشین-چیک شدہ ثبوتوں کو انٹرایکٹو طور پر تیار کرنے دیتا ہے۔

اسمارٹ کنٹریکٹس میں کمزور نمونوں کا پتہ لگانے کے لیے علامتی نفاذ پر مبنی ٹولز

Manticore - علامتی نفاذ پر مبنی EVM بائٹ کوڈ تجزیہ ٹول۔

hevm - hevm EVM بائٹ کوڈ کے لیے ایک علامتی نفاذ انجن اور مساوات چیکر ہے۔

GitHubopens in a new tab

Mythril - ایتھریم اسمارٹ کنٹریکٹس میں کمزوریوں کا پتہ لگانے کے لیے ایک علامتی نفاذ کا ٹول