స్మార్ట్ కాంట్రాక్టుల ఫార్మల్ వెరిఫికేషన్

స్మార్ట్ కాంట్రాక్టులు వికేంద్రీకృత, విశ్వాసం లేని మరియు పటిష్టమైన అప్లికేషన్‌లను సృష్టించడం సాధ్యం చేస్తున్నాయి, ఇవి కొత్త వినియోగ-కేసులను పరిచయం చేస్తాయి మరియు వినియోగదారుల కోసం విలువను అన్‌లాక్ చేస్తాయి. స్మార్ట్ కాంట్రాక్టులు పెద్ద మొత్తంలో విలువను నిర్వహిస్తాయి కాబట్టి, డెవలపర్‌లకు భద్రత ఒక క్లిష్టమైన పరిశీలన.

స్మార్ట్ కాంట్రాక్ట్ భద్రతను మెరుగుపరచడానికి సిఫార్సు చేయబడిన టెక్నిక్‌లలో ఫార్మల్ వెరిఫికేషన్ ఒకటి. ప్రోగ్రామ్‌లను పేర్కొనడం, రూపకల్పన చేయడం మరియు ధృవీకరించడం కోసం ఫార్మల్ పద్ధతులను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 (అంటే, ప్రోగ్రామ్) యొక్క స్టేట్‌పై ఉన్న ప్రెడికేట్లు, వరుసగా ప్రీకండిషన్లు మరియు పోస్ట్‌కండిషన్లుగా ఫార్మల్‌గా వివరించబడ్డాయి.

ప్రీకండిషన్ అనేది ఒక ఫంక్షన్ యొక్క సరైన ఎగ్జిక్యూషన్‌కు అవసరమైన షరతులను వివరించే ప్రెడికేట్; కాంట్రాక్ట్‌లోకి కాల్ చేసే వినియోగదారులు ఈ అవసరాన్ని తప్పనిసరిగా తీర్చాలి. పోస్ట్‌కండిషన్ అనేది సరిగ్గా ఎగ్జిక్యూట్ చేస్తే ఒక ఫంక్షన్ స్థాపించే షరతును వివరించే ప్రెడికేట్; ఫంక్షన్‌లోకి కాల్ చేసిన తర్వాత వినియోగదారులు ఈ షరతు నిజమని ఆశించవచ్చు. హోరే లాజిక్‌లో ఒక ఇన్‌వేరియంట్ అనేది ఒక ఫంక్షన్ యొక్క ఎగ్జిక్యూషన్ ద్వారా సంరక్షించబడే ప్రెడికేట్ (అంటే, అది మారదు).

హోరే-శైలి స్పెసిఫికేషన్లు పాక్షిక సరియైనత లేదా _మొత్తం సరియైనత_కు హామీ ఇవ్వగలవు. ఫంక్షన్ ఎగ్జిక్యూట్ చేయడానికి ముందు ప్రీకండిషన్ నిజమై, మరియు ఎగ్జిక్యూషన్ ముగిస్తే, పోస్ట్‌కండిషన్ కూడా నిజమైతే, ఒక కాంట్రాక్ట్ ఫంక్షన్ యొక్క ఇంప్లిమెంటేషన్ "పాక్షికంగా సరైనది" అవుతుంది. ఫంక్షన్ ఎగ్జిక్యూట్ చేయడానికి ముందు ప్రీకండిషన్ నిజమై, ఎగ్జిక్యూషన్ ముగుస్తుందని హామీ ఇవ్వబడి, మరియు అది ముగిసినప్పుడు పోస్ట్‌కండిషన్ నిజమైతే, మొత్తం సరియైనత రుజువు పొందబడుతుంది.

మొత్తం సరియైనత రుజువు పొందడం కష్టం, ఎందుకంటే కొన్ని ఎగ్జిక్యూషన్‌లు ముగిసే ముందు ఆలస్యం కావచ్చు లేదా అస్సలు ముగియకపోవచ్చు. అయినప్పటికీ, ఇతీరియము యొక్క గ్యాస్ మెకానిజం అనంతమైన ప్రోగ్రామ్ లూప్‌లను నివారిస్తుంది కాబట్టి ఎగ్జిక్యూషన్ ముగుస్తుందా లేదా అనే ప్రశ్న వాదించదగ్గ విధంగా వివాదాస్పద విషయం (ఎగ్జిక్యూషన్ విజయవంతంగా ముగుస్తుంది లేదా 'గ్యాస్ అయిపోయింది' లోపం కారణంగా ముగుస్తుంది).

హోరే లాజిక్ ఉపయోగించి సృష్టించబడిన స్మార్ట్ కాంట్రాక్ట్ స్పెసిఫికేషన్లు, ఒక కాంట్రాక్ట్‌లో ఫంక్షన్లు మరియు లూప్‌ల ఎగ్జిక్యూషన్ కొరకు నిర్వచించబడిన ప్రీకండిషన్లు, పోస్ట్‌కండిషన్లు, మరియు ఇన్‌వేరియంట్లను కలిగి ఉంటాయి. ప్రీకండిషన్లు తరచుగా ఒక ఫంక్షన్‌కు తప్పు ఇన్‌పుట్‌ల యొక్క అవకాశాన్ని కలిగి ఉంటాయి, పోస్ట్‌కండిషన్లు అటువంటి ఇన్‌పుట్‌లకు ఆశించిన ప్రతిస్పందనను వివరిస్తాయి (ఉదా., ఒక నిర్దిష్ట మినహాయింపును త్రో చేయడం). ఈ పద్ధతిలో, కాంట్రాక్ట్ ఇంప్లిమెంటేషన్‌ల సరియైనతను నిర్ధారించడానికి హోరే-శైలి లక్షణాలు ప్రభావవంతంగా ఉంటాయి.

అనేక ఫార్మల్ వెరిఫికేషన్ ఫ్రేమ్‌వర్క్‌లు ఫంక్షన్ల యొక్క సెమాంటిక్ సరియైనతను నిరూపించడానికి హోరే-శైలి స్పెసిఫికేషన్లను ఉపయోగిస్తాయి. Solidity లో require మరియు assert స్టేట్‌మెంట్లను ఉపయోగించి హోరే-శైలి లక్షణాలను (నిర్ధారణలుగా) నేరుగా కాంట్రాక్ట్ కోడ్‌కు జోడించడం కూడా సాధ్యమే.

require స్టేట్‌మెంట్లు ఒక ప్రీకండిషన్ లేదా ఇన్‌వేరియంట్‌ను వ్యక్తపరుస్తాయి మరియు తరచుగా వినియోగదారు ఇన్‌పుట్‌లను ధృవీకరించడానికి ఉపయోగిస్తారు, అయితే assert భద్రత కొరకు అవసరమైన పోస్ట్‌కండిషన్‌ను క్యాప్చర్ చేస్తుంది. ఉదాహరణకు, కాలింగ్ ఖాతా యొక్క గుర్తింపుపై ప్రీకండిషన్ తనిఖీగా require ఉపయోగించి ఫంక్షన్ల కొరకు సరైన యాక్సెస్ కంట్రోల్ (ఒక భద్రతా లక్షణానికి ఉదాహరణ) సాధించవచ్చు. అదేవిధంగా, ఫంక్షన్ ఎగ్జిక్యూషన్ తర్వాత కాంట్రాక్ట్ యొక్క స్టేట్‌ను నిర్ధారించడానికి assert ను ఉపయోగించడం ద్వారా ఒక కాంట్రాక్ట్‌లోని స్టేట్ వేరియబుల్స్ యొక్క అనుమతించదగిన విలువలపై ఇన్‌వేరియంట్ (ఉదా., సర్క్యులేషన్‌లో ఉన్న మొత్తం టోకెన్ల సంఖ్య) ను ఉల్లంఘన నుండి రక్షించవచ్చు.

ట్రేస్-లెవల్ లక్షణాలు

ట్రేస్-ఆధారిత స్పెసిఫికేషన్లు ఒక కాంట్రాక్టును వివిధ స్టేట్‌ల మధ్య మార్చే ఆపరేషన్లను మరియు ఈ ఆపరేషన్ల మధ్య సంబంధాలను వివరిస్తాయి. ముందు వివరించినట్లుగా, ట్రేస్‌లు ఒక కాంట్రాక్ట్ యొక్క స్టేట్‌ను ఒక నిర్దిష్ట మార్గంలో మార్చే ఆపరేషన్ల క్రమాలు.

ఈ విధానం స్మార్ట్ కాంట్రాక్టుల మోడల్‌పై ఆధారపడి ఉంటుంది, ఇవి ముందుగా నిర్వచించిన కొన్ని స్టేట్‌లతో (స్టేట్ వేరియబుల్స్ ద్వారా వర్ణించబడినవి) మరియు ముందుగా నిర్వచించిన ట్రాన్సిషన్ల సమితితో (కాంట్రాక్ట్ ఫంక్షన్ల ద్వారా వర్ణించబడినవి) స్టేట్-ట్రాన్సిషన్ సిస్టమ్‌లుగా ఉంటాయి. ఇంకా, ఒక కంట్రోల్ ఫ్లో గ్రాఫ్opens in a new tab (CFG), ఇది ఒక ప్రోగ్రామ్ యొక్క ఎగ్జిక్యూషన్ ఫ్లో యొక్క గ్రాఫికల్ ప్రాతినిధ్యం, తరచుగా ఒక కాంట్రాక్ట్ యొక్క కార్యాచరణ సెమాంటిక్స్‌ను వివరించడానికి ఉపయోగించబడుతుంది. ఇక్కడ, ప్రతి ట్రేస్ కంట్రోల్ ఫ్లో గ్రాఫ్‌పై ఒక పాత్‌గా సూచించబడుతుంది.

ప్రధానంగా, ట్రేస్-లెవల్ స్పెసిఫికేషన్లు స్మార్ట్ కాంట్రాక్టులలోని అంతర్గత ఎగ్జిక్యూషన్ ప్యాట్రన్ల గురించి తర్కించడానికి ఉపయోగించబడతాయి. ట్రేస్-లెవల్ స్పెసిఫికేషన్లను సృష్టించడం ద్వారా, మేము ఒక స్మార్ట్ కాంట్రాక్ట్ కొరకు అనుమతించదగిన ఎగ్జిక్యూషన్ పాత్‌లను (అంటే, స్టేట్ ట్రాన్సిషన్లు) నిర్ధారిస్తాము. సింబాలిక్ ఎగ్జిక్యూషన్ వంటి టెక్నిక్‌లను ఉపయోగించి, ఫార్మల్ మోడల్‌లో నిర్వచించని పాత్‌ను ఎగ్జిక్యూషన్ ఎప్పుడూ అనుసరించదని మనం ఫార్మల్‌గా ధృవీకరించవచ్చు.

ట్రేస్-లెవల్ లక్షణాలను వివరించడానికి కొన్ని పబ్లిక్‌గా అందుబాటులో ఉన్న ఫంక్షన్లను కలిగి ఉన్న ఒక DAO కాంట్రాక్ట్ యొక్క ఉదాహరణను ఉపయోగిద్దాం. ఇక్కడ, DAO కాంట్రాక్ట్ వినియోగదారులను క్రింది ఆపరేషన్లను చేయడానికి అనుమతిస్తుందని మనం ఊహిస్తున్నాము:

• నిధులు డిపాజిట్ చేయండి

• నిధులు డిపాజిట్ చేసిన తర్వాత ఒక ప్రతిపాదనపై ఓటు వేయండి

• వారు ఒక ప్రతిపాదనపై ఓటు వేయకపోతే రీఫండ్ క్లెయిమ్ చేయండి

ఉదాహరణ ట్రేస్-లెవల్ లక్షణాలు "నిధులు డిపాజిట్ చేయని వినియోగదారులు ఒక ప్రతిపాదనపై ఓటు వేయలేరు" లేదా "ఒక ప్రతిపాదనపై ఓటు వేయని వినియోగదారులు ఎల్లప్పుడూ రీఫండ్ క్లెయిమ్ చేయగలగాలి" కావచ్చు. రెండు లక్షణాలు ప్రాధాన్యత ఇవ్వబడిన ఎగ్జిక్యూషన్ క్రమాలను నిర్ధారిస్తాయి (నిధులు డిపాజిట్ చేయడానికి ముందు ఓటింగ్ జరగదు మరియు ఒక ప్రతిపాదనపై ఓటింగ్ చేసిన తర్వాత రీఫండ్‌లు క్లెయిమ్ చేయడం జరగదు).

స్మార్ట్ కాంట్రాక్టుల ఫార్మల్ వెరిఫికేషన్ కొరకు టెక్నిక్‌లు

మోడల్ చెకింగ్

మోడల్ చెకింగ్ అనేది ఒక ఫార్మల్ వెరిఫికేషన్ టెక్నిక్, దీనిలో ఒక అల్గోరిథం ఒక స్మార్ట్ కాంట్రాక్ట్ యొక్క ఫార్మల్ మోడల్‌ను దాని స్పెసిఫికేషన్‌కు వ్యతిరేకంగా తనిఖీ చేస్తుంది. మోడల్ చెకింగ్‌లో స్మార్ట్ కాంట్రాక్టులు తరచుగా స్టేట్-ట్రాన్సిషన్ సిస్టమ్‌లుగా సూచించబడతాయి, అయితే అనుమతించదగిన కాంట్రాక్ట్ స్టేట్‌లపై లక్షణాలు టెంపోరల్ లాజిక్ ఉపయోగించి నిర్వచించబడతాయి.

మోడల్ చెకింగ్‌కు ఒక సిస్టమ్ (అంటే, ఒక కాంట్రాక్ట్) యొక్క వియుక్త గణిత ప్రాతినిధ్యాన్ని సృష్టించడం మరియు ప్రపోజిషనల్ లాజిక్opens in a new tabలో పాతుకుపోయిన ఫార్ములాలను ఉపయోగించి ఈ సిస్టమ్ యొక్క లక్షణాలను వ్యక్తపరచడం అవసరం. ఇది మోడల్-చెకింగ్ అల్గోరిథం యొక్క పనిని సులభతరం చేస్తుంది, అవి ఒక గణిత మోడల్ ఇవ్వబడిన లాజికల్ ఫార్ములాను సంతృప్తిపరుస్తుందని నిరూపించడం.

ఫార్మల్ వెరిఫికేషన్‌లో మోడల్ చెకింగ్ ప్రధానంగా కాలక్రమేణా ఒక కాంట్రాక్ట్ యొక్క ప్రవర్తనను వివరించే టెంపోరల్ లక్షణాలను మూల్యాంకనం చేయడానికి ఉపయోగించబడుతుంది. స్మార్ట్ కాంట్రాక్టుల కొరకు టెంపోరల్ లక్షణాలలో భద్రత మరియు సజీవత్వం ఉన్నాయి, వీటిని మనం ముందు వివరించాము.

ఉదాహరణకు, యాక్సెస్ కంట్రోల్‌కు సంబంధించిన ఒక భద్రతా లక్షణాన్ని (ఉదా., కాంట్రాక్ట్ యజమాని మాత్రమే selfdestructను కాల్ చేయగలడు) ఫార్మల్ లాజిక్‌లో వ్రాయవచ్చు. ఆ తర్వాత, మోడల్-చెకింగ్ అల్గోరిథం కాంట్రాక్ట్ ఈ ఫార్మల్ స్పెసిఫికేషన్‌ను సంతృప్తిపరుస్తుందో లేదో ధృవీకరించగలదు.

మోడల్ చెకింగ్ స్టేట్ స్పేస్ ఎక్స్‌ప్లోరేషన్‌ను ఉపయోగిస్తుంది, దీనిలో ఒక స్మార్ట్ కాంట్రాక్ట్ యొక్క అన్ని సాధ్యమైన స్టేట్‌లను నిర్మించడం మరియు ప్రాపర్టీ ఉల్లంఘనలకు దారితీసే చేరుకోగల స్టేట్‌లను కనుగొనడానికి ప్రయత్నించడం జరుగుతుంది. అయినప్పటికీ, ఇది అనంతమైన సంఖ్యలో స్టేట్‌లకు దారితీయవచ్చు ("స్టేట్ ఎక్స్‌ప్లోజన్ సమస్య"గా పిలువబడుతుంది), అందువల్ల మోడల్ చెక్కర్‌లు స్మార్ట్ కాంట్రాక్టుల సమర్థవంతమైన విశ్లేషణను సాధ్యం చేయడానికి అబ్స్ట్రాక్షన్ టెక్నిక్‌లపై ఆధారపడతాయి.

థీరమ్ ప్రూవింగ్

థీరమ్ ప్రూవింగ్ అనేది స్మార్ట్ కాంట్రాక్టులతో సహా ప్రోగ్రామ్‌ల సరియైనత గురించి గణితశాస్త్రపరంగా తర్కించే ఒక పద్ధతి. ఇది ఒక కాంట్రాక్ట్ యొక్క సిస్టమ్ మోడల్‌ను మరియు దాని స్పెసిఫికేషన్‌లను గణిత ఫార్ములాలుగా (లాజిక్ స్టేట్‌మెంట్లు) మార్చడం కలిగి ఉంటుంది.

థీరమ్ ప్రూవింగ్ యొక్క లక్ష్యం ఈ స్టేట్‌మెంట్ల మధ్య లాజికల్ ఈక్వివలెన్స్‌ను ధృవీకరించడం. “లాజికల్ ఈక్వివలెన్స్” (దీనిని “లాజికల్ బై-ఇంప్లికేషన్” అని కూడా పిలుస్తారు) అనేది రెండు స్టేట్‌మెంట్ల మధ్య ఒక రకమైన సంబంధం, దీనిలో మొదటి స్టేట్‌మెంట్ నిజమైతే మాత్రమే రెండవ స్టేట్‌మెంట్ నిజమవుతుంది.

ఒక కాంట్రాక్ట్ యొక్క మోడల్ మరియు దాని ప్రాపర్టీ గురించిన స్టేట్‌మెంట్ల మధ్య అవసరమైన సంబంధం (లాజికల్ ఈక్వివలెన్స్) ఒక రుజువు చేయదగిన స్టేట్‌మెంట్‌గా (థీరమ్ అని పిలువబడుతుంది) రూపొందించబడింది. అనుమితి యొక్క ఒక ఫార్మల్ సిస్టమ్ ఉపయోగించి, ఆటోమేటెడ్ థీరమ్ ప్రూవర్ థీరమ్ యొక్క ప్రామాణికతను ధృవీకరించగలదు. మరో మాటలో చెప్పాలంటే, ఒక థీరమ్ ప్రూవర్ ఒక స్మార్ట్ కాంట్రాక్ట్ యొక్క మోడల్ దాని స్పెసిఫికేషన్‌లతో సరిగ్గా సరిపోలుతుందని నిశ్చయంగా నిరూపించగలదు.

మోడల్ చెకింగ్ కాంట్రాక్టులను పరిమిత స్టేట్‌లతో ట్రాన్సిషన్ సిస్టమ్‌లుగా మోడల్ చేస్తుండగా, థీరమ్ ప్రూవింగ్ అనంత-స్టేట్ సిస్టమ్‌ల విశ్లేషణను నిర్వహించగలదు. అయినప్పటికీ, దీని అర్థం ఒక ఆటోమేటెడ్ థీరమ్ ప్రూవర్ ఎల్లప్పుడూ ఒక లాజిక్ సమస్య "నిర్ణయించదగినది" కాదా అని తెలుసుకోలేదు.

ఫలితంగా, సరియైనత రుజువులను ఉత్పాదించడంలో థీరమ్ ప్రూవర్‌కు మార్గనిర్దేశం చేయడానికి తరచుగా మానవ సహాయం అవసరం. థీరమ్ ప్రూవింగ్‌లో మానవ ప్రయత్నాన్ని ఉపయోగించడం వల్ల ఇది పూర్తిగా ఆటోమేటెడ్ అయిన మోడల్ చెకింగ్ కంటే ఎక్కువ ఖర్చుతో కూడుకున్నది.

సింబాలిక్ ఎగ్జిక్యూషన్

సింబాలిక్ ఎగ్జిక్యూషన్ అనేది కాంక్రీట్ విలువలు (ఉదా., x == 5) బదులుగా సింబాలిక్ విలువలు (ఉదా., x > 5) ఉపయోగించి ఫంక్షన్లను ఎగ్జిక్యూట్ చేయడం ద్వారా ఒక స్మార్ట్ కాంట్రాక్ట్‌ను విశ్లేషించే ఒక పద్ధతి. ఒక ఫార్మల్ వెరిఫికేషన్ టెక్నిక్‌గా, సింబాలిక్ ఎగ్జిక్యూషన్ ఒక కాంట్రాక్ట్ కోడ్‌లోని ట్రేస్-లెవల్ లక్షణాల గురించి ఫార్మల్‌గా తర్కించడానికి ఉపయోగించబడుతుంది.

సింబాలిక్ ఎగ్జిక్యూషన్ ఒక ఎగ్జిక్యూషన్ ట్రేస్‌ను సింబాలిక్ ఇన్‌పుట్ విలువలపై ఒక గణిత ఫార్ములాగా సూచిస్తుంది, దీనిని పాత్ ప్రెడికేట్ అని కూడా పిలుస్తారు. ఒక SMT సాల్వర్opens in a new tab ఒక పాత్ ప్రెడికేట్ "సంతృప్తికరంగా" ఉందా (అంటే, ఫార్ములాను సంతృప్తిపరిచే విలువ ఉందా) అని తనిఖీ చేయడానికి ఉపయోగించబడుతుంది. ఒక దుర్బలమైన పాత్ సంతృప్తికరంగా ఉంటే, SMT సాల్వర్ ఎగ్జిక్యూషన్‌ను ఆ పాత్ వైపు నడిపించే ఒక కాంక్రీట్ విలువను ఉత్పత్తి చేస్తుంది.

ఒక స్మార్ట్ కాంట్రాక్ట్ యొక్క ఫంక్షన్ ఇన్‌పుట్‌గా ఒక uint విలువ (x) తీసుకుంటుందని మరియు x 5 కంటే ఎక్కువ మరియు 10 కంటే తక్కువ ఉన్నప్పుడు రివర్ట్ అవుతుందని అనుకుందాం. సాధారణ టెస్టింగ్ ప్రక్రియను ఉపయోగించి లోపాన్ని ప్రేరేపించే x విలువను కనుగొనడానికి, వాస్తవంగా లోపాన్ని ప్రేరేపించే ఇన్‌పుట్‌ను కనుగొంటామనే హామీ లేకుండా డజన్ల కొద్దీ టెస్ట్ కేసులను (లేదా అంతకంటే ఎక్కువ) అమలు చేయాల్సి ఉంటుంది.

దీనికి విరుద్ధంగా, ఒక సింబాలిక్ ఎగ్జిక్యూషన్ టూల్ ఫంక్షన్‌ను సింబాలిక్ విలువతో ఎగ్జిక్యూట్ చేస్తుంది: X > 5 ∧ X < 10 (అంటే, x 5 కంటే ఎక్కువ మరియు x 10 కంటే తక్కువ). సంబంధిత పాత్ ప్రెడికేట్ x = X > 5 ∧ X < 10 తర్వాత పరిష్కరించడానికి ఒక SMT సాల్వర్‌కు ఇవ్వబడుతుంది. ఒక నిర్దిష్ట విలువ ఫార్ములా x = X > 5 ∧ X < 10 ను సంతృప్తిపరిస్తే, SMT సాల్వర్ దానిని లెక్కిస్తుంది—ఉదాహరణకు, సాల్వర్ x కొరకు 7 విలువను ఉత్పత్తి చేయవచ్చు.

సింబాలిక్ ఎగ్జిక్యూషన్ ఒక ప్రోగ్రామ్‌కు ఇన్‌పుట్‌లపై ఆధారపడి ఉంటుంది, మరియు అన్ని చేరుకోగల స్టేట్‌లను అన్వేషించడానికి ఇన్‌పుట్‌ల సమితి అనంతంగా ఉండవచ్చు కాబట్టి, ఇది ఇప్పటికీ ఒక రకమైన టెస్టింగ్. అయినప్పటికీ, ఉదాహరణలో చూపినట్లుగా, ప్రాపర్టీ ఉల్లంఘనలను ప్రేరేపించే ఇన్‌పుట్‌లను కనుగొనడంలో సింబాలిక్ ఎగ్జిక్యూషన్ సాధారణ టెస్టింగ్ కంటే సమర్థవంతమైనది.

అంతేకాకుండా, ఫంక్షన్‌కు ఇన్‌పుట్‌లను యాదృచ్ఛికంగా ఉత్పత్తి చేసే ఇతర ప్రాపర్టీ-ఆధారిత టెక్నిక్‌ల (ఉదా., ఫజ్జింగ్) కంటే సింబాలిక్ ఎగ్జిక్యూషన్ తక్కువ తప్పుడు పాజిటివ్‌లను ఉత్పత్తి చేస్తుంది. సింబాలిక్ ఎగ్జిక్యూషన్ సమయంలో ఒక లోపం స్టేట్ ప్రేరేపించబడితే, లోపాన్ని ప్రేరేపించే ఒక కాంక్రీట్ విలువను ఉత్పత్తి చేసి, సమస్యను పునరుత్పత్తి చేయడం సాధ్యమవుతుంది.

సింబాలిక్ ఎగ్జిక్యూషన్ కొంతవరకు గణిత రుజువును కూడా అందించగలదు. పొంగి పొర్లు రక్షణతో కూడిన కాంట్రాక్ట్ ఫంక్షన్ యొక్క క్రింది ఉదాహరణను పరిగణించండి:

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  return z;
8}

పూర్ణాంక ఓవర్‌ఫ్లోకు దారితీసే ఒక ఎగ్జిక్యూషన్ ట్రేస్ ఫార్ములాను సంతృప్తిపరచాల్సి ఉంటుంది: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) అటువంటి ఫార్ములా పరిష్కరించబడే అవకాశం లేదు, అందువల్ల ఇది safe_add ఫంక్షన్ ఎప్పుడూ ఓవర్‌ఫ్లో కాదని గణిత రుజువుగా పనిచేస్తుంది.

స్మార్ట్ కాంట్రాక్టుల కొరకు ఫార్మల్ వెరిఫికేషన్‌ను ఎందుకు ఉపయోగించాలి?

విశ్వసనీయత అవసరం

ఫార్మల్ వెరిఫికేషన్ అనేది భద్రత-క్లిష్టమైన సిస్టమ్‌ల సరియైనతను అంచనా వేయడానికి ఉపయోగించబడుతుంది, దీని వైఫల్యం మరణం, గాయం లేదా ఆర్థిక నష్టం వంటి వినాశకరమైన పరిణామాలకు దారితీయవచ్చు. స్మార్ట్ కాంట్రాక్టులు భారీ మొత్తంలో విలువను నియంత్రించే అధిక-విలువ గల అప్లికేషన్లు, మరియు డిజైన్‌లో సాధారణ లోపాలు వినియోగదారులకు తిరిగి పొందలేని నష్టాలకుopens in a new tab దారితీయవచ్చు. అయితే, ఒక కాంట్రాక్ట్‌ను మోహరించడానికి ముందు ఫార్మల్‌గా ధృవీకరించడం, బ్లాక్‌చైన్‌లో నడుస్తున్నప్పుడు అది ఆశించిన విధంగా పని చేస్తుందనే హామీలను పెంచుతుంది.

విశ్వసనీయత అనేది ఏ స్మార్ట్ కాంట్రాక్ట్‌లోనైనా చాలా కావలసిన నాణ్యత, ప్రత్యేకించి ఇతీరియము వర్చువల్ మషీన్ (EVM)లో మోహరించిన సంకేత భాష సాధారణంగా మార్చలేనిది కాబట్టి. ప్రయోగం తర్వాత అప్‌గ్రేడ్‌లు సులభంగా అందుబాటులో లేనందున, కాంట్రాక్టుల విశ్వసనీయతను హామీ ఇవ్వాల్సిన అవసరం ఫార్మల్ వెరిఫికేషన్‌ను అవసరం చేస్తుంది. ఫార్మల్ వెరిఫికేషన్ పూర్ణాంక అండర్‌ఫ్లోలు మరియు ఓవర్‌ఫ్లోలు, పునః ప్రవేశం, మరియు పేలవమైన గ్యాస్ ఆప్టిమైజేషన్‌లు వంటి క్లిష్టమైన సమస్యలను గుర్తించగలదు, ఇవి ఆడిటర్లు మరియు టెస్టర్లను దాటవేయవచ్చు.

క్రియాత్మక సరియైనతను నిరూపించండి

ప్రోగ్రామ్ టెస్టింగ్ అనేది ఒక స్మార్ట్ కాంట్రాక్ట్ కొన్ని అవసరాలను సంతృప్తిపరుస్తుందని నిరూపించడానికి అత్యంత సాధారణ పద్ధతి. ఇది ఒక కాంట్రాక్ట్‌ను అది నిర్వహించాల్సిన డేటా యొక్క నమూనాతో అమలు చేయడం మరియు దాని ప్రవర్తనను విశ్లేషించడం కలిగి ఉంటుంది. నమూనా డేటా కొరకు కాంట్రాక్ట్ ఆశించిన ఫలితాలను తిరిగి ఇస్తే, అప్పుడు అభివృద్ధి చేసేవాళ్లకు దాని సరియైనత యొక్క లక్ష్య రుజువు ఉంటుంది.

అయితే, ఈ విధానం నమూనాలో భాగం కాని ఇన్‌పుట్ విలువల కొరకు సరైన అమలును నిరూపించలేదు. అందువల్ల, ఒక కాంట్రాక్ట్‌ను టెస్ట్ చేయడం బగ్‌లను గుర్తించడంలో సహాయపడవచ్చు (అంటే, కొన్ని సంకేత భాష పాత్‌లు ఎగ్జిక్యూషన్ సమయంలో కావలసిన ఫలితాలను తిరిగి ఇవ్వడంలో విఫలమైతే), కానీ అది బగ్‌ల లేమిని నిశ్చయంగా నిరూపించలేదు.

దీనికి విరుద్ధంగా, ఫార్మల్ వెరిఫికేషన్ ఒక స్మార్ట్ కాంట్రాక్ట్ అనంతమైన శ్రేణి ఎగ్జిక్యూషన్‌ల కొరకు అవసరాలను సంతృప్తిపరుస్తుందని ఫార్మల్‌గా నిరూపించగలదు, కాంట్రాక్ట్‌ను అసలు నడపకుండానే. దీనికి సరైన కాంట్రాక్ట్ ప్రవర్తనలను ఖచ్చితంగా వివరించే ఒక ఫార్మల్ స్పెసిఫికేషన్‌ను సృష్టించడం మరియు కాంట్రాక్ట్ యొక్క సిస్టమ్ యొక్క ఒక ఫార్మల్ (గణిత) మోడల్‌ను అభివృద్ధి చేయడం అవసరం. అప్పుడు మనం కాంట్రాక్ట్ యొక్క మోడల్ మరియు దాని స్పెసిఫికేషన్ మధ్య స్థిరత్వం కొరకు తనిఖీ చేయడానికి ఒక ఫార్మల్ ప్రూఫ్ విధానాన్ని అనుసరించవచ్చు.

ఫార్మల్ వెరిఫికేషన్‌తో, ఒక కాంట్రాక్ట్ యొక్క వ్యాపార లాజిక్ అవసరాలను సంతృప్తిపరుస్తుందా అని ధృవీకరించే ప్రశ్న ఒక గణిత ప్రతిపాదన, దానిని నిరూపించవచ్చు లేదా నిరాకరించవచ్చు. ఒక ప్రతిపాదనను ఫార్మల్‌గా నిరూపించడం ద్వారా, మనం పరిమిత సంఖ్యలో దశలతో అనంతమైన సంఖ్యలో టెస్ట్ కేసులను ధృవీకరించవచ్చు. ఈ పద్ధతిలో ఫార్మల్ వెరిఫికేషన్ ఒక స్పెసిఫికేషన్‌కు సంబంధించి ఒక కాంట్రాక్ట్ క్రియాత్మకంగా సరైనదని నిరూపించడానికి మంచి అవకాశాలను కలిగి ఉంటుంది.

ఆదర్శ ధృవీకరణ లక్ష్యాలు

ఒక ధృవీకరణ లక్ష్యం ఫార్మల్‌గా ధృవీకరించాల్సిన సిస్టమ్‌ను వివరిస్తుంది. ఫార్మల్ వెరిఫికేషన్ "ఎంబెడెడ్ సిస్టమ్స్" (ఒక పెద్ద సిస్టమ్‌లో భాగమైన చిన్న, సరళమైన సాఫ్ట్‌వేర్ ముక్కలు) లో ఉత్తమంగా ఉపయోగించబడుతుంది. అవి డొమైన్-నిర్దిష్ట లక్షణాలను ధృవీకరించడానికి ఉపకరణాలను సవరించడం సులభతరం చేస్తుంది కాబట్టి, కొన్ని నియమాలు ఉన్న ప్రత్యేక డొమైన్‌లకు కూడా అవి ఆదర్శంగా ఉంటాయి.

స్మార్ట్ కాంట్రాక్టులు—కనీసం, కొంతవరకు—రెండు అవసరాలను తీరుస్తాయి. ఉదాహరణకు, ఇతీరియము కాంట్రాక్టుల చిన్న పరిమాణం వాటిని ఫార్మల్ వెరిఫికేషన్‌కు అనుకూలంగా చేస్తుంది. అదేవిధంగా, EVM సరళమైన నియమాలను అనుసరిస్తుంది, ఇది EVM లో నడుస్తున్న ప్రోగ్రామ్‌ల కొరకు సెమాంటిక్ లక్షణాలను నిర్దేశించడం మరియు ధృవీకరించడం సులభతరం చేస్తుంది.

వేగవంతమైన అభివృద్ధి చక్రం

మోడల్ చెకింగ్ మరియు సింబాలిక్ ఎగ్జిక్యూషన్ వంటి ఫార్మల్ వెరిఫికేషన్ టెక్నిక్‌లు, సాధారణంగా స్మార్ట్ కాంట్రాక్ట్ సంకేత భాష యొక్క సాధారణ విశ్లేషణ (టెస్టింగ్ లేదా ఆడిటింగ్ సమయంలో నిర్వహించబడేది) కంటే సమర్థవంతమైనవి. ఎందుకంటే ఫార్మల్ వెరిఫికేషన్ నిర్ధారణలను టెస్ట్ చేయడానికి సింబాలిక్ విలువలపై ఆధారపడుతుంది ("ఒక వినియోగదారుడు n ఈథర్‌లను ఉపసంహరించుకోవడానికి ప్రయత్నిస్తే ఏమిటి?") టెస్టింగ్ వలె కాకుండా ఇది కాంక్రీట్ విలువలను ఉపయోగిస్తుంది ("ఒక వినియోగదారుడు 5 ఈథర్‌లను ఉపసంహరించుకోవడానికి ప్రయత్నిస్తే ఏమిటి?").

సింబాలిక్ ఇన్‌పుట్ వేరియబుల్స్ బహుళ కాంక్రీట్ విలువల వర్గాలను కవర్ చేయగలవు, కాబట్టి ఫార్మల్ వెరిఫికేషన్ విధానాలు తక్కువ సమయంలో ఎక్కువ సంకేత భాష కవరేజీని వాగ్దానం చేస్తాయి. సమర్థవంతంగా ఉపయోగించినప్పుడు, ఫార్మల్ వెరిఫికేషన్ అభివృద్ధి చేసేవాళ్ల కొరకు అభివృద్ధి చక్రాన్ని వేగవంతం చేస్తుంది.

ఫార్మల్ వెరిఫికేషన్ ఖరీదైన డిజైన్ లోపాలను తగ్గించడం ద్వారా వికేంద్రీకృత అప్లికేషన్లు (డాప్స్) నిర్మించే ప్రక్రియను కూడా మెరుగుపరుస్తుంది. దుర్బలత్వాలను సరిచేయడానికి కాంట్రాక్టులను (సాధ్యమైన చోట) అప్‌గ్రేడ్ చేయడానికి కోడ్‌బేస్‌ల విస్తృతమైన పునర్విమర్శ మరియు అభివృద్ధిపై ఎక్కువ కృషి అవసరం. ఫార్మల్ వెరిఫికేషన్ కాంట్రాక్ట్ ఇంప్లిమెంటేషన్‌లలో అనేక లోపాలను గుర్తించగలదు, ఇవి టెస్టర్లు మరియు ఆడిటర్లను దాటవేయవచ్చు మరియు ఒక కాంట్రాక్ట్‌ను మోహరించడానికి ముందు ఆ సమస్యలను పరిష్కరించడానికి తగినంత అవకాశాన్ని అందిస్తుంది.

ఫార్మల్ వెరిఫికేషన్ యొక్క లోపాలు

మానవ శ్రమ ఖర్చు

ఫార్మల్ వెరిఫికేషన్, ప్రత్యేకించి సెమీ-ఆటోమేటెడ్ వెరిఫికేషన్, దీనిలో ఒక మానవుడు సరియైనత రుజువులను ఉత్పాదించడానికి ప్రూవర్‌కు మార్గనిర్దేశం చేస్తాడు, గణనీయమైన మానవ శ్రమ అవసరం. అంతేకాకుండా, ఫార్మల్ స్పెసిఫికేషన్ సృష్టించడం అనేది అధిక స్థాయి నైపుణ్యం అవసరమయ్యే ఒక సంక్లిష్టమైన కార్యాచరణ.

ఈ కారకాలు (ప్రయత్నం మరియు నైపుణ్యం) ఫార్మల్ వెరిఫికేషన్‌ను టెస్టింగ్ మరియు ఆడిట్‌లు వంటి కాంట్రాక్టులలో సరియైనతను అంచనా వేసే సాధారణ పద్ధతులతో పోలిస్తే ఎక్కువ డిమాండ్ మరియు ఖరీదైనవిగా చేస్తాయి. అయినప్పటికీ, స్మార్ట్ కాంట్రాక్ట్ ఇంప్లిమెంటేషన్‌లలో లోపాల ఖర్చును బట్టి, పూర్తి ధృవీకరణ ఆడిట్ కొరకు ఖర్చు చెల్లించడం ఆచరణాత్మకమైనది.

తప్పుడు నెగెటివ్‌లు

ఫార్మల్ వెరిఫికేషన్ స్మార్ట్ కాంట్రాక్ట్ యొక్క ఎగ్జిక్యూషన్ ఫార్మల్ స్పెసిఫికేషన్‌తో సరిపోలుతుందో లేదో మాత్రమే తనిఖీ చేయగలదు. అలాగే, స్పెసిఫికేషన్ స్మార్ట్ కాంట్రాక్ట్ యొక్క ఆశించిన ప్రవర్తనలను సరిగ్గా వివరిస్తుందని నిర్ధారించుకోవడం ముఖ్యం.

స్పెసిఫికేషన్లు సరిగా వ్రాయబడకపోతే, లక్షణాల ఉల్లంఘనలు—ఇవి దుర్బలమైన ఎగ్జిక్యూషన్‌లను సూచిస్తాయి—ఫార్మల్ వెరిఫికేషన్ ఆడిట్ ద్వారా గుర్తించబడవు. ఈ సందర్భంలో, ఒక అభివృద్ధి చేసేవాడు కాంట్రాక్ట్ బగ్-రహితమని తప్పుగా భావించవచ్చు.

పనితీరు సమస్యలు

ఫార్మల్ వెరిఫికేషన్ అనేక పనితీరు సమస్యలను ఎదుర్కొంటుంది. ఉదాహరణకు, మోడల్ చెకింగ్ మరియు సింబాలిక్ చెకింగ్ సమయంలో ఎదుర్కొనే స్టేట్ మరియు పాత్ ఎక్స్‌ప్లోజన్ సమస్యలు, వరుసగా, ధృవీకరణ ప్రక్రియలను ప్రభావితం చేయవచ్చు. అలాగే, ఫార్మల్ వెరిఫికేషన్ ఉపకరణాలు తరచుగా వాటి అంతర్లీన లేయర్‌లో SMT సాల్వర్‌లు మరియు ఇతర కన్‌స్ట్రైంట్ సాల్వర్‌లను ఉపయోగిస్తాయి, మరియు ఈ సాల్వర్‌లు గణనపరంగా తీవ్రమైన ప్రక్రియలపై ఆధారపడతాయి.

అలాగే, ప్రోగ్రామ్ వెరిఫైయర్‌లు ఒక లక్షణం (లాజికల్ ఫార్ములాగా వర్ణించబడింది) సంతృప్తిపరచగలదా లేదా కాదా అని నిర్ధారించడం ఎల్లప్పుడూ సాధ్యం కాదు ("నిర్ణయాత్మకత సమస్యopens in a new tab") ఎందుకంటే ఒక ప్రోగ్రామ్ ఎప్పటికీ ముగియకపోవచ్చు. అలాగే, ఒక కాంట్రాక్ట్ బాగా స్పెసిఫై చేయబడినప్పటికీ కొన్ని లక్షణాలను నిరూపించడం అసాధ్యం కావచ్చు.

ఇతీరియము స్మార్ట్ కాంట్రాక్టుల కొరకు ఫార్మల్ వెరిఫికేషన్ ఉపకరణాలు

ఫార్మల్ స్పెసిఫికేషన్లను సృష్టించడం కొరకు స్పెసిఫికేషన్ భాషలు

చట్టం: చట్టం నిల్వ అప్‌డేట్‌లు, ప్రీ/పోస్ట్ షరతులు మరియు కాంట్రాక్ట్ ఇన్‌వేరియంట్‌ల స్పెసిఫికేషన్‌ను అనుమతిస్తుంది. దాని ఉపకరణాల సూట్ Coq, SMT సాల్వర్‌లు లేదా hevm ద్వారా అనేక లక్షణాలను నిరూపించగల ప్రూఫ్ బ్యాకెండ్‌లను కూడా కలిగి ఉంది.

• GitHubopens in a new tab
• డాక్యుమెంటేషన్opens in a new tab

Scribble - Scribble స్పెసిఫికేషన్ భాషలోని సంకేత భాష ఉల్లేఖనాలను స్పెసిఫికేషన్‌ను తనిఖీ చేసే కాంక్రీట్ నిర్ధారణలుగా మారుస్తుంది.

• దస్తావేజులను సమకూర్చుటopens in a new tab

Dafny - Dafny అనేది ఒక వెరిఫికేషన్-సిద్ధ ప్రోగ్రామింగ్ భాష, ఇది సంకేత భాష యొక్క సరియైనత గురించి తర్కించడానికి మరియు నిరూపించడానికి ఉన్నత-స్థాయి ఉల్లేఖనాలపై ఆధారపడుతుంది.

• GitHubopens in a new tab

సరియైనతను తనిఖీ చేయడం కొరకు ప్రోగ్రామ్ వెరిఫైయర్‌లు

Certora Prover - Certora Prover అనేది స్మార్ట్ కాంట్రాక్టులలో సంకేత భాష సరియైనతను తనిఖీ చేయడానికి ఒక ఆటోమేటిక్ ఫార్మల్ వెరిఫికేషన్ ఉపకరణం. స్పెసిఫికేషన్లు CVL (Certora వెరిఫికేషన్ భాష)లో వ్రాయబడతాయి, ప్రాపర్టీ ఉల్లంఘనలు స్టాటిక్ విశ్లేషణ మరియు కన్‌స్ట్రైంట్-సాల్వింగ్ కలయికను ఉపయోగించి గుర్తించబడతాయి.

• వెబ్‌సైట్opens in a new tab
• దస్తావేజులను సమకూర్చుటopens in a new tab

Solidity SMTChecker - Solidity యొక్క SMTChecker SMT (సాటిస్‌ఫైయబిలిటీ మోడ్యులో థియరీలు) మరియు హార్న్ సాల్వింగ్‌పై ఆధారపడిన ఒక అంతర్నిర్మిత మోడల్ చెక్కర్. ఇది సంకలనం సమయంలో ఒక కాంట్రాక్ట్ యొక్క సోర్స్ కోడ్ స్పెసిఫికేషన్‌లతో సరిపోలుతుందో లేదో నిర్ధారిస్తుంది మరియు భద్రతా లక్షణాల ఉల్లంఘనల కొరకు స్టాటిక్‌గా తనిఖీ చేస్తుంది.

• GitHubopens in a new tab

solc-verify - solc-verify అనేది Solidity కంపైలర్ యొక్క విస్తరించిన వెర్షన్, ఇది ఉల్లేఖనాలు మరియు మాడ్యులర్ ప్రోగ్రామ్ వెరిఫికేషన్ ఉపయోగించి Solidity సంకేత భాషపై ఆటోమేటెడ్ ఫార్మల్ వెరిఫికేషన్‌ను నిర్వహించగలదు.

• GitHubopens in a new tab

KEVM - KEVM అనేది K ఫ్రేమ్‌వర్క్‌లో వ్రాయబడిన ఇతీరియము వర్చువల్ మషీన్ (EVM) యొక్క ఫార్మల్ సెమాంటిక్స్. KEVM ఎగ్జిక్యూటబుల్ మరియు రీచబిలిటీ లాజిక్ ఉపయోగించి నిర్దిష్ట ప్రాపర్టీ-సంబంధిత నిర్ధారణలను నిరూపించగలదు.

• GitHubopens in a new tab
• దస్తావేజులను సమకూర్చుటopens in a new tab

థీరమ్ ప్రూవింగ్ కొరకు లాజికల్ ఫ్రేమ్‌వర్క్‌లు

Isabelle - Isabelle/HOL అనేది ఒక ప్రూఫ్ అసిస్టెంట్, ఇది గణిత ఫార్ములాలను ఒక ఫార్మల్ భాషలో వ్యక్తీకరించడానికి అనుమతిస్తుంది మరియు ఆ ఫార్ములాలను నిరూపించడానికి ఉపకరణాలను అందిస్తుంది. ప్రధాన అప్లికేషన్ గణిత రుజువుల ఫార్మలైజేషన్ మరియు ముఖ్యంగా ఫార్మల్ వెరిఫికేషన్, ఇందులో కంప్యూటర్ హార్డ్‌వేర్ లేదా సాఫ్ట్‌వేర్ యొక్క సరియైనతను నిరూపించడం మరియు కంప్యూటర్ భాషలు మరియు ప్రోటోకాల్‌ల లక్షణాలను నిరూపించడం ఉంటుంది.

• GitHubopens in a new tab
• దస్తావేజులను సమకూర్చుటopens in a new tab

Rocq - Rocq అనేది ఒక ఇంటరాక్టివ్ థీరమ్ ప్రూవర్, ఇది మీకు థీరమ్‌లను ఉపయోగించి ప్రోగ్రామ్‌లను నిర్వచించడానికి మరియు సరియైనత యొక్క మెషిన్-చెక్డ్ ప్రూఫ్‌లను ఇంటరాక్టివ్‌గా ఉత్పత్తి చేయడానికి అనుమతిస్తుంది.

• GitHubopens in a new tab
• దస్తావేజులను సమకూర్చుటopens in a new tab

స్మార్ట్ కాంట్రాక్టులలో దుర్బలమైన ప్యాట్రన్‌లను గుర్తించడం కొరకు సింబాలిక్ ఎగ్జిక్యూషన్-ఆధారిత ఉపకరణాలు

Manticore - సింబాలిక్ ఎగ్జిక్యూషన్‌పై ఆధారపడిన EVM బైట్‌కోడ్ విశ్లేషణ ఉపకరణం.

• GitHubopens in a new tab
• దస్తావేజులను సమకూర్చుటopens in a new tab

hevm - hevm అనేది EVM బైట్‌కోడ్ కొరకు ఒక సింబాలిక్ ఎగ్జిక్యూషన్ ఇంజిన్ మరియు ఈక్వివలెన్స్ చెక్కర్.

• GitHubopens in a new tab

Mythril - ఇతీరియము స్మార్ట్ కాంట్రాక్టులలో దుర్బలత్వాలను గుర్తించడానికి ఒక సింబాలిక్ ఎగ్జిక్యూషన్ ఉపకరణం

• GitHubopens in a new tab
• డాక్యుమెంటేషన్opens in a new tab

మరింత సమాచారం

• స్మార్ట్ కాంట్రాక్టుల ఫార్మల్ వెరిఫికేషన్ ఎలా పనిచేస్తుందిopens in a new tab
• ఫార్మల్ వెరిఫికేషన్ దోషరహిత స్మార్ట్ కాంట్రాక్టులను ఎలా నిర్ధారించగలదుopens in a new tab
• ఇతీరియము పర్యావరణ వ్యవస్థలో ఫార్మల్ వెరిఫికేషన్ ప్రాజెక్టుల యొక్క ఒక అవలోకనంopens in a new tab
• ఇతీరియము 2.0 డిపాజిట్ స్మార్ట్ కాంట్రాక్ట్ యొక్క ఎండ్-టు-ఎండ్ ఫార్మల్ వెరిఫికేషన్opens in a new tab
• ప్రపంచంలో అత్యంత ప్రజాదరణ పొందిన స్మార్ట్ కాంట్రాక్ట్‌ను అధికారికంగా ధృవీకరించడంopens in a new tab
• SMTChecker మరియు ఫార్మల్ వెరిఫికేషన్opens in a new tab