اسمارٹ کانٹریکٹس کی فارمل ویریفکیشن

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

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

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

فارمل ویریفکیشن کیا ہے؟

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

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

فارمل ماڈل کیا ہے؟

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

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

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

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

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

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

فارمل تصریح کیا ہے؟

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

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

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

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

اسمارٹ کانٹریکٹس کے لیے فارمل تصریحات کی اقسام

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

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

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

ہائی لیول تصریحات

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

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

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

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

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

لو لیول تصریحات

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

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

لو لیول فارمل تصریحات کو ہور اسٹائل خصوصیات یا ایگزیکیوشن پاتھس پر invariants کے طور پر دیا جا سکتا ہے۔

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

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

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

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

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

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

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

require اسٹیٹمنٹس ایک پری کنڈیشن یا invariant کا اظہار کرتی ہیں اور اکثر صارف کے ان پٹس کی توثیق کے لیے استعمال ہوتی ہیں، جبکہ assert حفاظت کے لیے ضروری پوسٹ کنڈیشن کو حاصل کرتا ہے۔ مثال کے طور پر، فنکشنز کے لیے مناسب ایکسیس کنٹرول (سیفٹی پراپرٹی کی ایک مثال) کو کال کرنے والے اکاؤنٹ کی شناخت پر پری کنڈیشن چیک کے طور پر require کا استعمال کر کے حاصل کیا جا سکتا ہے۔ اسی طرح، کانٹریکٹ میں اسٹیٹ ویری ایبلز کی قابل قبول قدروں پر ایک invariant (مثلاً، گردش میں ٹوکنز کی کل تعداد) کو فنکشن ایگزیکیوشن کے بعد کانٹریکٹ کی اسٹیٹ کی تصدیق کے لیے 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 پیدا کر سکتا ہے۔

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

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

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

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) کا باعث بن سکتی ہیں۔ تاہم، تعیناتی (deployment) سے پہلے کانٹریکٹ کی فارمل طور پر تصدیق کرنا اس بات کی ضمانتوں کو بڑھا سکتا ہے کہ یہ بلاک چین پر چلنے کے بعد توقع کے مطابق کارکردگی دکھائے گا۔

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

فنکشنل درستگی ثابت کریں

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

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

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

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

مثالی ویریفکیشن اہداف

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

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

تیز تر ڈیولپمنٹ سائیکل

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

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

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

فارمل ویریفکیشن کی خامیاں

دستی مشقت کی لاگت

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

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

غلط منفی (False negatives)

فارمل ویریفکیشن صرف یہ جانچ سکتی ہے کہ آیا اسمارٹ کانٹریکٹ کا ایگزیکیوشن فارمل تصریح سے میل کھاتا ہے۔ اس طرح، یہ یقینی بنانا ضروری ہے کہ تصریح اسمارٹ کانٹریکٹ کے متوقع برتاؤ کو مناسب طریقے سے بیان کرتی ہے۔

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

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

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

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

ایتھیریم اسمارٹ کانٹریکٹس کے لیے فارمل ویریفکیشن ٹولز

فارمل تصریحات بنانے کے لیے تصریحی زبانیں

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

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

Documentation (opens in a new tab)

Dafny - Dafny ایک ویریفکیشن کے لیے تیار پروگرامنگ زبان ہے جو کوڈ کی درستگی کے بارے میں استدلال کرنے اور ثابت کرنے کے لیے ہائی لیول اینوٹیشنز پر انحصار کرتی ہے۔

GitHub (opens in a new tab)

درستگی کی جانچ کے لیے پروگرام ویریفائرز

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

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

GitHub (opens in a new tab)

solc-verify - solc-verify سولیڈیٹی کمپائلر کا ایک توسیعی ورژن ہے جو اینوٹیشنز اور ماڈیولر پروگرام ویریفکیشن کا استعمال کرتے ہوئے سولیڈیٹی کوڈ پر خودکار فارمل ویریفکیشن انجام دے سکتا ہے۔

GitHub (opens in a new tab)

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

تھیورم پروونگ کے لیے منطقی فریم ورکس

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

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

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

Manticore - سمبولک ایگزیکیوشن پر مبنی EVM بائٹ کوڈ کے تجزیے کا ایک ٹول۔

hevm - hevm EVM بائٹ کوڈ کے لیے ایک سمبولک ایگزیکیوشن انجن اور ایکوئیویلینس چیکر ہے۔

GitHub (opens in a new tab)

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