স্মার্ট কন্ট্রাক্টের ফরমাল ভেরিফিকেশন

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

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

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

ফরমাল ভেরিফিকেশন কী?

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

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

ফরমাল মডেল কী?

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

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

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

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

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

লো-লেভেল মডেলগুলোকে আদর্শ হিসেবে বিবেচনা করা হয় কারণ এগুলো ইথিরিয়ামের এক্সিকিউশন পরিবেশে (অর্থাৎ, EVM) একটি স্মার্ট কন্ট্রাক্টের প্রকৃত এক্সিকিউশন উপস্থাপন করে। লো-লেভেল মডেলিং কৌশলগুলো স্মার্ট কন্ট্রাক্টে গুরুত্বপূর্ণ নিরাপত্তা প্রপার্টি প্রতিষ্ঠা করতে এবং সম্ভাব্য দুর্বলতা শনাক্ত করতে বিশেষভাবে কার্যকর।

ফরমাল স্পেসিফিকেশন কী?

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

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

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

স্মার্ট কন্ট্রাক্টের নিরাপদ বাস্তবায়ন তৈরিতে ফরমাল স্পেসিফিকেশন অত্যন্ত গুরুত্বপূর্ণ। যেসব কন্ট্রাক্ট ইনভ্যারিয়েন্ট বাস্তবায়ন করতে ব্যর্থ হয় বা এক্সিকিউশনের সময় তাদের প্রপার্টি লঙ্ঘিত হয়, সেগুলো এমন দুর্বলতার ঝুঁকিতে থাকে যা কার্যকারিতার ক্ষতি করতে পারে বা ক্ষতিকারক এক্সপ্লয়েটের কারণ হতে পারে।

স্মার্ট কন্ট্রাক্টের জন্য ফরমাল স্পেসিফিকেশনের ধরন

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

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

হাই-লেভেল স্পেসিফিকেশনগুলো সাধারণত স্মার্ট কন্ট্রাক্টের জন্য দুটি গুরুত্বপূর্ণ টেম্পোরাল প্রপার্টি ক্যাপচার করে: সেফটি (safety) এবং লাইভনেস (liveness)। সেফটি প্রপার্টিগুলো এই ধারণা উপস্থাপন করে যে "কখনো খারাপ কিছু ঘটে না" এবং সাধারণত ইনভ্যারিয়েন্স প্রকাশ করে। একটি সেফটি প্রপার্টি সাধারণ সফটওয়্যার প্রয়োজনীয়তা সংজ্ঞায়িত করতে পারে, যেমন ডেডলক (opens in a new tab) থেকে মুক্তি, অথবা কন্ট্রাক্টের জন্য ডোমেইন-নির্দিষ্ট প্রপার্টি প্রকাশ করতে পারে (যেমন, ফাংশনগুলোর জন্য অ্যাক্সেস কন্ট্রোলের ইনভ্যারিয়েন্ট, স্টেট ভেরিয়েবলের গ্রহণযোগ্য মান, বা টোকেন ট্রান্সফারের শর্ত)।

উদাহরণস্বরূপ এই সেফটি প্রয়োজনীয়তাটি নিন যা ERC-20 টোকেন কন্ট্রাক্টে transfer() বা transferFrom() ব্যবহারের শর্তগুলো কভার করে: "একজন প্রেরকের ব্যালেন্স কখনো পাঠানোর জন্য অনুরোধ করা টোকেনের পরিমাণের চেয়ে কম হয় না।"। একটি কন্ট্রাক্ট ইনভ্যারিয়েন্টের এই সাধারণ ভাষার বর্ণনাকে একটি ফরমাল (গাণিতিক) স্পেসিফিকেশনে অনুবাদ করা যেতে পারে, যা পরে বৈধতার জন্য কঠোরভাবে পরীক্ষা করা যেতে পারে।

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

লো-লেভেল স্পেসিফিকেশন

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

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

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

হোর-স্টাইল প্রপার্টি

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

আদর্শ ভেরিফিকেশন টার্গেট

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

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

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

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

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

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

ফরমাল ভেরিফিকেশনের অসুবিধা

কায়িক শ্রমের খরচ

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

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

ফলস নেগেটিভ

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

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

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

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

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

ইথিরিয়াম স্মার্ট কন্ট্রাক্টের জন্য ফরমাল ভেরিফিকেশন টুল

ফরমাল স্পেসিফিকেশন তৈরির জন্য স্পেসিফিকেশন ল্যাঙ্গুয়েজ

Act: Act স্টোরেজ আপডেট, প্রি/পোস্ট কন্ডিশন এবং কন্ট্রাক্ট ইনভ্যারিয়েন্টের স্পেসিফিকেশন অনুমোদন করে। এর টুল স্যুটে প্রুফ ব্যাকএন্ডও রয়েছে যা 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)-এ লেখা হয়, যেখানে স্ট্যাটিক অ্যানালাইসিস এবং কনস্ট্রেইন্ট-সলভিংয়ের সংমিশ্রণ ব্যবহার করে প্রপার্টি লঙ্ঘন শনাক্ত করা হয়।

Solidity SMTChecker - সলিডিটির SMTChecker হলো SMT (Satisfiability Modulo Theories) এবং হর্ন সলভিংয়ের ওপর ভিত্তি করে একটি বিল্ট-ইন মডেল চেকার। এটি নিশ্চিত করে যে কম্পাইলেশনের সময় একটি কন্ট্রাক্টের সোর্স কোড স্পেসিফিকেশনের সাথে মেলে কিনা এবং স্ট্যাটিকভাবে সেফটি প্রপার্টির লঙ্ঘন পরীক্ষা করে।

GitHub (opens in a new tab)

solc-verify - solc-verify হলো সলিডিটি কম্পাইলারের একটি বর্ধিত সংস্করণ যা টীকা এবং মডুলার প্রোগ্রাম ভেরিফিকেশন ব্যবহার করে সলিডিটি কোডে স্বয়ংক্রিয় ফরমাল ভেরিফিকেশন সম্পাদন করতে পারে।

GitHub (opens in a new tab)

KEVM - KEVM হলো K ফ্রেমওয়ার্কে লেখা ইথিরিয়াম ভার্চুয়াল মেশিন (EVM)-এর একটি ফরমাল শব্দার্থবিদ্যা। KEVM এক্সিকিউটেবল এবং রিচেবিলিটি লজিক ব্যবহার করে নির্দিষ্ট প্রপার্টি-সম্পর্কিত দাবি প্রমাণ করতে পারে।

থিওরেম প্রুভিংয়ের জন্য লজিক্যাল ফ্রেমওয়ার্ক

Isabelle - Isabelle/HOL হলো একটি প্রুফ অ্যাসিস্ট্যান্ট যা গাণিতিক সূত্রগুলোকে একটি ফরমাল ভাষায় প্রকাশ করার অনুমতি দেয় এবং সেই সূত্রগুলো প্রমাণ করার জন্য টুল প্রদান করে। প্রধান অ্যাপ্লিকেশন হলো গাণিতিক প্রমাণের ফরম্যালাইজেশন এবং বিশেষ করে ফরমাল ভেরিফিকেশন, যার মধ্যে কম্পিউটার হার্ডওয়্যার বা সফটওয়্যারের সঠিকতা প্রমাণ করা এবং কম্পিউটার ভাষা ও প্রটোকলের প্রপার্টি প্রমাণ করা অন্তর্ভুক্ত।

Rocq - Rocq হলো একটি ইন্টারেক্টিভ থিওরেম প্রুভার যা আপনাকে থিওরেম ব্যবহার করে প্রোগ্রাম সংজ্ঞায়িত করতে এবং ইন্টারেক্টিভভাবে সঠিকতার মেশিন-চেকড প্রমাণ তৈরি করতে দেয়।

স্মার্ট কন্ট্রাক্টে দুর্বল প্যাটার্ন শনাক্ত করার জন্য সিম্বলিক এক্সিকিউশন-ভিত্তিক টুল

Manticore - সিম্বলিক এক্সিকিউশনের ওপর ভিত্তি করে EVM বাইটকোড বিশ্লেষণ করার একটি টুল।

hevm - hevm হলো EVM বাইটকোডের জন্য একটি সিম্বলিক এক্সিকিউশন ইঞ্জিন এবং ইকুইভ্যালেন্স চেকার।

GitHub (opens in a new tab)

Mythril - ইথিরিয়াম স্মার্ট কন্ট্রাক্টে দুর্বলতা শনাক্ত করার জন্য একটি সিম্বলিক এক্সিকিউশন টুল