স্মার্ট কন্ট্র্যাক্টের আনুষ্ঠানিক যাচাইকরণ

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

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

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

আনুষ্ঠানিক যাচাইকরণ কী?

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

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

একটি আনুষ্ঠানিক মডেল কী?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ইথেরিয়াম স্মার্ট কন্ট্র্যাক্টের জন্য আনুষ্ঠানিক যাচাইকরণ টুলস

আনুষ্ঠানিক স্পেসিফিকেশন তৈরির জন্য স্পেসিফিকেশন ভাষা

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

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

নথিপত্রopens in a new tab

Dafny - Dafny একটি যাচাইকরণ-প্রস্তুত প্রোগ্রামিং ভাষা যা কোডের সঠিকতা সম্পর্কে যুক্তি ও প্রমাণ করার জন্য উচ্চ-স্তরের টীকাগুলির উপর নির্ভর করে।

GitHubopens in a new tab

সঠিকতা পরীক্ষা করার জন্য প্রোগ্রাম ভেরিফায়ার

Certora Prover - Certora Prover স্মার্ট কন্ট্র্যাক্টে কোডের সঠিকতা পরীক্ষা করার জন্য একটি স্বয়ংক্রিয় আনুষ্ঠানিক যাচাইকরণ টুল। স্পেসিফিকেশনগুলি CVL (Certora Verification Language) এ লেখা হয়, যেখানে স্ট্যাটিক বিশ্লেষণ এবং কনস্ট্রেইন্ট-সলভিং এর সংমিশ্রণ ব্যবহার করে সম্পত্তি লঙ্ঘন সনাক্ত করা হয়।

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

GitHubopens in a new tab

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

GitHubopens in a new tab

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

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

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

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

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

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

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

GitHubopens in a new tab

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