來源：每日經(jīng)濟新聞

8月27日晚,由北京大學(xué)大數據分析與應用技術國(guó)家工程實驗室和睿智合創(北京)科技有限公司(簡稱“睿智科技”)聯合舉辦的金融科技公益公開(kāi)課第三期線上開(kāi)課。北京大學(xué)數學(xué)科學(xué)學(xué)院信息與計算科學(xué)系教授、博士生導師孫猛爲大家帶來的《區塊鏈形式化驗證》課程,受到了廣大網友的熱烈歡迎。

該系列公開(kāi)課于5月7日面(miàn)向(xiàng)全網免費開(kāi)課,首期課程爲睿智科技首席戰略官、摩根大通銀行原董事(shì)總經(jīng)理、美國(guó)運通公司原首席信貸官林晴帶來的《美國(guó)金融危機背景下的中國(guó)啓示錄》;第二期課程爲北京大學(xué)數字金融研究中心副主任,北京大學(xué)國(guó)家發(fā)展研究院副教授、博士生導師,斯坦福大學(xué)經(jīng)濟學(xué)博士黃卓帶來的《金融科技時代的中國(guó)财富管理》。

區塊鏈技術爲人類建立信任基礎

“很多人以爲比特币與區塊鏈兩(liǎng)者是一個東西,實際上比特币隻是第一個成(chéng)功的區塊鏈應用。你可以把區塊鏈理解成(chéng)智能(néng)手機,那麼(me)比特币隻是手機上一個做的非常好(hǎo)的App。”孫猛表示,區塊鏈是一種(zhǒng)分布式賬本技術,通過(guò)共識機制發(fā)動節點共同記賬,爲了防止共識信息被(bèi)篡改,通常采用鏈式數據結構,使用密碼學(xué)技術進(jìn)行數據存儲。

衆所周知,信用是所有金融活動的根基。傳統金融行業裡(lǐ)的所有機構(包括金融機構、金融科技公司、監管機構、中介機構等)的所有金融活動都(dōu)是爲了解決信任問題。在孫猛看來,區塊鏈最大的創新是第一次用技術解決了人類的共識問題,把密碼學(xué)、分布式系統、博弈論、P2P協議等諸多技術有機組合到一塊,通過(guò)理性的技術爲人類建立信任提供了方法,爲我們提供了一個很好(hǎo)的解決信任問題的途徑,也構成(chéng)了目前金融科技領域最核心的技術之一。

“通過(guò)區塊鏈,人們可以不需要借助第三方的信任背書,就能(néng)進(jìn)行點到點的交易、支付等金融活動,區塊鏈在金融行業已經(jīng)得到了非常廣泛的應用。”孫猛表示,另一方面(miàn),一行小的代碼錯誤或可能(néng)導緻巨大損失,同時金融領域巨大的經(jīng)濟利益也吸引著(zhe)大量黑客攻擊。“如何保證區塊鏈的安全性問題也變得越來越重要。”

(圖片來源:孫猛教授演講PPT)

“區塊鏈技術目前也面(miàn)臨著(zhe)一些挑戰,主要包括可擴展性、安全性、隐私保護和監管等問題。”孫猛認爲,“形式化驗證技術對(duì)于保障複雜的區塊鏈系統的安全性、可信性至關重要。爲了應對(duì)這(zhè)方面(miàn)的挑戰,我們已經(jīng)做了一些工作,當然距離真正應用還(hái)有一定的距離。”

區塊鏈+形式化驗證如何實現 1+1>2

當在區塊鏈系統中應用形式化驗證技術,會(huì)發(fā)生什麼(me)事(shì)情?

“我們前兩(liǎng)天剛剛過(guò)了七夕節,有一句非常應景的詩來形容這(zhè)個情況,就是‘金風玉露一相逢,便勝卻人間無數’。當區塊鏈和形式化技術兩(liǎng)者碰到一塊,這(zhè)個1+1得到的結果絕對(duì)是遠遠大于2的。”孫猛對(duì)此很有信心。

孫猛介紹道(dào),目前市場上做區塊鏈形式化驗證的項目相對(duì)較少,已知的項目有UIUC的Grigore Rosu教授團隊提供智能(néng)合約形式化驗證的平台——Runtime Verification;耶魯大學(xué)的邵中教授和哥倫比亞大學(xué)顧榮輝教授創立的Certik驗證框架;成(chéng)都(dōu)鏈安科技的Verification as a Service(VaaS)是一個同時支持EOS和以太坊區塊鏈的形式化驗證平台。

“這(zhè)些大部分還(hái)處于早期階段,在區塊鏈驗證裡(lǐ)頭還(hái)有很多可以做的工作。”孫猛表示,他的團隊目前在做的工作,主要的想法是把形式化驗證和測試結合起(qǐ)來,用在安全的以太坊虛拟機實現的開(kāi)發(fā)上,并且可以在字節碼的層次上對(duì)智能(néng)合約進(jìn)行驗證。

“我們的定義包括類型、指令和解釋器定義。”孫猛介紹道(dào),“然後(hòu)可以對(duì)經(jīng)過(guò)驗證的EVM進(jìn)行部署。我們定義一系列的driver來從WhyML程序中抽取Ocaml程序,抽取之後(hòu),EVM的OCaml實現被(bèi)封裝成(chéng)一個靜态庫,可以被(bèi)Rust中的虛拟機調用。在我們的框架裡(lǐ),Rust和Why3可以進(jìn)行交互,經(jīng)過(guò)驗證的模型可以直接在production environment中執行,并且可以被(bèi)進(jìn)一步測試。”

孫猛團隊還(hái)在做一些區塊鏈形式化驗證的工作,包括對(duì)塊同步協議、共識協議的形式化建模、以及對(duì)相關的性質在模型檢查工具UPPAAL裡(lǐ)面(miàn)做的形式化驗證等。

在課程的後(hòu)一階段,孫猛就網友關心的幾個問題進(jìn)行了回複。這(zhè)些問題有:爲什麼(me)形式化驗證對(duì)金融領域特别重要?現在在區塊鏈驗證方面(miàn)也已經(jīng)有一些相關的工具和平台,你們的工作和他們相比有什麼(me)優點或者不同之處?現在的人工智能(néng)、大數據、深度學(xué)習等技術對(duì)區塊鏈的安全性保障方面(miàn)有沒(méi)有什麼(me)幫助?

如果你對(duì)區塊鏈相關内容感興趣,歡迎關注公衆号【睿智科技Wiseco】,點擊【課程回放】觀看課程。

關于主講嘉賓

孫猛,北京大學(xué)數學(xué)科學(xué)學(xué)院信息與計算科學(xué)系教授,博士生導師,曾任聯合國(guó)大學(xué)國(guó)際軟件技術研究所客座研究員,荷蘭數學(xué)與計算機科學(xué)研究中心研究員,主要研究領域爲軟件理論和形式化方法。

近年來的工作主要包括:協調模型和語言,餘代數理論及其應用,形式化建模,軟件驗證與測試,信息物理融合系統,面(miàn)向(xiàng)服務與雲計算,區塊鏈智能(néng)合約的建模與驗證,大數據分析,機器學(xué)習與深度學(xué)習的理論基礎及相關技術在形式化驗證中的應用。

主持及作爲主要成(chéng)員參加國(guó)家及省部級項目十餘項,在IEEE Transactions on Software Engineering、Theoretical Computer Science、Science of Computer Programming、ICSE、ESEC/FSE、FM等國(guó)際期刊及會(huì)議發(fā)表論文90餘篇,獲TASE 2015等多個國(guó)際會(huì)議最佳論文獎,擔任ICFEM 2018等多個國(guó)際會(huì)議程序委員會(huì)主席,FM 2019、TACAS 2019等60餘個國(guó)際會(huì)議程序委員會(huì)委員。

關于主辦方:

北京大學(xué)大數據分析與應用技術國(guó)家工程實驗室由國(guó)家發(fā)展和改革委員會(huì)批複組建,整合了數學(xué)科學(xué)學(xué)院、信息科學(xué)學(xué)院和前沿交叉學(xué)院大數據科學(xué)中心的優勢研究力量和學(xué)科資源,是承擔原創大數據理論和技術的應用開(kāi)發(fā)和成(chéng)果轉化的創新平台,緻力于面(miàn)向(xiàng)企業一線技術需求的數學(xué)基礎研究與工程應用交叉融合發(fā)展以及大數據和人工智能(néng)學(xué)科的人才培養。

睿智合創(北京)科技有限公司(簡稱睿智科技)是一家以“打破金融信息非對(duì)稱”爲使命,爲廣大金融機構提供大數據洞察力系列産品、一站式科技賦能(néng)、智能(néng)導流三大核心業務的智能(néng)金融科技企業。睿智科技依托大數據洞察力和人工智能(néng)技術,緻力于成(chéng)爲連接億萬消費者的金融需求與千百家金融機構信貸供給的智能(néng)金融樞紐,爲促進(jìn)中國(guó)金融繁榮與普惠做出貢獻。