স্মার্ট কন্ট্রাক্টের বিধিবদ্ধ যাচাইকরণ

পৃষ্ঠা সম্পাদনা করুন

স্মার্ট কন্ট্রাক্ট বিকেন্দ্রীকৃত, আস্থা-নিরপেক্ষ এবং শক্তিশালী অ্যাপ্লিকেশন তৈরি করা সম্ভব করছে যা নতুন ব্যবহারের ক্ষেত্র প্রবর্তন করে এবং ব্যবহারকারীদের জন্য মান উন্মুক্ত করে। যেহেতু স্মার্ট কন্ট্রাক্ট বিপুল পরিমাণ মান পরিচালনা করে, তাই ডেভেলপারদের জন্য নিরাপত্তা একটি অত্যন্ত গুরুত্বপূর্ণ বিবেচ্য বিষয়।

বিধিবদ্ধ যাচাইকরণ হলো স্মার্ট কন্ট্রাক্টের নিরাপত্তা উন্নত করার জন্য প্রস্তাবিত কৌশলগুলোর মধ্যে একটি। বিধিবদ্ধ যাচাইকরণ, যা প্রোগ্রাম নির্দিষ্টকরণ, ডিজাইন এবং যাচাই করার জন্য বিধিবদ্ধ পদ্ধতি (opens in a new tab) ব্যবহার করে, তা বছরের পর বছর ধরে গুরুত্বপূর্ণ হার্ডওয়্যার এবং সফটওয়্যার সিস্টেমের সঠিকতা নিশ্চিত করতে ব্যবহৃত হয়ে আসছে।

স্মার্ট কন্ট্রাক্টে প্রয়োগ করা হলে, বিধিবদ্ধ যাচাইকরণ প্রমাণ করতে পারে যে একটি কন্ট্রাক্টের ব্যবসায়িক লজিক পূর্বনির্ধারিত স্পেসিফিকেশন পূরণ করে। কন্ট্রাক্ট কোডের সঠিকতা মূল্যায়নের অন্যান্য পদ্ধতি, যেমন টেস্টিং-এর তুলনায়, বিধিবদ্ধ যাচাইকরণ একটি স্মার্ট কন্ট্রাক্ট কার্যকারিতার দিক থেকে সঠিক হওয়ার আরও শক্তিশালী নিশ্চয়তা প্রদান করে।

বিধিবদ্ধ যাচাইকরণ কী?

বিধিবদ্ধ যাচাইকরণ বলতে একটি বিধিবদ্ধ স্পেসিফিকেশনের সাপেক্ষে কোনো সিস্টেমের সঠিকতা মূল্যায়নের প্রক্রিয়াকে বোঝায়। সহজ কথায়, বিধিবদ্ধ যাচাইকরণ আমাদের পরীক্ষা করতে দেয় যে কোনো সিস্টেমের আচরণ কিছু প্রয়োজনীয়তা পূরণ করে কি না (অর্থাৎ, এটি আমরা যা চাই তা করে কি না)।

সিস্টেমের (এই ক্ষেত্রে একটি স্মার্ট কন্ট্রাক্ট) প্রত্যাশিত আচরণগুলো বিধিবদ্ধ মডেলিং ব্যবহার করে বর্ণনা করা হয়, যেখানে স্পেসিফিকেশন ভাষাগুলো বিধিবদ্ধ বৈশিষ্ট্য তৈরি করতে সক্ষম করে। এরপর বিধিবদ্ধ যাচাইকরণ কৌশলগুলো যাচাই করতে পারে যে একটি কন্ট্রাক্টের বাস্তবায়ন তার স্পেসিফিকেশন মেনে চলে এবং এর সঠিকতার গাণিতিক প্রমাণ বের করতে পারে। যখন একটি কন্ট্রাক্ট তার স্পেসিফিকেশন পূরণ করে, তখন এটিকে "কার্যকারিতার দিক থেকে সঠিক", "ডিজাইন অনুসারে সঠিক", বা "গঠন অনুসারে সঠিক" হিসেবে বর্ণনা করা হয়।

বিধিবদ্ধ মডেল কী?

কম্পিউটার বিজ্ঞানে, একটি বিধিবদ্ধ মডেল (opens in a new tab) হলো একটি কম্পিউটেশনাল প্রক্রিয়ার গাণিতিক বর্ণনা। প্রোগ্রামগুলোকে গাণিতিক ফাংশনে (সমীকরণ) বিমূর্ত করা হয়, যেখানে মডেলটি বর্ণনা করে যে একটি ইনপুট দেওয়া হলে ফাংশনগুলোর আউটপুট কীভাবে গণনা করা হয়।

বিধিবদ্ধ মডেলগুলো এমন একটি স্তরের বিমূর্ততা প্রদান করে যার ওপর ভিত্তি করে একটি প্রোগ্রামের আচরণের বিশ্লেষণ মূল্যায়ন করা যেতে পারে। বিধিবদ্ধ মডেলের অস্তিত্ব একটি বিধিবদ্ধ স্পেসিফিকেশন তৈরির সুযোগ দেয়, যা আলোচ্য মডেলের কাঙ্ক্ষিত বৈশিষ্ট্যগুলো বর্ণনা করে।

বিধিবদ্ধ যাচাইকরণের জন্য স্মার্ট কন্ট্রাক্ট মডেলিং করতে বিভিন্ন কৌশল ব্যবহৃত হয়। উদাহরণস্বরূপ, কিছু মডেল একটি স্মার্ট কন্ট্রাক্টের উচ্চ-স্তরের আচরণ সম্পর্কে যুক্তি দিতে ব্যবহৃত হয়। এই মডেলিং কৌশলগুলো স্মার্ট কন্ট্রাক্টগুলোতে একটি ব্ল্যাক-বক্স দৃষ্টিভঙ্গি প্রয়োগ করে, সেগুলোকে এমন সিস্টেম হিসেবে দেখে যা ইনপুট গ্রহণ করে এবং সেই ইনপুটগুলোর ওপর ভিত্তি করে কম্পিউটেশন চালায়।

উচ্চ-স্তরের মডেলগুলো স্মার্ট কন্ট্রাক্ট এবং বাহ্যিক এজেন্ট, যেমন এক্সটার্নালি ওনড অ্যাকাউন্ট (EOA), কন্ট্রাক্ট অ্যাকাউন্ট এবং ব্লকচেইন পরিবেশের মধ্যে সম্পর্কের ওপর ফোকাস করে। এই ধরনের মডেলগুলো এমন বৈশিষ্ট্য সংজ্ঞায়িত করতে কার্যকর যা নির্দিষ্ট ব্যবহারকারীর ইন্টারঅ্যাকশনের প্রতিক্রিয়ায় একটি কন্ট্রাক্টের কীভাবে আচরণ করা উচিত তা নির্দিষ্ট করে।

অন্যদিকে, অন্যান্য বিধিবদ্ধ মডেলগুলো একটি স্মার্ট কন্ট্রাক্টের নিম্ন-স্তরের আচরণের ওপর ফোকাস করে। যদিও উচ্চ-স্তরের মডেলগুলো একটি কন্ট্রাক্টের কার্যকারিতা সম্পর্কে যুক্তি দিতে সাহায্য করতে পারে, তবে সেগুলো বাস্তবায়নের অভ্যন্তরীণ কাজ সম্পর্কে বিস্তারিত তথ্য ধারণ করতে ব্যর্থ হতে পারে। নিম্ন-স্তরের মডেলগুলো প্রোগ্রাম বিশ্লেষণে একটি হোয়াইট-বক্স দৃষ্টিভঙ্গি প্রয়োগ করে এবং একটি কন্ট্রাক্টের এক্সিকিউশনের সাথে প্রাসঙ্গিক বৈশিষ্ট্যগুলো সম্পর্কে যুক্তি দিতে স্মার্ট কন্ট্রাক্ট অ্যাপ্লিকেশনগুলোর নিম্ন-স্তরের উপস্থাপনা, যেমন প্রোগ্রাম ট্রেস এবং কন্ট্রোল ফ্লো গ্রাফ (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() ব্যবহারের শর্তগুলো কভার করে: "একজন প্রেরকের ব্যালেন্স কখনো পাঠানোর জন্য অনুরোধ করা টোকেনের পরিমাণের চেয়ে কম হয় না।" একটি কন্ট্রাক্ট ইনভ্যারিয়েন্টের এই স্বাভাবিক-ভাষার বর্ণনাকে একটি বিধিবদ্ধ (গাণিতিক) স্পেসিফিকেশনে অনুবাদ করা যেতে পারে, যা পরে বৈধতার জন্য কঠোরভাবে পরীক্ষা করা যেতে পারে।

সজীবতা বৈশিষ্ট্যগুলো নিশ্চিত করে যে "অবশেষে ভালো কিছু ঘটে" এবং এটি বিভিন্ন স্টেটের মাধ্যমে অগ্রসর হওয়ার জন্য একটি কন্ট্রাক্টের ক্ষমতার সাথে সম্পর্কিত। সজীবতা বৈশিষ্ট্যের একটি উদাহরণ হলো "তারল্য", যা অনুরোধের ভিত্তিতে ব্যবহারকারীদের কাছে এর ব্যালেন্স হস্তান্তর করার জন্য একটি কন্ট্রাক্টের ক্ষমতাকে বোঝায়। যদি এই বৈশিষ্ট্যটি লঙ্ঘিত হয়, তবে ব্যবহারকারীরা কন্ট্রাক্টে সংরক্ষিত সম্পদ তুলতে অক্ষম হবেন, যেমনটি Parity ওয়ালেট ঘটনায় (opens in a new tab) ঘটেছিল।

নিম্ন-স্তরের স্পেসিফিকেশন

উচ্চ-স্তরের স্পেসিফিকেশনগুলো একটি কন্ট্রাক্টের ফাইনাইট-স্টেট মডেলকে প্রারম্ভিক বিন্দু হিসেবে নেয় এবং এই মডেলের কাঙ্ক্ষিত বৈশিষ্ট্যগুলো সংজ্ঞায়িত করে। এর বিপরীতে, নিম্ন-স্তরের স্পেসিফিকেশনগুলো (যাকে "বৈশিষ্ট্য-ভিত্তিক স্পেসিফিকেশন"ও বলা হয়) প্রায়শই প্রোগ্রামগুলোকে (স্মার্ট কন্ট্রাক্ট) গাণিতিক ফাংশনের সংগ্রহ নিয়ে গঠিত সিস্টেম হিসেবে মডেল করে এবং এই ধরনের সিস্টেমের সঠিক আচরণ বর্ণনা করে।

সহজ কথায়, নিম্ন-স্তরের স্পেসিফিকেশনগুলো প্রোগ্রাম ট্রেস বিশ্লেষণ করে এবং এই ট্রেসগুলোর ওপর একটি স্মার্ট কন্ট্রাক্টের বৈশিষ্ট্য সংজ্ঞায়িত করার চেষ্টা করে। ট্রেস বলতে ফাংশন এক্সিকিউশনের ক্রম বোঝায় যা একটি স্মার্ট কন্ট্রাক্টের স্টেট পরিবর্তন করে; তাই, নিম্ন-স্তরের স্পেসিফিকেশনগুলো একটি কন্ট্রাক্টের অভ্যন্তরীণ এক্সিকিউশনের জন্য প্রয়োজনীয়তা নির্দিষ্ট করতে সাহায্য করে।

নিম্ন-স্তরের বিধিবদ্ধ স্পেসিফিকেশনগুলো হোর-স্টাইলের বৈশিষ্ট্য বা এক্সিকিউশন পাথের ইনভ্যারিয়েন্ট হিসেবে দেওয়া যেতে পারে।

হোর-স্টাইলের বৈশিষ্ট্য

হোর লজিক (opens in a new tab) স্মার্ট কন্ট্রাক্টসহ প্রোগ্রামগুলোর সঠিকতা সম্পর্কে যুক্তি দেওয়ার জন্য বিধিবদ্ধ নিয়মের একটি সেট প্রদান করে। একটি হোর-স্টাইলের বৈশিষ্ট্য একটি হোর ট্রিপল {P}c{Q} দ্বারা উপস্থাপিত হয়, যেখানে c হলো একটি প্রোগ্রাম এবং P ও Q হলো c (অর্থাৎ, প্রোগ্রাম)-এর স্টেটের ওপর প্রেডিকেট, যা বিধিবদ্ধভাবে যথাক্রমে প্রিকন্ডিশন এবং পোস্টকন্ডিশন হিসেবে বর্ণিত।

একটি প্রিকন্ডিশন হলো একটি প্রেডিকেট যা একটি ফাংশনের সঠিক এক্সিকিউশনের জন্য প্রয়োজনীয় শর্তগুলো বর্ণনা করে; কন্ট্রাক্টে কল করা ব্যবহারকারীদের অবশ্যই এই প্রয়োজনীয়তা পূরণ করতে হবে। একটি পোস্টকন্ডিশন হলো একটি প্রেডিকেট যা সঠিকভাবে এক্সিকিউট হলে একটি ফাংশন যে শর্ত স্থাপন করে তা বর্ণনা করে; ব্যবহারকারীরা ফাংশনে কল করার পরে এই শর্তটি সত্য হবে বলে আশা করতে পারেন। হোর লজিকে একটি ইনভ্যারিয়েন্ট হলো একটি প্রেডিকেট যা একটি ফাংশনের এক্সিকিউশন দ্বারা সংরক্ষিত থাকে (অর্থাৎ, এটি পরিবর্তিত হয় না)।

হোর-স্টাইলের স্পেসিফিকেশনগুলো আংশিক সঠিকতা বা সম্পূর্ণ সঠিকতা-এর নিশ্চয়তা দিতে পারে। একটি কন্ট্রাক্ট ফাংশনের বাস্তবায়ন "আংশিকভাবে সঠিক" হয় যদি ফাংশনটি এক্সিকিউট হওয়ার আগে প্রিকন্ডিশন সত্য থাকে এবং যদি এক্সিকিউশন শেষ হয়, তবে পোস্টকন্ডিশনটিও সত্য হয়। সম্পূর্ণ সঠিকতার প্রমাণ পাওয়া যায় যদি ফাংশনটি এক্সিকিউট হওয়ার আগে একটি প্রিকন্ডিশন সত্য হয়, এক্সিকিউশন শেষ হওয়ার নিশ্চয়তা থাকে এবং যখন এটি শেষ হয়, তখন পোস্টকন্ডিশন সত্য থাকে।

সম্পূর্ণ সঠিকতার প্রমাণ পাওয়া কঠিন কারণ কিছু এক্সিকিউশন শেষ হওয়ার আগে বিলম্বিত হতে পারে, বা কখনোই শেষ নাও হতে পারে। তা সত্ত্বেও, এক্সিকিউশন শেষ হয় কি না সেই প্রশ্নটি তর্কসাপেক্ষভাবে একটি অমীমাংসিত বিষয় কারণ ইথেরিয়ামের গ্যাস মেকানিজম অসীম প্রোগ্রাম লুপ প্রতিরোধ করে (এক্সিকিউশন সফলভাবে শেষ হয় বা 'আউট-অফ-গ্যাস' ত্রুটির কারণে শেষ হয়)।

হোর লজিক ব্যবহার করে তৈরি করা স্মার্ট কন্ট্রাক্ট স্পেসিফিকেশনগুলোতে একটি কন্ট্রাক্টে ফাংশন এবং লুপের এক্সিকিউশনের জন্য প্রিকন্ডিশন, পোস্টকন্ডিশন এবং ইনভ্যারিয়েন্ট সংজ্ঞায়িত থাকবে। প্রিকন্ডিশনগুলোতে প্রায়শই একটি ফাংশনে ভুল ইনপুটের সম্ভাবনা অন্তর্ভুক্ত থাকে, যেখানে পোস্টকন্ডিশনগুলো এই ধরনের ইনপুটগুলোর প্রত্যাশিত প্রতিক্রিয়া বর্ণনা করে (যেমন, একটি নির্দিষ্ট এক্সেপশন থ্রো করা)। এইভাবে হোর-স্টাইলের বৈশিষ্ট্যগুলো কন্ট্রাক্ট বাস্তবায়নের সঠিকতা নিশ্চিত করার জন্য কার্যকর।

অনেক বিধিবদ্ধ যাচাইকরণ ফ্রেমওয়ার্ক ফাংশনগুলোর শব্দার্থিক সঠিকতা প্রমাণের জন্য হোর-স্টাইলের স্পেসিফিকেশন ব্যবহার করে। Solidity-তে 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 তৈরি করতে পারে।

যেহেতু সিম্বলিক এক্সিকিউশন একটি প্রোগ্রামের ইনপুটের ওপর নির্ভর করে, এবং সমস্ত রিচেবল স্টেট অন্বেষণ করার জন্য ইনপুটের সেট সম্ভাব্যভাবে অসীম, তাই এটি এখনো এক ধরনের টেস্টিং। তবে, উদাহরণে যেমন দেখানো হয়েছে, বৈশিষ্ট্য লঙ্ঘন ট্রিগার করে এমন ইনপুট খুঁজে বের করার জন্য সিম্বলিক এক্সিকিউশন নিয়মিত টেস্টিংয়ের চেয়ে বেশি কার্যকর।

তদুপরি, সিম্বলিক এক্সিকিউশন অন্যান্য বৈশিষ্ট্য-ভিত্তিক কৌশলগুলোর (যেমন, ফাজিং) তুলনায় কম ফলস পজিটিভ তৈরি করে যা এলোমেলোভাবে একটি ফাংশনে ইনপুট তৈরি করে। যদি সিম্বলিক এক্সিকিউশনের সময় একটি ত্রুটি স্টেট ট্রিগার হয়, তবে এমন একটি কংক্রিট মান তৈরি করা সম্ভব যা ত্রুটিটি ট্রিগার করে এবং সমস্যাটি পুনরুৎপাদন করে।

সিম্বলিক এক্সিকিউশন সঠিকতার কিছু মাত্রার গাণিতিক প্রমাণও প্রদান করতে পারে। ওভারফ্লো সুরক্ষাসহ একটি কন্ট্রাক্ট ফাংশনের নিম্নলিখিত উদাহরণটি বিবেচনা করুন:

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) ডিপ্লয় করা কোড সাধারণত অপরিবর্তনীয় হয়। লঞ্চ-পরবর্তী আপগ্রেডগুলো সহজে অ্যাক্সেসযোগ্য না হওয়ায়, কন্ট্রাক্টের নির্ভরযোগ্যতা নিশ্চিত করার প্রয়োজনীয়তা বিধিবদ্ধ যাচাইকরণকে অপরিহার্য করে তোলে। বিধিবদ্ধ যাচাইকরণ জটিল সমস্যাগুলো শনাক্ত করতে সক্ষম, যেমন ইন্টিজার আন্ডারফ্লো এবং ওভারফ্লো, রি-এন্ট্রান্সি এবং দুর্বল গ্যাস অপ্টিমাইজেশন, যা অডিটর এবং টেস্টারদের চোখ এড়িয়ে যেতে পারে।

কার্যকারিতার সঠিকতা প্রমাণ করা

প্রোগ্রাম টেস্টিং হলো একটি স্মার্ট কন্ট্রাক্ট কিছু প্রয়োজনীয়তা পূরণ করে তা প্রমাণ করার সবচেয়ে সাধারণ পদ্ধতি। এর মধ্যে একটি কন্ট্রাক্টকে এমন ডেটার নমুনা দিয়ে এক্সিকিউট করা জড়িত যা এটি পরিচালনা করবে বলে আশা করা হয় এবং এর আচরণ বিশ্লেষণ করা হয়। যদি কন্ট্রাক্টটি নমুনা ডেটার জন্য প্রত্যাশিত ফলাফল প্রদান করে, তবে ডেভেলপারদের কাছে এর সঠিকতার বস্তুনিষ্ঠ প্রমাণ থাকে।

তবে, এই পদ্ধতিটি এমন ইনপুট মানগুলোর জন্য সঠিক এক্সিকিউশন প্রমাণ করতে পারে না যা নমুনার অংশ নয়। অতএব, একটি কন্ট্রাক্ট পরীক্ষা করা বাগ শনাক্ত করতে সাহায্য করতে পারে (অর্থাৎ, যদি কিছু কোড পাথ এক্সিকিউশনের সময় কাঙ্ক্ষিত ফলাফল প্রদান করতে ব্যর্থ হয়), তবে এটি চূড়ান্তভাবে বাগের অনুপস্থিতি প্রমাণ করতে পারে না।

অন্যদিকে, বিধিবদ্ধ যাচাইকরণ কন্ট্রাক্টটি মোটেও না চালিয়ে অসীম পরিসরের এক্সিকিউশনের জন্য একটি স্মার্ট কন্ট্রাক্ট প্রয়োজনীয়তা পূরণ করে তা বিধিবদ্ধভাবে প্রমাণ করতে পারে। এর জন্য একটি বিধিবদ্ধ স্পেসিফিকেশন তৈরি করা প্রয়োজন যা সঠিকভাবে কন্ট্রাক্টের আচরণ বর্ণনা করে এবং কন্ট্রাক্টের সিস্টেমের একটি বিধিবদ্ধ (গাণিতিক) মডেল তৈরি করে। এরপর আমরা কন্ট্রাক্টের মডেল এবং এর স্পেসিফিকেশনের মধ্যে সামঞ্জস্য পরীক্ষা করার জন্য একটি বিধিবদ্ধ প্রমাণ পদ্ধতি অনুসরণ করতে পারি।

বিধিবদ্ধ যাচাইকরণের মাধ্যমে, একটি কন্ট্রাক্টের ব্যবসায়িক লজিক প্রয়োজনীয়তা পূরণ করে কি না তা যাচাই করার প্রশ্নটি একটি গাণিতিক প্রস্তাবনা যা প্রমাণ বা খণ্ডন করা যেতে পারে। একটি প্রস্তাবনা বিধিবদ্ধভাবে প্রমাণ করে, আমরা সসীম সংখ্যক ধাপের মাধ্যমে অসীম সংখ্যক টেস্ট কেস যাচাই করতে পারি। এইভাবে বিধিবদ্ধ যাচাইকরণের একটি স্পেসিফিকেশনের সাপেক্ষে একটি কন্ট্রাক্ট কার্যকারিতার দিক থেকে সঠিক তা প্রমাণ করার আরও ভালো সম্ভাবনা রয়েছে।

আদর্শ যাচাইকরণের লক্ষ্য

একটি যাচাইকরণের লক্ষ্য সেই সিস্টেমকে বর্ণনা করে যা বিধিবদ্ধভাবে যাচাই করা হবে। বিধিবদ্ধ যাচাইকরণ সবচেয়ে ভালোভাবে "এমবেডেড সিস্টেম" (ছোট, সাধারণ সফটওয়্যার যা একটি বড় সিস্টেমের অংশ গঠন করে)-এ ব্যবহৃত হয়। এগুলো এমন বিশেষ ডোমেইনের জন্যও আদর্শ যেখানে কয়েকটি নিয়ম রয়েছে, কারণ এটি ডোমেইন-নির্দিষ্ট বৈশিষ্ট্য যাচাই করার জন্য টুলগুলো পরিবর্তন করা সহজ করে তোলে।

স্মার্ট কন্ট্রাক্টগুলো—অন্তত, কিছুটা হলেও—উভয় প্রয়োজনীয়তা পূরণ করে। উদাহরণস্বরূপ, ইথেরিয়াম কন্ট্রাক্টগুলোর ছোট আকার সেগুলোকে বিধিবদ্ধ যাচাইকরণের উপযোগী করে তোলে। একইভাবে, EVM সহজ নিয়ম অনুসরণ করে, যা EVM-এ চলা প্রোগ্রামগুলোর জন্য শব্দার্থিক বৈশিষ্ট্য নির্দিষ্ট করা এবং যাচাই করা সহজ করে তোলে।

দ্রুততর ডেভেলপমেন্ট সাইকেল

বিধিবদ্ধ যাচাইকরণ কৌশলগুলো, যেমন মডেল চেকিং এবং সিম্বলিক এক্সিকিউশন, সাধারণত স্মার্ট কন্ট্রাক্ট কোডের নিয়মিত বিশ্লেষণের (টেস্টিং বা অডিটিংয়ের সময় সম্পাদিত) চেয়ে বেশি কার্যকর। এর কারণ হলো বিধিবদ্ধ যাচাইকরণ দাবিগুলো পরীক্ষা করার জন্য সিম্বলিক মানের ওপর নির্ভর করে ("যদি একজন ব্যবহারকারী n ইথার তোলার চেষ্টা করেন তবে কী হবে?") যা টেস্টিংয়ের বিপরীত যেখানে কংক্রিট মান ব্যবহার করা হয় ("যদি একজন ব্যবহারকারী 5 ইথার তোলার চেষ্টা করেন তবে কী হবে?")।

সিম্বলিক ইনপুট ভেরিয়েবলগুলো কংক্রিট মানের একাধিক ক্লাস কভার করতে পারে, তাই বিধিবদ্ধ যাচাইকরণ পদ্ধতিগুলো অল্প সময়ের মধ্যে আরও বেশি কোড কভারেজের প্রতিশ্রুতি দেয়। কার্যকরভাবে ব্যবহার করা হলে, বিধিবদ্ধ যাচাইকরণ ডেভেলপারদের জন্য ডেভেলপমেন্ট সাইকেল ত্বরান্বিত করতে পারে।

বিধিবদ্ধ যাচাইকরণ ব্যয়বহুল ডিজাইনের ত্রুটিগুলো কমিয়ে বিকেন্দ্রীকৃত অ্যাপ্লিকেশন (dapp) তৈরির প্রক্রিয়াকেও উন্নত করে। দুর্বলতাগুলো ঠিক করার জন্য কন্ট্রাক্ট আপগ্রেড করার (যেখানে সম্ভব) জন্য কোডবেসগুলোর ব্যাপক পুনর্লিখন এবং ডেভেলপমেন্টে আরও বেশি প্রচেষ্টা ব্যয় করা প্রয়োজন। বিধিবদ্ধ যাচাইকরণ কন্ট্রাক্ট বাস্তবায়নে অনেক ত্রুটি শনাক্ত করতে পারে যা টেস্টার এবং অডিটরদের চোখ এড়িয়ে যেতে পারে এবং একটি কন্ট্রাক্ট ডিপ্লয় করার আগে সেই সমস্যাগুলো ঠিক করার পর্যাপ্ত সুযোগ প্রদান করে।

বিধিবদ্ধ যাচাইকরণের অসুবিধা

কায়িক শ্রমের ব্যয়

বিধিবদ্ধ যাচাইকরণ, বিশেষ করে আধা-স্বয়ংক্রিয় যাচাইকরণ যেখানে একজন মানুষ সঠিকতার প্রমাণ বের করতে প্রমাণকারীকে গাইড করে, তার জন্য যথেষ্ট কায়িক শ্রমের প্রয়োজন হয়। তদুপরি, বিধিবদ্ধ স্পেসিফিকেশন তৈরি করা একটি জটিল কাজ যার জন্য উচ্চ স্তরের দক্ষতার প্রয়োজন।

এই বিষয়গুলো (প্রচেষ্টা এবং দক্ষতা) কন্ট্রাক্টে সঠিকতা মূল্যায়নের স্বাভাবিক পদ্ধতি, যেমন টেস্টিং এবং অডিটের তুলনায় বিধিবদ্ধ যাচাইকরণকে আরও বেশি চাহিদাপূর্ণ এবং ব্যয়বহুল করে তোলে। তা সত্ত্বেও, স্মার্ট কন্ট্রাক্ট বাস্তবায়নে ত্রুটির ব্যয়ের কথা বিবেচনা করে একটি সম্পূর্ণ যাচাইকরণ অডিটের জন্য ব্যয় করা বাস্তবসম্মত।

ফলস নেগেটিভ

বিধিবদ্ধ যাচাইকরণ কেবল পরীক্ষা করতে পারে যে স্মার্ট কন্ট্রাক্টের এক্সিকিউশন বিধিবদ্ধ স্পেসিফিকেশনের সাথে মেলে কি না। তাই, স্পেসিফিকেশনটি একটি স্মার্ট কন্ট্রাক্টের প্রত্যাশিত আচরণগুলো সঠিকভাবে বর্ণনা করে তা নিশ্চিত করা গুরুত্বপূর্ণ।

যদি স্পেসিফিকেশনগুলো খারাপভাবে লেখা হয়, তবে বৈশিষ্ট্যের লঙ্ঘন—যা দুর্বল এক্সিকিউশনের দিকে নির্দেশ করে—বিধিবদ্ধ যাচাইকরণ অডিট দ্বারা শনাক্ত করা যাবে না। এই ক্ষেত্রে, একজন ডেভেলপার ভুলভাবে ধরে নিতে পারেন যে কন্ট্রাক্টটি বাগ-মুক্ত।

পারফরম্যান্স সমস্যা

বিধিবদ্ধ যাচাইকরণ বেশ কয়েকটি পারফরম্যান্স সমস্যার সম্মুখীন হয়। উদাহরণস্বরূপ, যথাক্রমে মডেল চেকিং এবং সিম্বলিক চেকিংয়ের সময় সম্মুখীন হওয়া স্টেট এবং পাথ এক্সপ্লোশন সমস্যাগুলো যাচাইকরণ পদ্ধতিকে প্রভাবিত করতে পারে। এছাড়াও, বিধিবদ্ধ যাচাইকরণ টুলগুলো প্রায়শই তাদের অন্তর্নিহিত স্তরে SMT সমাধানকারী এবং অন্যান্য কনস্ট্রেইন্ট সমাধানকারী ব্যবহার করে, এবং এই সমাধানকারীগুলো কম্পিউটেশনালি নিবিড় পদ্ধতির ওপর নির্ভর করে।

এছাড়াও, প্রোগ্রাম যাচাইকারীদের পক্ষে সর্বদা নির্ধারণ করা সম্ভব নয় যে একটি বৈশিষ্ট্য (একটি যৌক্তিক সূত্র হিসেবে বর্ণিত) পূরণ করা যেতে পারে কি না ("ডিসাইডেবিলিটি প্রবলেম (opens in a new tab)") কারণ একটি প্রোগ্রাম কখনোই শেষ নাও হতে পারে। তাই, একটি কন্ট্রাক্ট ভালোভাবে নির্দিষ্ট করা থাকলেও এর কিছু বৈশিষ্ট্য প্রমাণ করা অসম্ভব হতে পারে।

ইথেরিয়াম স্মার্ট কন্ট্রাক্টের জন্য বিধিবদ্ধ যাচাইকরণ টুল

বিধিবদ্ধ স্পেসিফিকেশন তৈরির জন্য স্পেসিফিকেশন ভাষা

Act: Act স্টোরেজ আপডেট, প্রি/পোস্ট কন্ডিশন এবং কন্ট্রাক্ট ইনভ্যারিয়েন্টের স্পেসিফিকেশনের অনুমতি দেয়। এর টুল স্যুটে প্রুফ ব্যাকএন্ডও রয়েছে যা Coq, SMT সমাধানকারী বা hevm-এর মাধ্যমে অনেক বৈশিষ্ট্য প্রমাণ করতে সক্ষম।

Scribble - Scribble স্পেসিফিকেশন ভাষায় কোড টীকাগুলোকে (annotations) কংক্রিট অ্যাসার্টে রূপান্তরিত করে যা স্পেসিফিকেশন পরীক্ষা করে।

ডকুমেন্টেশন (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) এবং হর্ন সলভিংয়ের ওপর ভিত্তি করে একটি বিল্ট-ইন মডেল চেকার। এটি নিশ্চিত করে যে কম্পাইলেশনের সময় একটি কন্ট্রাক্টের সোর্স কোড স্পেসিফিকেশনের সাথে মেলে কি না এবং স্ট্যাটিকভাবে নিরাপত্তা বৈশিষ্ট্যের লঙ্ঘন পরীক্ষা করে।

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 - ইথেরিয়াম স্মার্ট কন্ট্রাক্টে দুর্বলতা শনাক্ত করার জন্য একটি সিম্বলিক এক্সিকিউশন টুল