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

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

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

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

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

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

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

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

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