隨著以太坊區(qū)塊鏈的發(fā)展,智能合約作為以太坊的核心技術(shù)也得到越來越多的應(yīng)用,其中應(yīng)用之一是用戶通過代幣智能合約進(jìn)行新代幣的開發(fā)。除以太幣外,在以太坊主流代幣標(biāo)準(zhǔn)協(xié)議ERC20的基礎(chǔ)上,以太坊支持用戶通過代幣智能合約完成代幣的構(gòu)建發(fā)行、管理和交易。代幣智能合約種類多,持有大量資金,易受到攻擊者的攻擊。目前代幣智能合約已曝出存在多種類型的漏洞,也發(fā)生被攻擊的安全事件,造成大量損失,因此保證合約的安全性并對(duì)合約進(jìn)行安全審計(jì)是非常必要的。形式化驗(yàn)證方法是專門針對(duì)協(xié)議或系統(tǒng)的安全性所提出的一種檢驗(yàn)分析方法,能夠更全面、深入地研究合約的安全性。針對(duì)代幣智能合約的安全問題,本文以代幣智能合約的形式化建模與驗(yàn)證為研究重點(diǎn),結(jié)合以太坊目前主流的ERC20代幣標(biāo)準(zhǔn)協(xié)議,提出了面向ERC20標(biāo)準(zhǔn)的代幣智能合約形式化模型,并將形式化模型應(yīng)用到對(duì)代幣智能合約造成威脅的高危漏洞的形式化分析中。具體研究內(nèi)容如下:1.針對(duì)代幣智能合約形式化建模的需求,提出了面向ERC20標(biāo)準(zhǔn)的代幣智能合約形式化模型框架。描述了模型定義的具體函數(shù)行為和攻擊者模型,對(duì)合約中函數(shù)行為進(jìn)行抽象,利用多集合重寫規(guī)則定義代幣智能合約的建模規(guī)則。針... 

【文章來源】：中國科學(xué)技術(shù)大學(xué)安徽省 211工程院校 985工程院校

【文章頁數(shù)】：84 頁

【學(xué)位級(jí)別】：碩士

【部分圖文】：

圖２．１以太坊整體架構(gòu)??以太坊平臺(tái)中的應(yīng)用基于以太坊智能合約開展，智能合約像是一個(gè)以太坊??

?第２章相關(guān)技術(shù)???號(hào)，用戶無法自定義其他的符號(hào)，這些符號(hào)可以表示積分、財(cái)產(chǎn)等。因此在以太??坊中，除了原生貨幣以太幣之外，用戶可開發(fā)新的代幣以滿足其不同的需求。??２．１．１以太坊區(qū)塊??以太坊中的數(shù)據(jù)會(huì)被通過文件的形式永久存儲(chǔ)記錄，這些文件被稱為以太??坊區(qū)塊［３Ｇ］。區(qū)塊可看作一種數(shù)據(jù)結(jié)構(gòu)，區(qū)塊上記錄了在一段時(shí)間內(nèi)產(chǎn)生的交易??和狀態(tài)更變的結(jié)果。各種操作執(zhí)行交易產(chǎn)生的各種信息存放在區(qū)塊中，并通過指??針和前一個(gè)區(qū)塊相連。以太坊區(qū)塊主要由區(qū)塊頭和區(qū)塊體構(gòu)成，區(qū)塊結(jié)構(gòu)如下??圖２．２所示。此外，我們用兩個(gè)值來識(shí)別區(qū)塊：區(qū)塊頭哈希值和區(qū)塊高度。??區(qū)塊頭??版本號(hào)?時(shí)間敝?Ｍｅｒｋｌｅ根隨機(jī)數(shù)??區(qū)塊體???交易數(shù)Ｍ???交易?交易?｜交易?交易?交易?交易??圖２．２區(qū)塊結(jié)構(gòu)示意圖??區(qū)塊頭是區(qū)塊的核心組成部分，區(qū)塊頭包括上一區(qū)塊的哈希值、時(shí)間戳、??Ｍｅｒｋｌｅ根等相關(guān)信息，區(qū)塊頭詳細(xì)結(jié)構(gòu)和含義如表２．１所示。區(qū)塊體中包含本區(qū)??塊中所有和交易相關(guān)的信息，以太坊中交易是整體架構(gòu)中的重要組成部分，交易??將以太坊中的賬戶連接起來，可實(shí)現(xiàn)資產(chǎn)價(jià)值的傳遞和轉(zhuǎn)移。區(qū)塊體詳細(xì)結(jié)構(gòu)和??含義如表２．２所示。??表２．１區(qū)塊頭詳細(xì)結(jié)構(gòu)??字段名?描述含義??版本?版本號(hào)，用于跟蹤更新???區(qū)塊哈希值－?引用鏈中前一區(qū)塊的哈希值??時(shí)間戳?＾?該區(qū)塊產(chǎn)生的近似時(shí)間??Ｍｅｒｋｌｅ根?該區(qū)塊中有關(guān)交易的Ｍｅｒｋｌｅ根的哈希值??￣￣隨機(jī)數(shù)?用于工作量證明的計(jì)數(shù)器??以太坊中的交易主要是指將交易從一個(gè)賬戶發(fā)送到另一個(gè)賬戶，交易主要??１０??

?包含發(fā)送者的簽名、接收者簽名、發(fā)送的金額數(shù)量等內(nèi)容。交易中定義了交易費(fèi)??用這樣一個(gè)概念，交易費(fèi)用由ｇａｓ表示，主要是為了防止用戶在鏈中發(fā)送太多無??意義的交易，因此每一筆交易需要付出一定的代價(jià)。用戶發(fā)送一筆交易時(shí)需要支??付一定的ｇａｓ費(fèi)用用于這筆交易的執(zhí)行，當(dāng)執(zhí)行一筆交易需要復(fù)雜繁瑣的計(jì)算步??驟時(shí)，這筆交易消耗的ｇａｓ越多。交易執(zhí)行完成后，支付的ｇａｓ若沒有被消耗完，??則會(huì)返還給發(fā)起這筆交易的賬戶中。??２．１．２以太坊賬戶??以太坊中有兩種賬戶：外部賬戶和合約賬戶。如圖２．３所示，外部賬戶是由密??鑰控制的賬戶，有賬戶余額，無代碼，能觸發(fā)交易，包括轉(zhuǎn)賬或執(zhí)行合約。合約賬??戶是由代碼控制的，有賬戶余額，有代碼，能被觸發(fā)執(zhí)行智能合約代碼，在合約??創(chuàng)建后自動(dòng)運(yùn)行。以太坊的賬戶信息本質(zhì)上是由ｎｏｎｃｅ、ｂａｌａｎｃｅ、ｃｏｄｅＨａｓｈ、??ｓｔｏｒａｇｅＲｏｏｔ組成的一個(gè)數(shù)據(jù)結(jié)構(gòu)。??合約賬戶??外部賬戶????Ｉ丨代碼Ｉ???；?［??????ｎｏｎｃｅ?ｂａｌａｎｃｅ?ｎｏｎｃｅ?ｂａｌａｎｃｅ??ｓｔｏｒａｇｅ?ｃｏｄｅＨａ?ｓｔｏｒａｇｅ?ｃｏｄｅｌｌａ??Ｒｏｏｔ?ｓｈ?Ｒ〇〇ｔ?｜?ｓｈ??圖２．３以太坊賬戶示意圖??（１）?ｎｏｎｃｅ：當(dāng)前賬戶發(fā)出的消息計(jì)數(shù)器，指賬戶發(fā)出過多少次交易。??１１??


本文編號(hào)：2949265