以太坊開發(fā)者大會(huì)DEVCON2第二天繼續(xù)迎來了多次技術(shù)高潮，現(xiàn)場更像是粉絲見面會(huì)。會(huì)上，來自英國的區(qū)塊鏈金融算法初創(chuàng)公司Imandra推出了其針對(duì)以太坊運(yùn)行的智能合約形式化驗(yàn)證平臺(tái)，在系統(tǒng)和算法越來越復(fù)雜之際，通過它可利用互動(dòng)驗(yàn)證等工具進(jìn)行金融交易驗(yàn)證。

Imandra創(chuàng)始人Dr.Grant Passmore介紹：“之所以研究形式化驗(yàn)證，主要是因?yàn)槟壳靶袠I(yè)內(nèi)發(fā)生了一些事情表明，我們還需要在根本上建立穩(wěn)健的風(fēng)險(xiǎn)控制工具，比如說投行，他們可能有很大的風(fēng)險(xiǎn)漏洞，他們投資了以太仿，以防止未來其數(shù)十萬個(gè)投資組合暴露在風(fēng)險(xiǎn)當(dāng)中?！?/span>

Imandra是金融算法公司Aesthetic Integration旗下的項(xiàng)目，在去年的Devcon1之后，Imandra取得了多個(gè)不錯(cuò)的成績：在620家區(qū)塊鏈公司的競爭中，獲得了瑞銀集團(tuán)（UBS）“未來金融全球挑戰(zhàn)”的第一名；今年8月獲得谷歌支撐的種子基金融資。Imandra主要基于區(qū)塊鏈研發(fā)針對(duì)金融交易的算法，比如黑池和其他用于不同交易體系之間的驗(yàn)證的算法，能夠自動(dòng)檢測(cè)交易的風(fēng)險(xiǎn)。

該公司聯(lián)合創(chuàng)始人Denis Ignatovich是一名博士后，曾是銀行風(fēng)險(xiǎn)交易負(fù)責(zé)人，也負(fù)責(zé)該公司算法的安全性。他表示，交易場景中參數(shù)文件和交易規(guī)則可以被轉(zhuǎn)化成數(shù)學(xué)上的精確參數(shù)，以代碼的形式表示，并可進(jìn)行自動(dòng)推導(dǎo)的分析。在投資銀行中，成百上千的場景交易也可以被快速核對(duì)每一平臺(tái)的操作，投資者也可以看見他們?cè)诓煌瑘鼍暗慕灰资侨绾伪憩F(xiàn)的。

為什么要運(yùn)用形式化驗(yàn)證呢？Grant Passmore博士向雷鋒網(wǎng)表示，“形式化驗(yàn)證使用自動(dòng)的數(shù)學(xué)模擬技術(shù)來保證系統(tǒng)的參數(shù)一致性，然后利用同樣的技術(shù)來檢測(cè)實(shí)際生產(chǎn)系統(tǒng)是否一致。這樣的技術(shù)已經(jīng)被應(yīng)用于安全性需求極高的行業(yè)，比如金融和航空?！?/span>

智能合約用以太仿的字節(jié)碼來表示，Imandra可以證明智能合約的性能規(guī)范。Passmore介紹說，Imandra智能合約有兩個(gè)層面的算法分析——第一是高級(jí)策略層，用來確保高層合約規(guī)范和設(shè)計(jì)的一致性。在合約運(yùn)行之前，它會(huì)被轉(zhuǎn)換成低層級(jí)的字節(jié)碼?！暗诙蛹?jí)的分析屬于字節(jié)碼層，用來分析區(qū)塊鏈中實(shí)際被執(zhí)行的字節(jié)碼。”

“Imandra技術(shù)方面的最新突破在于，加入了約束變成語言SMT，把技術(shù)和數(shù)學(xué)的理論結(jié)合在一起，此外還包括線性和非線性程序等等，以及基于模型自動(dòng)化的推導(dǎo)，因?yàn)橛袝r(shí)候邏輯可能表示為遞歸，所以我們就必須要采用寫推導(dǎo)的不變式等等來表示。這對(duì)于形式化驗(yàn)證都是非常重要的。”

Passmore表示，在DAO慘敗之前，區(qū)塊鏈社區(qū)一直以創(chuàng)建網(wǎng)頁app的心態(tài)來創(chuàng)建智能合約，所以我們見到了DAO那樣的災(zāi)難性損失。這一事件給我們的啟示是，創(chuàng)建智能合約時(shí)應(yīng)該抱著嚴(yán)格的軟件工程意識(shí)，以建立關(guān)鍵性安全控制算法的心態(tài)來設(shè)計(jì)。

雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。