作爲比特币的一項關鍵底層技術，近些年區塊鏈成(chéng)爲了非常火爆的概念和趨勢，而且構成(chéng)了目前金融科技領域最核心的技術之一。通過(guò)區塊鏈，人們可以不需要借助第三方的信任背書，就能(néng)進(jìn)行點到點的交易、支付等金融活動，實現了在金融行業的廣泛應用。但要警惕的是，區塊鏈中一行小的代碼錯誤就可能(néng)會(huì)導緻金融行業的巨大損失，金融領域巨大的經(jīng)濟利益也會(huì)吸引大量的黑客攻擊，因此，如何保證區塊鏈的安全性問題也變得越來越重要。

《區塊鏈安全性形式化驗證研究》正是在此背景下所進(jìn)行的課題，該課題也是北大-睿智Fintech聯合實驗室第一期結題項目之一。近日，項目負責人、北京大學(xué)數學(xué)科學(xué)學(xué)院信息與計算科學(xué)系教授孫猛進(jìn)行了結題彙報。來自北京大學(xué)、睿智科技的各位專家委員會(huì)成(chéng)員參加了評審會(huì)議。

項目負責人、北京大學(xué)數學(xué)科學(xué)學(xué)院信息與計算科學(xué)系教授孫猛

孫猛介紹，以太坊平台有很多深的漏洞，如短地址攻擊、拒絕服務攻擊等，實際上很多漏洞通過(guò)形式化方法都(dōu)能(néng)找出來。“而要保證智能(néng)合約的正确性、安全性，就要求我們确保這(zhè)些漏洞完全被(bèi)檢測。形式化驗證（Formal Verification)提供了很好(hǎo)的解決方案。”

圖片來源：項目負責人、北京大學(xué)數學(xué)科學(xué)學(xué)院

信息與計算科學(xué)系教授孫猛提供

形式化方法是基于嚴格數學(xué)基礎，對(duì)計算機系統進(jìn)行形式規約、開(kāi)發(fā)和驗證的技術。形式驗證是證明不同形式規約之間的邏輯關系，這(zhè)些邏輯關系反映了在開(kāi)發(fā)不同階段産品之間的需要滿足的各類正确性需求。

圖片來源：項目負責人、北京大學(xué)數學(xué)科學(xué)學(xué)院

信息與計算科學(xué)系教授孫猛提供

“我們這(zhè)個項目最初的計劃是完成(chéng)三項研究，一是使用WhyML作爲中間語言，給出以太坊虛拟機EVM的形式化定義，并實現到OCaml語言上的轉換，從而可對(duì)以太坊上的智能(néng)合約安全性進(jìn)行形式化驗證；二是選取1〜2種(zhǒng)比較典型的區塊鏈架構，使用定理證明和模型檢查技術對(duì)區塊鏈上的協議進(jìn)行形式化描述和驗證。”孫猛表示，希望初步形成(chéng)區塊鏈形式化建模和驗證的方法論，爲後(hòu)續進(jìn)一步研究打下基礎。

“目前看，原計劃各部分工作均已順利完成(chéng)，共發(fā)表及錄用國(guó)際會(huì)議論文4篇，并開(kāi)發(fā)了智能(néng)合約驗證的原型工具，初步形成(chéng)了相關的方法框架。”孫猛表示。

學(xué)術委員會(huì)的睿智科技成(chéng)員代表：聯席總裁兼CFO黃建、CTO蘇明富、模型研發(fā)總監劉洋博士分别就“隐私計算”“聯邦學(xué)習”“數據分層與處理”等問題與孫猛進(jìn)行了交流。

最後(hòu)，《區塊鏈安全性形式化驗證研究》項目通過(guò)學(xué)術委員會(huì)的投票，順利完成(chéng)結題。

左起(qǐ)：睿智科技CTO蘇明富

項目負責人、北京大學(xué)數學(xué)科學(xué)學(xué)院信息與計算科學(xué)系教授孫猛

睿智科技聯席總裁兼CFO黃建

睿智科技模型研發(fā)總監劉洋博士

2019年9月，大數據分析與應用技術國(guó)家工程實驗室與睿智科技聯合發(fā)起(qǐ)的北大-睿智科技Fintech聯合實驗室在北京大學(xué)靜園六院正式成(chéng)立。該聯合實驗室將(jiāng)探索産學(xué)研結合的新模式，推動大數據和人工智能(néng)等前沿技術在金融科技行業中的應用和發(fā)展，助力傳統金融行業的數字化轉型。

聯合實驗室的課題研發(fā)面(miàn)向(xiàng)北大師生開(kāi)放申請。同時，北大師生如有金融科技領域的前沿課題，也可以向(xiàng)聯合實驗室提交單獨的申請報告，待學(xué)術委員會(huì)審核通過(guò)後(hòu)將(jiāng)予以實施并提供經(jīng)費支持。