নিরাপত্তা, টেস্টিং এবং বিধিবদ্ধ যাচাইকরণ

আমরা Runtime Verification, একটি রিসার্চ এবং ডেভেলপমেন্ট কোম্পানি যা ক্রিটিকাল সিস্টেমের নিরাপত্তা এবং সঠিকতা নিশ্চিত করতে কঠোর টুল তৈরি করে। আমাদের টিম KEVM তৈরি করেছে, যা K Framework-এ লেখা Ethereum Virtual Machine (EVM)-এর সবচেয়ে সম্পূর্ণ এবং ব্যাটল-টেস্টেড ফরমাল সিম্যান্টিকস। KEVM শুধুমাত্র একটি স্পেসিফিকেশন নয়, এটি একটি এক্সিকিউটেবল স্পেসিফিকেশন যা স্মার্ট কন্ট্রাক্ট সম্পর্কে সিম্বলিক্যালি যুক্তি দিতে, কনফরম্যান্স টেস্ট চালাতে, গ্যাস ব্যবহার বিশ্লেষণ করতে, প্রোগ্রাম ডিবাগ করতে এবং সঠিকতার বৈশিষ্ট্যগুলো আনুষ্ঠানিকভাবে যাচাই করতে ব্যবহার করা যেতে পারে। এটি সম্পূর্ণ Ethereum টেস্ট স্যুট পাস করে এবং Solidity ও Vyper উভয় ক্ষেত্রেই ERC-20 টোকেনসহ হাই-ভ্যালু কন্ট্রাক্ট যাচাই করতে ব্যবহৃত হয়। আমরা সম্প্রতি Pectra আপগ্রেড সমর্থন করার জন্য সিম্যান্টিকস আপডেট করেছি। KEVM সক্রিয়ভাবে Kontrol দ্বারা ব্যবহৃত হচ্ছে - যা Soldiity-এর জন্য আমাদের ফরমাল ভেরিফিকেশন টুল, এটি EVM ইকোসিস্টেমের লিডিং টিমগুলো দ্বারা সক্রিয়ভাবে ব্যবহৃত হয়, যার মধ্যে রয়েছে Optimism, Ethereum Foundation, Lido, Uniswap এবং সেইসাথে বৃহত্তর Ethereum কমিউনিটির সিকিউরিটি গবেষক এবং অডিটররা। আমরা সক্রিয়ভাবে এই রিপোজিটরিটি মেইনটেইন করি, Ethereum-এর প্রোটোকল ইভোলিউশনে অবদান রাখি এবং Foundry-এর মতো ডেভেলপার টুলের সাথে ইন্টিগ্রেট করি। KEVM-এর মাধ্যমে, আমরা প্রমাণযোগ্যভাবে সঠিক এবং সুরক্ষিত স্মার্ট কন্ট্রাক্ট ইনফ্রাস্ট্রাকচারে যা সম্ভব তার সীমানা প্রসারিত করছি।

Branching Tree Technique-এর উপর ভিত্তি করে একটি স্মার্ট কন্ট্রাক্ট টেস্ট জেনারেটর।

Runtime Verification এক দশকেরও বেশি সময় ধরে ওপেন-সোর্স ফরমাল ভেরিফিকেশন টুলের অগ্রভাগে রয়েছে। আমাদের সাধারণ পদ্ধতি আমাদের প্রযুক্তিকে একাধিক ব্লকচেইনে ব্যবহার করার অনুমতি দেয়। যদিও KEVM সমস্ত EVM-ভিত্তিক স্মার্ট কন্ট্রাক্টে আমাদের ভেরিফিকেশন ইনফ্রাস্ট্রাকচার অফার করে, Kontrol Solidity স্মার্ট কন্ট্রাক্টের জন্য ফরমাল ভেরিফিকেশনে প্রবেশের বাধা অনেকাংশে কমিয়ে দেয়। আমাদের টুলিং সম্পূর্ণ ওপেন সোর্স এবং কোনো অতিরিক্ত খরচ ছাড়াই Optimism ইকোসিস্টেমের সকল ডেভেলপারের জন্য বিনামূল্যে অ্যাক্সেসযোগ্য। KEVM হলো K ফ্রেমওয়ার্কে লেখা একটি EVM এক্সিকিউটেবল ফরমাল সিম্যান্টিকস। KEVM সমস্ত Ethereum কনফরম্যান্স টেস্ট পাস করে এবং K ফ্রেমওয়ার্কের সাহায্যে স্মার্ট কন্ট্রাক্ট আনুষ্ঠানিকভাবে যাচাই করার এন্ট্রি পয়েন্ট। তবে, প্লেইন KEVM ব্যবহার করার জন্য স্পেসিফিকেশন লিখতে K ফ্রেমওয়ার্কের উপর অ্যাড-হক ট্রেনিং প্রয়োজন। এছাড়াও, এই স্পেসিফিকেশনগুলো বেশ ভার্বোস হতে পারে, যা এগুলো লেখার অসুবিধা বাড়িয়ে দেয়। Kontrol ডেভেলপারদের তাদের স্মার্ট কন্ট্রাক্টের ফরমাল স্পেসিফিকেশন সরাসরি Foundry প্রপার্টি টেস্ট হিসেবে লেখার অনুমতি দিয়ে এর সমাধান করে। এই টেস্টগুলো স্বয়ংক্রিয়ভাবে KEVM স্পেসিফিকেশনে অনুবাদ করা হয়, যা সমস্ত ভেরিফিকেশন গ্যারান্টি বজায় রেখে ডেভেলপারদের জন্য অনেক সহজ অভিজ্ঞতা প্রদান করে।