ஸ்மார்ட் ஒப்பந்தங்களின் ஃபார்மல் வெரிஃபிகேஷன்

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

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

ஸ்மார்ட் ஒப்பந்தங்களில் அமலாக்கும்போது, formal verification ஒரு ஒப்பந்தத்தின் business logic-ஐ முன்பிரிவு செய்யப்பட்ட specification-க்கு உடன்படுகிறதா என்பதை நிரூபிக்க முடியும். Contract code-இன் சரியானதை மதிப்பீடு செய்யும் மற்ற முறைகளோடு ஒப்பிடுகையில், formal verification ஒரு ஸ்மார்ட் ஒப்பந்தம் செயல்திறனாகச் சரியானது என்பதற்கான வலுவான உறுதிகளை வழங்குகிறது.

Formal verification என்ன?

Formal verification என்பது ஒரு முறைமைவின் சரியான தன்மையை ஒரு formal specification-க்கு ஒப்பிடுவதற்கான செயல்முறை ஆகும். எளிதாகக் சொல்லுங்கள், formal verification மூலம் ஒரு முறைமை ஒரு சில தேவைகளைப் பூர்த்தி செய்யவா என்பதை சரிபார்க்க முடியும் (அதாவது, இது நாங்கள் விரும்பும் அளவுக்குச் செயற்படுகிறதா).

முறையமைப்பின் எதிர்பார்க்கப்படும் செயற்பாடுகள் (இந்தச் சந்தர்ப்பத்தில் ஒரு ஸ்மார்ட் ஒப்பந்தம்) formal modeling மூலம் விவரிக்கப்படுகின்றன, அதேசமயம் specification languages மூலம் formal properties உருவாக்கப்படுகின்றன. Formal verification techniques பின்னர், ஒரு ஒப்பந்தத்தின் அமலாக்கம் அதன் specification-க்கு ஏற்பதாக உள்ளதா என்பதைச் சரிபார்க்க முடியும் மற்றும் அதன் சரியானதன்மைக்குக் கணிதத சான்றை உருவாக்க முடியும். ஒரு ஒப்பந்தம் அதன் specification-ஐ பூர்த்தி செய்யும்போது, அதனை “செயல்திறனாகச் சரியானது”, செய்த முறைமையாகச் சரியானது”, அல்லது “உருவாக்கத்தில் சரியானது” எனக் குறிப்பிடப்படுகிறது.

ஃபார்மல் மாடல் என்றால் என்ன?

கணினி அறிவியலில், ஒரு ஃபார்மல் மாடல்opens in a new tab என்பது ஒரு கணக்கீட்டு செயல்முறையின் கணித விளக்கமாகும். Programs-ஐ கணித செயல்பாடுகளாக (equations) சுருக்கமாக்குவதால், model உள்ளீடு கொடுக்கப்பட்டால் functions-க்கு outputs எப்படி கணிக்கப்படுகின்றன என்பதைக் குறிப்பிடுகிறது.

Formal models என்பது ஒரு program-இன் behavior-ஐப் பற்றி ஆராய்வதற்கான ஒரு சுருக்கத்தை வழங்குகிறது. ஃபார்மல் மாடல்கள் இருப்பது ஒரு ஃபார்மல் ஸ்பெசிஃபிகேஷனை உருவாக்குவதை அனுமதிக்கிறது, இது கேள்விக்குரிய மாதிரியின் விரும்பிய பண்புகளை விவரிக்கிறது.

Smart contracts-இன் formal verification-க்கு மாறுபட்ட நுட்பங்கள் modeling செய்யப் பயன்படுத்தப்படுகின்றன. உதாரணமாக, சில models ஒரு smart contract-இன் மேம்பட்ட behavior-ஐப் பற்றிப் புரிந்துகொள்ள reasoning செய்யப் பயன்படுத்தப்படுகின்றன. இந்த modeling techniques, smart contracts-ஐ கருப்பு பெட்டி view ஆகக் கருதுகின்றன, இதை systems ஆகக் கருதுகின்றன, இதுவும் inputs-ஐ ஏற்றுக்கொண்டு அவற்றின் அடிப்படையில் கணக்கீடு செய்கிறது.

மேம்பட்ட models-ஐ, smart contracts மற்றும் வெளிப்புற முகவரிகள் (externally owned accounts (EOAs), contract accounts, மற்றும் blockchain environment போன்ற) ஆகியவற்றின் உறவுகளுக்கு மையமாகக் கொண்டு focus செய்கின்றன. குறிப்பிட்ட பயனர் தொடர்புக்களுக்குப் பதிலளிக்கும்போது ஒப்பந்தம் எப்படி நடந்து கொள்ள வேண்டும் என்பதைக் குறிப்பிட்ட பண்புகளை வரையறுக்க இந்த மாதிரியான models உதவிகரமாக உள்ளன.

மாறாக, மற்ற formal models ஒரு smart contract-இன் கீழ்மட்ட behavior-ஐ focus செய்கின்றன. மேம்பட்ட models ஒப்பந்தத்தின் செயல்பாட்டைப் பற்றிப் புரிந்துகொள்ள உதவியாயினும், அவை அமலாக்கத்தின் உட்புற செயல்பாடுகளின் விவரங்களைப் பதிவு செய்ய இயலாது. கீழ்மட்ட மாதிரிகள் நிரல் பகுப்பாய்விற்கு ஒரு வெள்ளை-பெட்டி பார்வையைப் பயன்படுத்துகின்றன மற்றும் ஸ்மார்ட் ஒப்பந்தப் பயன்பாடுகளின் கீழ்-நிலை பிரதிநிதித்துவங்களான நிரல் தடங்கள் மற்றும் கட்டுப்பாட்டுப் பாய்வு வரைபடங்கள்opens in a new tab போன்றவற்றைச் சார்ந்து, ஒரு ஒப்பந்தத்தின் செயல்பாட்டிற்குப் பொருத்தமான பண்புகளைப் பற்றி பகுத்தறிய உதவுகின்றன.

கீழ்மட்ட மாதிரிகள் சிறந்ததாகக் கருதப்படுகின்றன, ஏனெனில் அவை Ethereum-இன் செயலாக்க சூழலில் (அதாவது, EVM) ஒரு ஸ்மார்ட் ஒப்பந்தத்தின் உண்மையான செயல்பாட்டைப் பிரதிநிதித்துவப்படுத்துகின்றன. கீழ்மட்ட modeling techniques குறிப்பாக smart contracts-இல் முக்கியமான பாதுகாப்பு பண்புகளை நிலைநிறுத்த மற்றும் சாத்தியமான குறைகளைக் கண்டறிவதில் மிகவும் பயனுள்ளதாக உள்ளன.

ஃபார்மல் ஸ்பெசிஃபிகேஷன் என்றால் என்ன?

சாதாரண விளக்கம் என்பது ஒரு குறிப்பிட்ட அமைப்பு பூர்த்தி செய்ய வேண்டிய தொழில்நுட்ப தேவையை மட்டும் குறிக்கிறது. Programming-இல், specifications என்பது ஒரு program-இன் execution-ஐப் பற்றிய பொது எண்ணங்களை (அதாவது, program என்ன செய்ய வேண்டும் என்பதைக் குறிப்பிடும்).

ஸ்மார்ட் ஒப்பந்தங்களின் பின்னணியில், ஃபார்மல் ஸ்பெசிஃபிகேஷன்கள் பண்புகளைக் குறிக்கின்றன—அதாவது ஒரு ஒப்பந்தம் பூர்த்தி செய்ய வேண்டிய தேவைகளின் முறையான விளக்கங்கள். இந்த மாதிரியான பண்புகள் "invariants" என்று விவரிக்கப்படுகின்றன மற்றும் ஒப்பந்தத்தின் execution-ஐப் பற்றிய தார்க்கிகமான assertions ஆகும், இது எந்தவித விதிவிலக்குகள் இல்லாமல் ஒவ்வொரு சாத்தியமான சூழலிலும் உண்மையாகவே இருக்க வேண்டும்.

எனவே, ஒரு formal specification என்பது formal language-இல் எழுதப்பட்ட statements-க்களின் தொகுப்பாகக் கருதலாம், இது smart contract-இன் நோக்கத்திற்கான execution-ஐ விவரிக்கின்றது. Specifications ஒரு ஒப்பந்தத்தின் பண்புகளைக் குறிக்கின்றன மற்றும் ஒப்பந்தம் வெவ்வேறு சூழல்களில் எப்படி நடந்து கொள்ள வேண்டும் என்பதைக் குறிப்பிடுகின்றன. Formal verification-இன் நோக்கம், ஒரு smart contract இந்தப் பண்புகளை (invariants) கொண்டுள்ளதா என்பதையும், execution போது இந்தப் பண்புகள் மீறப்படவில்லையா என்பதையும் தீர்மானிப்பதே ஆகும்.

Formal specifications ஒரு smart contract-இன் பாதுகாப்பான அமலாக்கங்களை உருவாக்குவதில் மிகவும் முக்கியமானதாகும். Contracts இல் invariants-ஐச் செயல்படுத்தத் தவறினால் அல்லது execution-இல் அவற்றின் பண்புகள் மீறப்பட்டால், அது செயல்திறனை கெடுக்க அல்லது தீய நோக்கத்துடன் exploits ஏற்படுத்தும் சாத்தியம் உள்ளது.

ஸ்மார்ட் ஒப்பந்தங்களுக்கான ஃபார்மல் ஸ்பெசிஃபிகேஷன்களின் வகைகள்

Formal specifications என்பது ஒரு program-இன் execution சரியானதாக உள்ளதா என்பதை mathematical reasoning மூலம் தீர்மானிக்க உதவுகிறது. Formal models போலவே, formal specifications ஒரு ஒப்பந்தத்தின் செயலாக்கத்தின் மேம்பட்ட properties அல்லது கீழ்மட்ட behavior-ஐப் பதிவுசெய்யக்கூடியவை.

ஒரு நிரலின் பண்புகளைப் பற்றி முறையான பகுத்தறிவுக்கு அனுமதிக்கும் நிரல் தர்க்கத்தின்opens in a new tab கூறுகளைப் பயன்படுத்தி ஃபார்மல் ஸ்பெசிஃபிகேஷன்கள் பெறப்படுகின்றன. Program logic-ல், ஒரு program என்ன செய்ய வேண்டும் என்பதைக் குறிக்கும் formal rules இருக்கின்றன. ஃபார்மல் ஸ்பெசிஃபிகேஷன்களை உருவாக்குவதில் அடையக்கூடிய தர்க்கம்opens in a new tab, தற்காலிக தர்க்கம்opens in a new tab மற்றும் ஹோர் தர்க்கம்opens in a new tab உள்ளிட்ட பல்வேறு நிரல் தர்க்கங்கள் பயன்படுத்தப்படுகின்றன.

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

உயர்-நிலை விவரக்குறிப்புகள்

High-level specification அல்லது "model-oriented specification" எனப்படும் ஒரு high-level behavior-ஐ விவரிக்கிறது. உயர்-நிலை விவரக்குறிப்புகள் ஒரு ஸ்மார்ட் ஒப்பந்தத்தை வரையறுக்கப்பட்ட நிலை இயந்திரமாகopens in a new tab (FSM) மாதிரியாக்குகின்றன, இது செயல்பாடுகளைச் செய்வதன் மூலம் நிலைகளுக்கு இடையில் மாறக்கூடியது, FSM மாதிரிக்கான முறையான பண்புகளை வரையறுக்க தற்காலிக தர்க்கம் பயன்படுத்தப்படுகிறது.

தற்காலிக தர்க்கங்கள்opens in a new tab என்பவை "காலத்தின் அடிப்படையில் தகுதிப்படுத்தப்பட்ட முன்மொழிவுகளைப் பற்றி பகுத்தறிவதற்கான விதிகள் (உதாரணமாக, "நான் எப்போதும் பசியாக இருக்கிறேன்" அல்லது "நான் இறுதியில் பசியாக இருப்பேன்")." . Formal verification-இல், temporal logics பயன்பாடு, state-machines ஆக model செய்யப்பட்ட அமைப்புகளின் சரியான behavior பற்றிய assertions-ஐ வெளிப்படுத்துவதற்காகப் பயன்படுத்தப்படுகிறது. குறிப்பாக, temporal logic என்பது ஒரு smart contract எதிர்காலத்தில் இருக்கக்கூடிய states மற்றும் அவை states இடையே எவ்வாறு மாற்றப்படுகின்றன என்பதைக் குறிக்கிறது.

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

உதாரணமாக, ERC-20 டோக்கன் ஒப்பந்தங்களில் transfer() அல்லது transferFrom() பயன்படுத்துவதற்கான நிபந்தனைகளை உள்ளடக்கிய இந்த பாதுகாப்புத் தேவையைக் கவனியுங்கள்: “அனுப்புநரின் இருப்பு, அனுப்பப்பட வேண்டிய டோக்கன்களின் கோரப்பட்ட அளவை விட ஒருபோதும் குறைவாக இருக்காது.”. இந்த contract invariant-ஐ ஒரு natural-language விளக்கமாக இருந்து, அதை ஒரு formal (mathematical) specification-ஆக மாற்றி, அதன் செல்லுபடியை கடுமையாகச் சரிபார்க்க முடியும்.

Liveness properties என்பது “நல்லது எதாவது இறுதியில் நடக்கிறது” என்பதைக் கூறுகிறது மற்றும் ஒப்பந்தம் பல்வேறு நிலைகளுக்கு மாறும் திறனைப் பற்றிக் கவலைப்படுகிறது. ஒரு liveness property-க்கு எடுத்துக்காட்டு “liquidity” ஆகும், இது ஒப்பந்தம் தனது balances-ஐப் பயனர்களுக்குக் கோரிக்கையின் அடிப்படையில் மாற்றும் திறனைக் குறிக்கிறது. இந்தப் பண்பு மீறப்பட்டால், பாரிட்டி வாலட் சம்பவத்தில்opens in a new tab நடந்தது போல, பயனர்கள் ஒப்பந்தத்தில் சேமிக்கப்பட்ட சொத்துக்களை எடுக்க முடியாமல் போகும்.

கீழ்-நிலை விவரக்குறிப்புகள்

High-level specifications ஒரு ஒப்பந்தத்தின் finite-state model-ஐ தொடக்கமாக எடுத்துக் கொண்டு, இந்த model-இன் விரும்பிய properties-ஐ வரையறுக்கிறது. மாறாக, Low-level specifications (அல்லது "property-oriented specifications") பெரும்பாலும் programs (smart contracts) ஆகியவற்றை கணிதக் கருவிகளின் தொகுப்பாக முறைமைகளாக மாடல் செய்து, இந்த முறைமைகளின் சரியான behavior-ஐ விவரிக்கின்றன.

எளிமையாகச் சொன்னால், கீழ்-நிலை விவரக்குறிப்புகள் நிரல் தடங்களை பகுப்பாய்வு செய்து, இந்த தடங்களின் மீது ஒரு ஸ்மார்ட் ஒப்பந்தத்தின் பண்புகளை வரையறுக்க முயற்சிக்கின்றன. Traces என்பது ஒரு smart contract-இன் நிலையை மாற்றும் செயலாக்கங்களின் வரிசையைக் குறிக்கின்றன; எனவே, Low-level specifications ஒப்பந்தத்தின் உள் செயலாக்கத்திற்கான தேவைகளை விவரிக்க உதவுகிறது.

Low-level formal specifications-ஐ Hoare-style properties அல்லது execution paths-இல் invariants என வழங்க முடியும்.

ஹோர்-பாணி பண்புகள்

ஹோர் தர்க்கம்opens in a new tab ஸ்மார்ட் ஒப்பந்தங்கள் உட்பட நிரல்களின் சரியான தன்மையைப் பற்றி பகுத்தறிவதற்கான முறையான விதிகளின் தொகுப்பை வழங்குகிறது. ஒரு ஹோர்-பாணி பண்பு {P}c{Q} என்ற ஹோர் மும்மையால் குறிப்பிடப்படுகிறது, இதில் c என்பது ஒரு நிரல் மற்றும் P மற்றும் Q ஆகியவை c-இன் (அதாவது, நிரலின்) நிலையின் மீதான பயனிலைகள் ஆகும், இவை முறையே முன்நிபந்தனைகள் மற்றும் பின்நிபந்தனைகள் என முறையாக விவரிக்கப்படுகின்றன.

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

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

டோட்டல் correctness-ஐ உறுதிப்படுத்தும் ப்ரூஃப் பெறுவது கடினம், ஏனெனில் சில செயல்பாடுகள் நிறைவடைய முன்னர் தாமதமாவது அல்லது முடிவடையாமலே போவது போன்ற பிரச்சனைகள் இருக்கலாம். அதுவே, செயல்பாடு முடிவடைவதா என்பது ஒரு அவசியம் என்ற கேள்விக்குப் பதிலளிக்க வேண்டும், ஏனெனில் Ethereum-இன் காஸ் மெக்கானிசம் முடிவற்ற ப்ரோக்ராம் லூப்கள்-ஐ தடுக்கிறது (செயல்பாடு வெற்றிகரமாக நிறைவடையும் அல்லது 'out-of-gas' பிழை காரணமாக முடிவடையும்).

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

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

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

தட-நிலை பண்புகள்

ட்ரேஸ்-பேஸ்டு ஸ்பெசிபிகேஷன்கள் ஒரு கான்ட்ராக்ட் பல்வேறு ஸ்டேட்களுக்கு இடையில் ட்ரான்சிஷன் செய்யும் செயல்பாடுகளை, மற்றும் இந்த ஆபரேஷன்கள் ஒன்றுக்கொன்று தொடர்புடையதை விவரிக்கின்றன. முன்னர் விளக்கப்பட்டபடி, ட்ரேஸ்கள் ஒரு குறிப்பிட்ட முறையில் ஒரு கான்ட்ராக்டின் ஸ்டேட்-ஐ மாற்றும் ஆபரேஷன்களின் தொடர்ச்சியாகும்.

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

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

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

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

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

ஸ்மார்ட் ஒப்பந்தங்களின் ஃபார்மல் வெரிஃபிகேஷனுக்கான நுட்பங்கள்

மாடல் சரிபார்ப்பு

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

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

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

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

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

தேற்றம் நிரூபணம்

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

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

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

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

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

குறியீட்டு செயலாக்கம்

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

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

ஒரு ஸ்மார்ட் ஒப்பந்தத்தின் செயல்பாடு 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 மற்றும் (z >= x) மற்றும் (z >= y) மற்றும் (z < x அல்லது z < y) என்ற சூத்திரத்தை திருப்திப்படுத்த வேண்டும். அத்தகைய சூத்திரத்தை தீர்ப்பது சாத்தியமில்லை, எனவே இது safe_add செயல்பாடு ஒருபோதும் ஓவர்ஃப்ளோ ஆகாது என்பதற்கான கணித ஆதாரமாக செயல்படுகிறது.

ஏன் ஸ்மார்ட் கான்ட்ராக்ட்களுக்கு பார்மல் வெரிபிகேஷனை பயன்படுத்த வேண்டும்? ஃபார்மல் வெரிஃபிகேஷனின் நன்மைகள்

நம்பகத்தன்மைக்கான தேவை

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

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

செயல்பாட்டு சரியான தன்மையை நிரூபித்தல்

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

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

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

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

சிறந்த சரிபார்ப்பு இலக்குகள்

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

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

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

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

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

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

ஃபார்மல் வெரிஃபிகேஷனின் குறைபாடுகள்

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

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

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

தவறான எதிர்மறைகள்

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

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

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

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

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

Ethereum ஸ்மார்ட் ஒப்பந்தங்களுக்கான ஃபார்மல் வெரிஃபிகேஷன் கருவிகள்

ஃபார்மல் ஸ்பெசிஃபிகேஷன்களை உருவாக்குவதற்கான விவரக்குறிப்பு மொழிகள்

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

GitHubopens in a new tab

solc-verify - solc-verify என்பது Solidity கம்பைலரின் நீட்டிக்கப்பட்ட பதிப்பாகும், இது சிறுகுறிப்புகள் மற்றும் மாடுலர் நிரல் சரிபார்ப்பைப் பயன்படுத்தி Solidity குறியீட்டில் தானியங்கு ஃபார்மல் வெரிஃபிகேஷனைச் செய்ய முடியும்.

GitHubopens in a new tab

KEVM - KEVM என்பது K கட்டமைப்பில் எழுதப்பட்ட Ethereum Virtual Machine (EVM)-இன் ஒரு முறையான சொற்பொருளாகும். KEVM இயக்கக்கூடியது மற்றும் அடையக்கூடிய தர்க்கத்தைப் பயன்படுத்தி சில பண்பு-தொடர்பான உறுதிமொழிகளை நிரூபிக்க முடியும்.

தேற்றம் நிரூபணத்திற்கான தர்க்கரீதியான கட்டமைப்புகள்

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

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

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

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

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

GitHubopens in a new tab

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