سمارٹ کنٹریکٹس کی رسمی تصدیق

صفحہ میں ترمیم کریں

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

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

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

رسمی تصدیق کیا ہے؟

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

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

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

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

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

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

اعلیٰ سطحی ماڈلز سمارٹ کنٹریکٹس اور بیرونی ایجنٹس، جیسے کہ بیرونی ملکیت والے اکاؤنٹس (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 لاجک (opens in a new tab) شامل ہیں۔

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

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

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

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

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

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

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

نچلی سطح کی تخصیصات

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

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

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

Hoare طرز کی خصوصیات

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

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

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

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

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

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

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

ٹریس لیول کی خصوصیات

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

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

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

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

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

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

سمارٹ کنٹریکٹس کی رسمی تصدیق کے لیے تکنیکیں

ماڈل چیکنگ

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

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

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

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

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

تھیورم پرونگ (Theorem proving)

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

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

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

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

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

علامتی نفاذ (Symbolic execution)

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

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

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

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

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

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

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

function safe_add(uint x, uint y) returns(uint z){

  z = x + y;
  require(z>=x);
  require(z>=y);

  return z;
}

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

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

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

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

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

عملی درستگی کو ثابت کرنا

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

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

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

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

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

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

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

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

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

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

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

رسمی تصدیق کی خامیاں

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

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

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

غلط منفی (False negatives)

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

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

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

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

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

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

رسمی تخصیصات بنانے کے لیے تخصیص کی زبانیں

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

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

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

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

GitHub (opens in a new tab)

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

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

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

GitHub (opens in a new tab)

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

GitHub (opens in a new tab)

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

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

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

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

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

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

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

GitHub (opens in a new tab)

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

مزید مطالعہ

صفحہ کی آخری اپ ڈیٹ: ۲۸ اپریل، ۲۰۲۶

+12

واپس اوپر جائیں ↑