ஸ்மார்ட் ஒப்பந்தங்களின் முறையான சரிபார்ப்பு

ஸ்மார்ட் ஒப்பந்தங்கள் பரவலாக்கப்பட்ட, நம்பிக்கையற்ற மற்றும் வலுவான பயன்பாடுகளை உருவாக்குவதை சாத்தியமாக்குகின்றன, இவை புதிய பயன்பாட்டு நிகழ்வுகளை அறிமுகப்படுத்துகின்றன மற்றும் பயனர்களுக்கான மதிப்பைத் திறக்கின்றன. ஸ்மார்ட் ஒப்பந்தங்கள் அதிக அளவிலான மதிப்பைக் கையாளுவதால், டெவலப்பர்களுக்கு பாதுகாப்பு என்பது ஒரு முக்கியமான கருத்தாகும்.

ஸ்மார்ட் ஒப்பந்தப் பாதுகாப்பை மேம்படுத்துவதற்குப் பரிந்துரைக்கப்படும் நுட்பங்களில் முறையான சரிபார்ப்பும் (Formal verification) ஒன்றாகும். நிரல்களைக் குறிப்பிடவும், வடிவமைக்கவும் மற்றும் சரிபார்க்கவும் முறையான வழிமுறைகளைப் (opens in a new tab) பயன்படுத்தும் முறையான சரிபார்ப்பு, முக்கியமான வன்பொருள் மற்றும் மென்பொருள் அமைப்புகளின் சரியான தன்மையை உறுதிப்படுத்த பல ஆண்டுகளாகப் பயன்படுத்தப்படுகிறது.

ஸ்மார்ட் ஒப்பந்தங்களில் செயல்படுத்தப்படும் போது, ஒரு ஒப்பந்தத்தின் வணிக தர்க்கம் முன்வரையறுக்கப்பட்ட விவரக்குறிப்பை (specification) பூர்த்தி செய்கிறது என்பதை முறையான சரிபார்ப்பு நிரூபிக்க முடியும். சோதனை போன்ற ஒப்பந்தக் குறியீட்டின் சரியான தன்மையை மதிப்பிடுவதற்கான பிற முறைகளுடன் ஒப்பிடுகையில், முறையான சரிபார்ப்பு ஒரு ஸ்மார்ட் ஒப்பந்தம் செயல்பாட்டு ரீதியாக சரியானது என்பதற்கான வலுவான உத்தரவாதங்களை அளிக்கிறது.

முறையான சரிபார்ப்பு என்றால் என்ன?

முறையான சரிபார்ப்பு என்பது ஒரு முறையான விவரக்குறிப்பைப் பொறுத்து ஒரு அமைப்பின் சரியான தன்மையை மதிப்பிடும் செயல்முறையைக் குறிக்கிறது. எளிமையான வார்த்தைகளில் கூறுவதானால், ஒரு அமைப்பின் நடத்தை சில தேவைகளைப் பூர்த்தி செய்கிறதா (அதாவது, நாம் விரும்புவதை அது செய்கிறதா) என்பதைச் சரிபார்க்க முறையான சரிபார்ப்பு அனுமதிக்கிறது.

அமைப்பின் (இந்த விஷயத்தில் ஒரு ஸ்மார்ட் ஒப்பந்தம்) எதிர்பார்க்கப்படும் நடத்தைகள் முறையான மாடலிங் மூலம் விவரிக்கப்படுகின்றன, அதே நேரத்தில் விவரக்குறிப்பு மொழிகள் முறையான பண்புகளை உருவாக்க உதவுகின்றன. முறையான சரிபார்ப்பு நுட்பங்கள் ஒரு ஒப்பந்தத்தின் செயலாக்கம் அதன் விவரக்குறிப்புடன் இணங்குகிறதா என்பதைச் சரிபார்த்து, முந்தையதின் சரியான தன்மைக்கான கணித ஆதாரத்தைப் பெறலாம். ஒரு ஒப்பந்தம் அதன் விவரக்குறிப்பை திருப்திப்படுத்தும் போது, அது "செயல்பாட்டு ரீதியாக சரியானது", "வடிவமைப்பால் சரியானது" அல்லது "கட்டுமானத்தால் சரியானது" என்று விவரிக்கப்படுகிறது.

முறையான மாதிரி (formal model) என்றால் என்ன?

கணினி அறிவியலில், முறையான மாதிரி (opens in a new tab) என்பது ஒரு கணக்கீட்டு செயல்முறையின் கணித விளக்கமாகும். நிரல்கள் கணிதச் செயல்பாடுகளாக (சமன்பாடுகள்) சுருக்கப்படுகின்றன, உள்ளீடு கொடுக்கப்பட்டால் செயல்பாடுகளுக்கான வெளியீடுகள் எவ்வாறு கணக்கிடப்படுகின்றன என்பதை மாதிரி விவரிக்கிறது.

முறையான மாதிரிகள் ஒரு நிரலின் நடத்தை பற்றிய பகுப்பாய்வை மதிப்பிடுவதற்கான சுருக்கத்தின் அளவை வழங்குகின்றன. முறையான மாதிரிகளின் இருப்பு ஒரு முறையான விவரக்குறிப்பை உருவாக்க அனுமதிக்கிறது, இது கேள்விக்குரிய மாதிரியின் விரும்பிய பண்புகளை விவரிக்கிறது.

முறையான சரிபார்ப்பிற்காக ஸ்மார்ட் ஒப்பந்தங்களை மாடலிங் செய்ய பல்வேறு நுட்பங்கள் பயன்படுத்தப்படுகின்றன. எடுத்துக்காட்டாக, சில மாதிரிகள் ஸ்மார்ட் ஒப்பந்தத்தின் உயர்-நிலை நடத்தையைப் பற்றி அறியப் பயன்படுத்தப்படுகின்றன. இந்த மாடலிங் நுட்பங்கள் ஸ்மார்ட் ஒப்பந்தங்களுக்கு பிளாக்-பாக்ஸ் பார்வையைப் பயன்படுத்துகின்றன, அவற்றை உள்ளீடுகளை ஏற்றுக்கொண்டு அந்த உள்ளீடுகளின் அடிப்படையில் கணக்கீட்டைச் செயல்படுத்தும் அமைப்புகளாகப் பார்க்கின்றன.

உயர்-நிலை மாதிரிகள் ஸ்மார்ட் ஒப்பந்தங்கள் மற்றும் வெளிப்புற முகவர்களான வெளிப்புறமாக சொந்தமான கணக்குகள் (EOAs), ஒப்பந்தக் கணக்குகள் மற்றும் பிளாக்செயின் சூழல் ஆகியவற்றுக்கு இடையேயான உறவில் கவனம் செலுத்துகின்றன. சில பயனர் தொடர்புகளுக்கு பதிலளிக்கும் விதமாக ஒரு ஒப்பந்தம் எவ்வாறு செயல்பட வேண்டும் என்பதைக் குறிப்பிடும் பண்புகளை வரையறுக்க இத்தகைய மாதிரிகள் பயனுள்ளதாக இருக்கும்.

மாறாக, பிற முறையான மாதிரிகள் ஸ்மார்ட் ஒப்பந்தத்தின் குறைந்த-நிலை நடத்தையில் கவனம் செலுத்துகின்றன. உயர்-நிலை மாதிரிகள் ஒரு ஒப்பந்தத்தின் செயல்பாட்டைப் பற்றி அறிய உதவினாலும், அவை செயலாக்கத்தின் உள் செயல்பாடுகள் பற்றிய விவரங்களைப் பிடிக்கத் தவறிவிடலாம். குறைந்த-நிலை மாதிரிகள் நிரல் பகுப்பாய்விற்கு ஒயிட்-பாக்ஸ் பார்வையைப் பயன்படுத்துகின்றன மற்றும் ஒப்பந்தத்தின் செயலாக்கத்திற்குத் தொடர்புடைய பண்புகளைப் பற்றி அறிய, நிரல் தடயங்கள் மற்றும் கட்டுப்பாட்டு ஓட்ட வரைபடங்கள் (opens in a new tab) போன்ற ஸ்மார்ட் ஒப்பந்தப் பயன்பாடுகளின் குறைந்த-நிலை பிரதிநிதித்துவங்களை நம்பியுள்ளன.

குறைந்த-நிலை மாதிரிகள் எத்தேரியத்தின் செயலாக்கச் சூழலில் (அதாவது, EVM) ஸ்மார்ட் ஒப்பந்தத்தின் உண்மையான செயலாக்கத்தைக் குறிப்பதால் அவை சிறந்ததாகக் கருதப்படுகின்றன. ஸ்மார்ட் ஒப்பந்தங்களில் முக்கியமான பாதுகாப்புப் பண்புகளை நிறுவுவதற்கும் சாத்தியமான பாதிப்புகளைக் கண்டறிவதற்கும் குறைந்த-நிலை மாடலிங் நுட்பங்கள் குறிப்பாகப் பயனுள்ளதாக இருக்கும்.

முறையான விவரக்குறிப்பு (formal specification) என்றால் என்ன?

விவரக்குறிப்பு என்பது ஒரு குறிப்பிட்ட அமைப்பு பூர்த்தி செய்ய வேண்டிய தொழில்நுட்பத் தேவையாகும். நிரலாக்கத்தில், விவரக்குறிப்புகள் ஒரு நிரலின் செயலாக்கம் பற்றிய பொதுவான யோசனைகளைக் குறிக்கின்றன (அதாவது, நிரல் என்ன செய்ய வேண்டும்).

ஸ்மார்ட் ஒப்பந்தங்களின் சூழலில், முறையான விவரக்குறிப்புகள் பண்புகளைக் குறிக்கின்றன—ஒரு ஒப்பந்தம் பூர்த்தி செய்ய வேண்டிய தேவைகளின் முறையான விளக்கங்கள். இத்தகைய பண்புகள் "மாறிலிகள்" (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) என்பவை "நேரத்தின் அடிப்படையில் தகுதிபெற்ற முன்மொழிவுகளைப் பற்றி பகுத்தறிவதற்கான விதிகள் (எ.கா., "நான் எப்போதும் பசியுடன் இருக்கிறேன்" அல்லது "நான் இறுதியில் பசியுடன் இருப்பேன்")." முறையான சரிபார்ப்பிற்குப் பயன்படுத்தப்படும் போது, நிலை-இயந்திரங்களாக வடிவமைக்கப்பட்ட அமைப்புகளின் சரியான நடத்தை பற்றிய கூற்றுகளைக் கூற தற்காலிக தர்க்கங்கள் பயன்படுத்தப்படுகின்றன. குறிப்பாக, ஒரு தற்காலிக தர்க்கம் ஒரு ஸ்மார்ட் ஒப்பந்தம் இருக்கக்கூடிய எதிர்கால நிலைகளையும் அது நிலைகளுக்கு இடையில் எவ்வாறு மாறுகிறது என்பதையும் விவரிக்கிறது.

உயர்-நிலை விவரக்குறிப்புகள் பொதுவாக ஸ்மார்ட் ஒப்பந்தங்களுக்கான இரண்டு முக்கியமான தற்காலிக பண்புகளைப் பிடிக்கின்றன: பாதுகாப்பு மற்றும் உயிரோட்டம். பாதுகாப்புப் பண்புகள் "எந்தவொரு கெட்டதும் நடக்காது" என்ற கருத்தைக் குறிக்கின்றன மற்றும் பொதுவாக மாறுபாட்டை வெளிப்படுத்துகின்றன. ஒரு பாதுகாப்புப் பண்பு முட்டுக்கட்டையிலிருந்து (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 இன் (அதாவது, நிரல்) நிலையின் முன்கணிப்புகள் ஆகும், இவை முறையே முன்நிபந்தனைகள் மற்றும் பின்நிபந்தனைகள் என முறையாக விவரிக்கப்படுகின்றன.

முன்நிபந்தனை என்பது ஒரு செயல்பாட்டின் சரியான செயலாக்கத்திற்குத் தேவையான நிபந்தனைகளை விவரிக்கும் ஒரு முன்கணிப்பு ஆகும்; ஒப்பந்தத்தை அழைக்கும் பயனர்கள் இந்தத் தேவையைப் பூர்த்தி செய்ய வேண்டும். பின்நிபந்தனை என்பது ஒரு செயல்பாடு சரியாகச் செயல்படுத்தப்பட்டால் அது நிறுவும் நிபந்தனையை விவரிக்கும் ஒரு முன்கணிப்பு ஆகும்; செயல்பாட்டை அழைத்த பிறகு இந்த நிபந்தனை உண்மையாக இருக்கும் என்று பயனர்கள் எதிர்பார்க்கலாம். ஹோர் தர்க்கத்தில் ஒரு மாறிலி என்பது ஒரு செயல்பாட்டின் செயலாக்கத்தால் பாதுகாக்கப்படும் ஒரு முன்கணிப்பு ஆகும் (அதாவது, அது மாறாது).

ஹோர்-பாணி விவரக்குறிப்புகள் பகுதி சரியான தன்மை அல்லது மொத்த சரியான தன்மை ஆகியவற்றுக்கு உத்தரவாதம் அளிக்க முடியும். செயல்பாடு செயல்படுத்தப்படுவதற்கு முன்பு முன்நிபந்தனை உண்மையாக இருந்தால், மற்றும் செயலாக்கம் முடிவடைந்தால், பின்நிபந்தனையும் உண்மையாக இருந்தால், ஒப்பந்தச் செயல்பாட்டின் செயலாக்கம் "பகுதியளவு சரியானது". செயல்பாடு செயல்படுத்துவதற்கு முன்பு ஒரு முன்நிபந்தனை உண்மையாக இருந்தால், செயலாக்கம் முடிவடையும் என்று உத்தரவாதம் அளிக்கப்பட்டு, அது முடிவடையும் போது, பின்நிபந்தனை உண்மையாக இருந்தால், மொத்த சரியான தன்மைக்கான ஆதாரம் பெறப்படுகிறது.

சில செயலாக்கங்கள் முடிவடைவதற்கு முன்பு தாமதமாகலாம் அல்லது முடிவடையாமலேயே போகலாம் என்பதால், மொத்த சரியான தன்மைக்கான ஆதாரத்தைப் பெறுவது கடினம். எத்தேரியத்தின் எரிவாயு பொறிமுறையானது முடிவற்ற நிரல் சுழல்களைத் தடுப்பதால் (செயலாக்கம் வெற்றிகரமாக முடிவடைகிறது அல்லது 'எரிவாயு தீர்ந்துவிட்டது' பிழையால் முடிவடைகிறது) செயலாக்கம் முடிவடைகிறதா என்ற கேள்வி விவாதத்திற்குரியது.

ஹோர் தர்க்கத்தைப் பயன்படுத்தி உருவாக்கப்பட்ட ஸ்மார்ட் ஒப்பந்த விவரக்குறிப்புகள் ஒரு ஒப்பந்தத்தில் செயல்பாடுகள் மற்றும் சுழல்களின் செயலாக்கத்திற்காக வரையறுக்கப்பட்ட முன்நிபந்தனைகள், பின்நிபந்தனைகள் மற்றும் மாறிலிகளைக் கொண்டிருக்கும். முன்நிபந்தனைகள் பெரும்பாலும் ஒரு செயல்பாட்டிற்கான தவறான உள்ளீடுகளின் சாத்தியத்தை உள்ளடக்குகின்றன, பின்நிபந்தனைகள் அத்தகைய உள்ளீடுகளுக்கு எதிர்பார்க்கப்படும் பதிலை விவரிக்கின்றன (எ.கா., ஒரு குறிப்பிட்ட விதிவிலக்கை எறிதல்). இந்த முறையில் ஹோர்-பாணி பண்புகள் ஒப்பந்தச் செயலாக்கங்களின் சரியான தன்மையை உறுதிப்படுத்துவதில் பயனுள்ளதாக இருக்கும்.

பல முறையான சரிபார்ப்பு கட்டமைப்புகள் செயல்பாடுகளின் சொற்பொருள் சரியான தன்மையை நிரூபிக்க ஹோர்-பாணி விவரக்குறிப்புகளைப் பயன்படுத்துகின்றன. Solidity இல் require மற்றும் assert அறிக்கைகளைப் பயன்படுத்துவதன் மூலம் ஹோர்-பாணி பண்புகளை (கூற்றுகளாக) நேரடியாக ஒப்பந்தக் குறியீட்டில் சேர்க்க முடியும்.

require அறிக்கைகள் ஒரு முன்நிபந்தனை அல்லது மாறிலியை வெளிப்படுத்துகின்றன மற்றும் பெரும்பாலும் பயனர் உள்ளீடுகளைச் சரிபார்க்கப் பயன்படுத்தப்படுகின்றன, அதே நேரத்தில் assert பாதுகாப்பிற்குத் தேவையான பின்நிபந்தனையைப் பிடிக்கிறது. எடுத்துக்காட்டாக, செயல்பாடுகளுக்கான சரியான அணுகல் கட்டுப்பாட்டை (பாதுகாப்புப் பண்புக்கு ஒரு எடுத்துக்காட்டு) அழைக்கும் கணக்கின் அடையாளத்தில் முன்நிபந்தனைச் சரிபார்ப்பாக require ஐப் பயன்படுத்தி அடையலாம். இதேபோல், ஒரு ஒப்பந்தத்தில் உள்ள நிலை மாறிகளின் அனுமதிக்கக்கூடிய மதிப்புகளின் மீதான மாறிலியை (எ.கா., புழக்கத்தில் உள்ள டோக்கன்களின் மொத்த எண்ணிக்கை) செயல்பாட்டுச் செயலாக்கத்திற்குப் பிறகு ஒப்பந்தத்தின் நிலையை உறுதிப்படுத்த assert ஐப் பயன்படுத்துவதன் மூலம் மீறலில் இருந்து பாதுகாக்க முடியும்.

சுவடு-நிலை பண்புகள் (Trace-level properties)

சுவடு அடிப்படையிலான விவரக்குறிப்புகள் ஒரு ஒப்பந்தத்தை வெவ்வேறு நிலைகளுக்கு இடையில் மாற்றும் செயல்பாடுகளையும் இந்தச் செயல்பாடுகளுக்கு இடையிலான உறவுகளையும் விவரிக்கின்றன. முன்பு விளக்கியபடி, தடயங்கள் என்பது ஒரு ஒப்பந்தத்தின் நிலையை ஒரு குறிப்பிட்ட வழியில் மாற்றும் செயல்பாடுகளின் வரிசைகளாகும்.

இந்த அணுகுமுறை ஸ்மார்ட் ஒப்பந்தங்களின் மாதிரியை நிலை-மாற்ற அமைப்புகளாக சில முன்வரையறுக்கப்பட்ட நிலைகளுடன் (நிலை மாறிகளால் விவரிக்கப்படுகிறது) முன்வரையறுக்கப்பட்ட மாற்றங்களின் தொகுப்புடன் (ஒப்பந்தச் செயல்பாடுகளால் விவரிக்கப்படுகிறது) நம்பியுள்ளது. மேலும், ஒரு நிரலின் செயலாக்க ஓட்டத்தின் வரைகலை பிரதிநிதித்துவமான கட்டுப்பாட்டு ஓட்ட வரைபடம் (opens in a new tab) (CFG), பெரும்பாலும் ஒரு ஒப்பந்தத்தின் செயல்பாட்டு சொற்பொருளை விவரிக்கப் பயன்படுத்தப்படுகிறது. இங்கே, ஒவ்வொரு சுவடும் கட்டுப்பாட்டு ஓட்ட வரைபடத்தில் ஒரு பாதையாகக் குறிக்கப்படுகிறது.

முதன்மையாக, ஸ்மார்ட் ஒப்பந்தங்களில் உள் செயலாக்கத்தின் வடிவங்களைப் பற்றி அறிய சுவடு-நிலை விவரக்குறிப்புகள் பயன்படுத்தப்படுகின்றன. சுவடு-நிலை விவரக்குறிப்புகளை உருவாக்குவதன் மூலம், ஸ்மார்ட் ஒப்பந்தத்திற்கான அனுமதிக்கக்கூடிய செயலாக்கப் பாதைகளை (அதாவது, நிலை மாற்றங்கள்) நாங்கள் வலியுறுத்துகிறோம். குறியீட்டுச் செயலாக்கம் போன்ற நுட்பங்களைப் பயன்படுத்தி, முறையான மாதிரியில் வரையறுக்கப்படாத பாதையைச் செயலாக்கம் ஒருபோதும் பின்பற்றாது என்பதை நாம் முறையாகச் சரிபார்க்கலாம்.

சுவடு-நிலை பண்புகளை விவரிக்க சில பொதுவில் அணுகக்கூடிய செயல்பாடுகளைக் கொண்ட DAO ஒப்பந்தத்தின் உதாரணத்தைப் பயன்படுத்துவோம். இங்கே, DAO ஒப்பந்தம் பயனர்களைப் பின்வரும் செயல்பாடுகளைச் செய்ய அனுமதிக்கிறது என்று கருதுகிறோம்:

நிதியை டெபாசிட் செய்தல்
நிதியை டெபாசிட் செய்த பிறகு ஒரு முன்மொழிவில் வாக்களித்தல்
அவர்கள் ஒரு முன்மொழிவில் வாக்களிக்கவில்லை என்றால் பணத்தைத் திரும்பப் பெறக் கோருதல்

எடுத்துக்காட்டு சுவடு-நிலை பண்புகள் "நிதியை டெபாசிட் செய்யாத பயனர்கள் ஒரு முன்மொழிவில் வாக்களிக்க முடியாது" அல்லது "ஒரு முன்மொழிவில் வாக்களிக்காத பயனர்கள் எப்போதும் பணத்தைத் திரும்பப் பெறக் கோர முடியும்" என்பதாக இருக்கலாம். இரண்டு பண்புகளும் விருப்பமான செயலாக்க வரிசைகளை வலியுறுத்துகின்றன (நிதியை டெபாசிட் செய்வதற்கு முன்பு வாக்களிப்பது நடக்காது மற்றும் ஒரு முன்மொழிவில் வாக்களித்த பிறகு பணத்தைத் திரும்பப் பெறுவது நடக்காது).

ஸ்மார்ட் ஒப்பந்தங்களின் முறையான சரிபார்ப்பிற்கான நுட்பங்கள்

மாதிரி சரிபார்ப்பு (Model checking)

மாதிரி சரிபார்ப்பு என்பது ஒரு முறையான சரிபார்ப்பு நுட்பமாகும், இதில் ஒரு அல்காரிதம் ஸ்மார்ட் ஒப்பந்தத்தின் முறையான மாதிரியை அதன் விவரக்குறிப்புக்கு எதிராகச் சரிபார்க்கிறது. மாதிரி சரிபார்ப்பில் ஸ்மார்ட் ஒப்பந்தங்கள் பெரும்பாலும் நிலை-மாற்ற அமைப்புகளாகக் குறிக்கப்படுகின்றன, அதே நேரத்தில் அனுமதிக்கக்கூடிய ஒப்பந்த நிலைகளின் பண்புகள் தற்காலிக தர்க்கத்தைப் பயன்படுத்தி வரையறுக்கப்படுகின்றன.

மாதிரி சரிபார்ப்பிற்கு ஒரு அமைப்பின் (அதாவது, ஒரு ஒப்பந்தம்) சுருக்கமான கணிதப் பிரதிநிதித்துவத்தை உருவாக்குவது மற்றும் முன்மொழிவு தர்க்கத்தில் (opens in a new tab) வேரூன்றிய சூத்திரங்களைப் பயன்படுத்தி இந்த அமைப்பின் பண்புகளை வெளிப்படுத்துவது தேவைப்படுகிறது. இது மாதிரி-சரிபார்ப்பு அல்காரிதத்தின் பணியை எளிதாக்குகிறது, அதாவது ஒரு கணித மாதிரி கொடுக்கப்பட்ட தர்க்கரீதியான சூத்திரத்தை திருப்திப்படுத்துகிறது என்பதை நிரூபிக்கிறது.

முறையான சரிபார்ப்பில் மாதிரி சரிபார்ப்பு முதன்மையாக காலப்போக்கில் ஒரு ஒப்பந்தத்தின் நடத்தையை விவரிக்கும் தற்காலிக பண்புகளை மதிப்பிடுவதற்குப் பயன்படுத்தப்படுகிறது. ஸ்மார்ட் ஒப்பந்தங்களுக்கான தற்காலிக பண்புகளில் பாதுகாப்பு மற்றும் உயிரோட்டம் ஆகியவை அடங்கும், இவற்றை நாங்கள் முன்பு விளக்கினோம்.

எடுத்துக்காட்டாக, அணுகல் கட்டுப்பாடு தொடர்பான பாதுகாப்புப் பண்பு (எ.கா., ஒப்பந்தத்தின் உரிமையாளர் மட்டுமே selfdestruct ஐ அழைக்க முடியும்) முறையான தர்க்கத்தில் எழுதப்படலாம். அதன்பிறகு, ஒப்பந்தம் இந்த முறையான விவரக்குறிப்பை திருப்திப்படுத்துகிறதா என்பதை மாதிரி-சரிபார்ப்பு அல்காரிதம் சரிபார்க்க முடியும்.

மாதிரி சரிபார்ப்பு நிலை விண்வெளி ஆய்வைப் பயன்படுத்துகிறது, இது ஸ்மார்ட் ஒப்பந்தத்தின் சாத்தியமான அனைத்து நிலைகளையும் உருவாக்குவது மற்றும் பண்பு மீறல்களை ஏற்படுத்தும் அணுகக்கூடிய நிலைகளைக் கண்டறிய முயற்சிப்பது ஆகியவற்றை உள்ளடக்கியது. இருப்பினும், இது எண்ணற்ற நிலைகளுக்கு வழிவகுக்கும் ("நிலை வெடிப்பு சிக்கல்" என்று அழைக்கப்படுகிறது), எனவே மாதிரி சரிபார்ப்பவர்கள் ஸ்மார்ட் ஒப்பந்தங்களின் திறமையான பகுப்பாய்வைச் சாத்தியமாக்க சுருக்க நுட்பங்களை நம்பியுள்ளனர்.

தேற்றம் நிரூபித்தல் (Theorem proving)

தேற்றம் நிரூபித்தல் என்பது ஸ்மார்ட் ஒப்பந்தங்கள் உட்பட நிரல்களின் சரியான தன்மை பற்றி கணித ரீதியாகப் பகுத்தறியும் ஒரு முறையாகும். இது ஒரு ஒப்பந்தத்தின் அமைப்பின் மாதிரி மற்றும் அதன் விவரக்குறிப்புகளைக் கணிதச் சூத்திரங்களாக (தர்க்க அறிக்கைகள்) மாற்றுவதை உள்ளடக்கியது.

தேற்றம் நிரூபிப்பதன் நோக்கம் இந்த அறிக்கைகளுக்கு இடையிலான தர்க்கரீதியான சமநிலையைச் சரிபார்ப்பதாகும். "தர்க்கரீதியான சமநிலை" ("தர்க்கரீதியான இரு-உட்குறிப்பு" என்றும் அழைக்கப்படுகிறது) என்பது இரண்டு அறிக்கைகளுக்கு இடையிலான ஒரு வகையான உறவாகும், அதாவது இரண்டாவது அறிக்கை உண்மையாக இருந்தால் மற்றும் இருந்தால் மட்டுமே முதல் அறிக்கை உண்மையாக இருக்கும்.

ஒரு ஒப்பந்தத்தின் மாதிரி மற்றும் அதன் பண்பு பற்றிய அறிக்கைகளுக்கு இடையிலான தேவையான உறவு (தர்க்கரீதியான சமநிலை) நிரூபிக்கக்கூடிய அறிக்கையாக (தேற்றம் என்று அழைக்கப்படுகிறது) வடிவமைக்கப்பட்டுள்ளது. அனுமானத்தின் முறையான அமைப்பைப் பயன்படுத்தி, தானியங்கு தேற்றம் நிரூபிப்பவர் தேற்றத்தின் செல்லுபடியாகும் தன்மையைச் சரிபார்க்க முடியும். வேறு வார்த்தைகளில் கூறுவதானால், ஒரு தேற்றம் நிரூபிப்பவர் ஒரு ஸ்மார்ட் ஒப்பந்தத்தின் மாதிரி அதன் விவரக்குறிப்புகளுடன் துல்லியமாகப் பொருந்துகிறது என்பதை உறுதியாக நிரூபிக்க முடியும்.

மாதிரி சரிபார்ப்பு ஒப்பந்தங்களை வரையறுக்கப்பட்ட நிலைகளைக் கொண்ட மாற்ற அமைப்புகளாக மாதிரியாக்கும் அதே வேளையில், தேற்றம் நிரூபித்தல் முடிவற்ற-நிலை அமைப்புகளின் பகுப்பாய்வைக் கையாள முடியும். இருப்பினும், ஒரு தர்க்கச் சிக்கல் "தீர்மானிக்கக்கூடியதா" இல்லையா என்பதை ஒரு தானியங்கு தேற்றம் நிரூபிப்பவரால் எப்போதும் அறிய முடியாது என்பதே இதன் பொருளாகும்.

இதன் விளைவாக, சரியான தன்மைக்கான ஆதாரங்களைப் பெறுவதில் தேற்றம் நிரூபிப்பவருக்கு வழிகாட்ட மனித உதவி பெரும்பாலும் தேவைப்படுகிறது. தேற்றம் நிரூபிப்பதில் மனித முயற்சியைப் பயன்படுத்துவது, முழுமையாகத் தானியங்குபடுத்தப்பட்ட மாதிரி சரிபார்ப்பை விடப் பயன்படுத்துவதற்கு அதிகச் செலவுமிக்கதாக ஆக்குகிறது.

குறியீட்டுச் செயலாக்கம் (Symbolic execution)

குறியீட்டுச் செயலாக்கம் என்பது கான்கிரீட் மதிப்புகளுக்கு (எ.கா., 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 ஐ உருவாக்கலாம்.

குறியீட்டுச் செயலாக்கம் ஒரு நிரலுக்கான உள்ளீடுகளை நம்பியிருப்பதால், மற்றும் அணுகக்கூடிய அனைத்து நிலைகளையும் ஆராய்வதற்கான உள்ளீடுகளின் தொகுப்பு முடிவற்றதாக இருப்பதால், இது இன்னும் ஒரு வகையான சோதனையாகவே உள்ளது. இருப்பினும், எடுத்துக்காட்டில் காட்டப்பட்டுள்ளபடி, பண்பு மீறல்களைத் தூண்டும் உள்ளீடுகளைக் கண்டறிவதற்கு வழக்கமான சோதனையை விடக் குறியீட்டுச் செயலாக்கம் மிகவும் திறமையானது.

மேலும், குறியீட்டுச் செயலாக்கம் ஒரு செயல்பாட்டிற்குத் தோராயமாக உள்ளீடுகளை உருவாக்கும் பிற பண்பு அடிப்படையிலான நுட்பங்களை (எ.கா., ஃபஸ்ஸிங்) விடக் குறைவான தவறான நேர்மறைகளை (false positives) உருவாக்குகிறது. குறியீட்டுச் செயலாக்கத்தின் போது பிழை நிலை தூண்டப்பட்டால், பிழையைத் தூண்டும் ஒரு கான்கிரீட் மதிப்பை உருவாக்கிச் சிக்கலை மீண்டும் உருவாக்க முடியும்.

குறியீட்டுச் செயலாக்கம் சரியான தன்மைக்கான சில அளவிலான கணித ஆதாரத்தையும் வழங்க முடியும். வழிதல் பாதுகாப்புடன் கூடிய ஒப்பந்தச் செயல்பாட்டின் பின்வரும் உதாரணத்தைக் கவனியுங்கள்:

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 இல் இயங்கும் நிரல்களுக்கான சொற்பொருள் பண்புகளைக் குறிப்பிடுவதையும் சரிபார்ப்பதையும் எளிதாக்குகிறது.

வேகமான மேம்பாட்டுச் சுழற்சி

மாதிரி சரிபார்ப்பு மற்றும் குறியீட்டுச் செயலாக்கம் போன்ற முறையான சரிபார்ப்பு நுட்பங்கள் பொதுவாக ஸ்மார்ட் ஒப்பந்தக் குறியீட்டின் வழக்கமான பகுப்பாய்வை விட (சோதனை அல்லது தணிக்கையின் போது செய்யப்படுகிறது) மிகவும் திறமையானவை. கான்கிரீட் மதிப்புகளைப் பயன்படுத்தும் சோதனையைப் போலல்லாமல் ("ஒரு பயனர் 5 ஈதரைத் திரும்பப் பெற முயன்றால் என்ன செய்வது?"), கூற்றுகளைச் சோதிக்க ("ஒரு பயனர் n ஈதரைத் திரும்பப் பெற முயன்றால் என்ன செய்வது?") முறையான சரிபார்ப்புக் குறியீட்டு மதிப்புகளை நம்பியிருப்பதே இதற்குக் காரணமாகும்.

குறியீட்டு உள்ளீட்டு மாறிகள் பல வகையான கான்கிரீட் மதிப்புகளை உள்ளடக்கும், எனவே முறையான சரிபார்ப்பு அணுகுமுறைகள் குறுகிய காலக்கட்டத்தில் அதிகக் குறியீடு கவரேஜை உறுதியளிக்கின்றன. திறம்படப் பயன்படுத்தப்படும் போது, முறையான சரிபார்ப்பு டெவலப்பர்களுக்கான மேம்பாட்டுச் சுழற்சியை துரிதப்படுத்தும்.

விலையுயர்ந்த வடிவமைப்புப் பிழைகளைக் குறைப்பதன் மூலம் பரவலாக்கப்பட்ட பயன்பாடுகளை (dapps) உருவாக்கும் செயல்முறையையும் முறையான சரிபார்ப்பு மேம்படுத்துகிறது. பாதிப்புகளைச் சரிசெய்ய ஒப்பந்தங்களை மேம்படுத்துவதற்கு (சாத்தியமான இடங்களில்) குறியீட்டுத் தளங்களை விரிவாக மீண்டும் எழுத வேண்டும் மற்றும் மேம்பாட்டிற்கு அதிக முயற்சி செலவிட வேண்டும். சோதனையாளர்கள் மற்றும் தணிக்கையாளர்களைத் தாண்டிச் செல்லக்கூடிய ஒப்பந்தச் செயலாக்கங்களில் உள்ள பல பிழைகளை முறையான சரிபார்ப்பால் கண்டறிய முடியும் மற்றும் ஒப்பந்தத்தை வரிசைப்படுத்துவதற்கு முன்பு அந்தச் சிக்கல்களைச் சரிசெய்யப் போதுமான வாய்ப்பை வழங்குகிறது.

முறையான சரிபார்ப்பின் குறைபாடுகள்

உடல் உழைப்பின் செலவு

முறையான சரிபார்ப்பு, குறிப்பாகச் சரியான தன்மைக்கான ஆதாரங்களைப் பெற ஒரு மனிதன் நிரூபிப்பவருக்கு வழிகாட்டும் அரை-தானியங்கி சரிபார்ப்புக்கு, கணிசமான உடல் உழைப்பு தேவைப்படுகிறது. மேலும், முறையான விவரக்குறிப்பை உருவாக்குவது என்பது உயர்-நிலை திறன் தேவைப்படும் ஒரு சிக்கலான செயலாகும்.

இந்தக் காரணிகள் (முயற்சி மற்றும் திறன்) சோதனை மற்றும் தணிக்கைகள் போன்ற ஒப்பந்தங்களில் சரியான தன்மையை மதிப்பிடுவதற்கான வழக்கமான முறைகளுடன் ஒப்பிடும்போது முறையான சரிபார்ப்பை அதிகத் தேவையுள்ளதாகவும் செலவுமிக்கதாகவும் ஆக்குகின்றன. ஆயினும்கூட, ஸ்மார்ட் ஒப்பந்தச் செயலாக்கங்களில் உள்ள பிழைகளின் விலையைக் கருத்தில் கொண்டு, முழுச் சரிபார்ப்புத் தணிக்கைக்கான செலவைச் செலுத்துவது நடைமுறைக்குரியது.

தவறான எதிர்மறைகள் (False negatives)

ஸ்மார்ட் ஒப்பந்தத்தின் செயலாக்கம் முறையான விவரக்குறிப்புடன் பொருந்துகிறதா என்பதை மட்டுமே முறையான சரிபார்ப்பால் சரிபார்க்க முடியும். எனவே, ஒரு ஸ்மார்ட் ஒப்பந்தத்தின் எதிர்பார்க்கப்படும் நடத்தைகளை விவரக்குறிப்புச் சரியாக விவரிக்கிறதா என்பதை உறுதிப்படுத்துவது முக்கியம்.

விவரக்குறிப்புகள் மோசமாக எழுதப்பட்டிருந்தால், பண்புகளின் மீறல்களை—பாதிக்கப்படக்கூடிய செயலாக்கங்களைச் சுட்டிக்காட்டும்—முறையான சரிபார்ப்புத் தணிக்கையால் கண்டறிய முடியாது. இந்த நிலையில், ஒப்பந்தம் பிழையற்றது என்று ஒரு டெவலப்பர் தவறாகக் கருதலாம்.

செயல்திறன் சிக்கல்கள்

முறையான சரிபார்ப்புப் பல செயல்திறன் சிக்கல்களைச் சந்திக்கிறது. எடுத்துக்காட்டாக, மாதிரி சரிபார்ப்பு மற்றும் குறியீட்டுச் சரிபார்ப்பின் போது முறையே எதிர்கொள்ளும் நிலை மற்றும் பாதை வெடிப்புச் சிக்கல்கள் சரிபார்ப்பு நடைமுறைகளைப் பாதிக்கலாம். மேலும், முறையான சரிபார்ப்புக் கருவிகள் பெரும்பாலும் SMT தீர்ப்பான்கள் மற்றும் பிற கட்டுப்பாட்டுத் தீர்ப்பான்களை அவற்றின் அடிப்படை அடுக்கில் பயன்படுத்துகின்றன, மேலும் இந்தத் தீர்ப்பான்கள் கணக்கீட்டு ரீதியாகத் தீவிரமான நடைமுறைகளை நம்பியுள்ளன.

மேலும், ஒரு நிரல் ஒருபோதும் முடிவடையாமல் போகலாம் என்பதால், ஒரு பண்பு (தர்க்கரீதியான சூத்திரமாக விவரிக்கப்பட்டுள்ளது) திருப்திப்படுத்த முடியுமா இல்லையா என்பதை ("தீர்மானிக்கக்கூடிய சிக்கல் (opens in a new tab)") நிரல் சரிபார்ப்பவர்களால் எப்போதும் தீர்மானிக்க முடியாது. எனவே, ஒரு ஒப்பந்தம் நன்கு குறிப்பிடப்பட்டிருந்தாலும் அதற்கான சில பண்புகளை நிரூபிப்பது சாத்தியமற்றதாக இருக்கலாம்.

எத்தேரியம் ஸ்மார்ட் ஒப்பந்தங்களுக்கான முறையான சரிபார்ப்புக் கருவிகள்

முறையான விவரக்குறிப்புகளை உருவாக்குவதற்கான விவரக்குறிப்பு மொழிகள்

Act: Act சேமிப்பகப் புதுப்பிப்புகள், முன்/பின் நிபந்தனைகள் மற்றும் ஒப்பந்த மாறிலிகளின் விவரக்குறிப்பை அனுமதிக்கிறது. இதன் கருவித் தொகுப்பில் Coq, SMT தீர்ப்பான்கள் அல்லது hevm வழியாகப் பல பண்புகளை நிரூபிக்கக்கூடிய ஆதாரப் பின்தளங்களும் (proof backends) உள்ளன.

Scribble - Scribble விவரக்குறிப்பு மொழியில் உள்ள குறியீட்டு சிறுகுறிப்புகளை விவரக்குறிப்பைச் சரிபார்க்கும் கான்கிரீட் கூற்றுகளாக Scribble மாற்றுகிறது.

ஆவணங்கள் (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) மற்றும் ஹார்ன் தீர்வு (Horn solving) ஆகியவற்றை அடிப்படையாகக் கொண்ட ஒரு உள்ளமைக்கப்பட்ட மாதிரி சரிபார்ப்பாகும். தொகுப்பின் போது ஒரு ஒப்பந்தத்தின் மூலக் குறியீடு விவரக்குறிப்புகளுடன் பொருந்துகிறதா என்பதை இது உறுதிப்படுத்துகிறது மற்றும் பாதுகாப்புப் பண்புகளின் மீறல்களை நிலையான முறையில் சரிபார்க்கிறது.

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 என்பது ஒரு ஊடாடும் தேற்றம் நிரூபிப்பவராகும், இது தேற்றங்களைப் பயன்படுத்தி நிரல்களை வரையறுக்கவும் மற்றும் இயந்திரத்தால் சரிபார்க்கப்பட்ட சரியான தன்மைக்கான ஆதாரங்களை ஊடாடும் வகையில் உருவாக்கவும் உங்களை அனுமதிக்கிறது.

ஸ்மார்ட் ஒப்பந்தங்களில் பாதிக்கப்படக்கூடிய வடிவங்களைக் கண்டறிவதற்கான குறியீட்டுச் செயலாக்க அடிப்படையிலான கருவிகள்

Manticore - குறியீட்டுச் செயலாக்கத்தின் அடிப்படையில் EVM பைட்கோடைப் பகுப்பாய்வு செய்வதற்கான ஒரு கருவி.

hevm - hevm என்பது EVM பைட்கோடுக்கான குறியீட்டுச் செயலாக்க இயந்திரம் மற்றும் சமநிலைச் சரிபார்ப்பாகும்.

GitHub (opens in a new tab)

Mythril - எத்தேரியம் ஸ்மார்ட் ஒப்பந்தங்களில் உள்ள பாதிப்புகளைக் கண்டறிவதற்கான குறியீட்டுச் செயலாக்கக் கருவி