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

ہم ⁦Runtime Verification⁩ ہیں، ایک ریسرچ اور ڈیولپمنٹ کمپنی جو اہم سسٹمز کی حفاظت اور درستگی کو یقینی بنانے کے لیے سخت ٹولز بناتی ہے۔ ہماری ٹیم نے ⁦KEVM⁩ تیار کیا ہے، جو ⁦Ethereum Virtual Machine (EVM)⁩ کی سب سے مکمل اور آزمودہ رسمی سیمینٹکس (formal semantics) ہے، جسے ⁦K Framework⁩ میں لکھا گیا ہے۔ ⁦KEVM⁩ صرف ایک تصریح (specification) نہیں ہے، یہ ایک ایگزیکیوٹیبل تصریح ہے جسے سمارٹ کنٹریکٹس کے بارے میں سمبولک استدلال کرنے، کنفارمنس ٹیسٹ چلانے، گیس کے استعمال کا تجزیہ کرنے، پروگرامز کو ڈیبگ کرنے، اور درستگی کی خصوصیات کی باقاعدہ تصدیق کرنے کے لیے استعمال کیا جا سکتا ہے۔ یہ مکمل ⁦Ethereum⁩ ٹیسٹ سوٹ کو پاس کرتا ہے اور اسے ⁦Solidity⁩ اور ⁦Vyper⁩ دونوں میں ⁦ERC-20⁩ ٹوکنز سمیت ہائی ویلیو کنٹریکٹس کی تصدیق کے لیے استعمال کیا جاتا ہے۔ ہم نے حال ہی میں ⁦Pectra⁩ اپ گریڈ کو سپورٹ کرنے کے لیے سیمینٹکس کو اپ ڈیٹ کیا ہے۔ ⁦KEVM⁩ کو ⁦Kontrol⁩ کے ذریعے فعال طور پر استعمال کیا جا رہا ہے - جو ⁦Solidity⁩ کے لیے ہمارا رسمی تصدیقی ٹول ہے، جسے ⁦EVM⁩ ایکو سسٹم میں معروف ٹیمیں فعال طور پر استعمال کرتی ہیں، جن میں ⁦Optimism⁩، ⁦Ethereum Foundation⁩، ⁦Lido⁩، ⁦Uniswap⁩، نیز وسیع تر ⁦Ethereum⁩ کمیونٹی کے سیکیورٹی محققین اور آڈیٹرز شامل ہیں۔ ہم فعال طور پر اس ریپوزٹری کو برقرار رکھتے ہیں، ⁦Ethereum⁩ کے پروٹوکول کے ارتقاء میں حصہ ڈالتے ہیں، اور ⁦Foundry⁩ جیسے ڈیولپر ٹولنگ کے ساتھ انٹیگریٹ کرتے ہیں۔ ⁦KEVM⁩ کے ذریعے، ہم ثابت شدہ درست اور محفوظ سمارٹ کنٹریکٹ انفراسٹرکچر میں ممکنات کی حدوں کو آگے بڑھا رہے ہیں۔

⁦Act⁩ فارمل ویریفکیشن کے لیے ایک سمارٹ کنٹریکٹ اسپیسیفکیشن لینگویج اور ٹول کٹ ہے۔ ⁦Act⁩ اسپیسیفکیشنز کسی ⁦EVM⁩ پروگرام کے تمام ممکنہ رویوں کی ایک رسمی، ہائی-لیول تفصیل ہیں۔ ⁦Act⁩ بہت سے موجودہ جنرل پرپز ویریفکیشن ٹولز کو اسپیسیفکیشن کے بارے میں خصوصیات ثابت کرنے کے لیے استعمال کرنے کی اجازت دیتا ہے۔ ایسے ٹولز میں ⁦SMT solvers⁩ (⁦cvc5⁩، ⁦z3⁩، ⁦bitwuzla⁩)، تھیورم پروورز (⁦Coq⁩) اور اکنامک انیلیسز ٹولنگ (⁦CheckMate⁩، ⁦Open Games⁩) شامل ہیں۔ ⁦Act⁩ اسپیسیفکیشنز کو خود بخود ⁦EVM⁩ میں ٹھوس امپلیمینٹیشنز کے مساوی ثابت کیا جا سکتا ہے۔ بہت سادہ کنٹریکٹس کے لیے، ⁦Act⁩ اسپیسیفکیشنز کو خود بخود ⁦EVM⁩ بائٹ کوڈ سے جنریٹ کیا جا سکتا ہے۔ یہ ایک اینڈ-ٹو-اینڈ پائپ لائن ہے جو ⁦EVM⁩ بائٹ کوڈ کی ہائی لیول خصوصیات کے بارے میں اصولی استدلال کو سپورٹ کرتی ہے۔ یہ درستگی (جیسے اکاؤنٹنگ انویرینٹس) اور معاشی خصوصیات (جیسے انسنٹیو کمپیٹیبلٹی) دونوں کے بارے میں استدلال کو سپورٹ کرتی ہے۔ ⁦Act⁩ اسپیسیفکیشنز ایک ہائی-لیول سمارٹ کنٹریکٹ کی نمائندگی کے طور پر کام کرتی ہیں، جو موجودہ جنرل پرپز انیلیسز اور ویریفکیشن ٹولنگ کو ⁦EVM⁩ سیاق و سباق میں آسانی سے انٹیگریٹ کرنے کی اجازت دیتی ہیں۔

⁦Titanoboa⁩ ایک ⁦Vyper⁩ انٹرپریٹر اور ٹیسٹنگ فریم ورک ہے جو ⁦Vyper⁩ سمارٹ کنٹریکٹس کے لیے ایک جدید، مربوط ڈیولپمنٹ تجربہ فراہم کرتا ہے۔ یہ ڈیولپرز کو براہ راست ⁦Python⁩ کے اندر ⁦Vyper⁩ کنٹریکٹس کو ٹیسٹ اور ڈیبگ کرنے کے قابل بناتا ہے، جو پریٹی ٹریس بیکس (pretty tracebacks)، فورکنگ، ڈیبگنگ کی صلاحیتیں، ⁦pytest⁩ انٹیگریشن اور آؤٹ آف دی باکس فزنگ جیسی خصوصیات پیش کرتا ہے۔ اپنی سٹینڈ الون صلاحیتوں سے ہٹ کر، ⁦Titanoboa⁩ ⁦Ape⁩ اور ⁦Moccasin⁩ جیسے دیگر مقبول ٹیسٹنگ فریم ورکس کی بنیاد کے طور پر کام کرتا ہے، اور ⁦Vyper⁩ ایکو سسٹم کے لیے انفراسٹرکچر کا ایک بنیادی حصہ ہے۔