傭兵在上週六撰寫了曌鏈MIT的相關文章，主要介紹的是MIT富有創新亮點的共識演算法，歡迎大家前往閱讀：、
今天想跟大家看看的是MIT使用的另外一個亮點：新的非圖靈完備的 合約語義處理語言(CLP)
智慧合約發展現狀
智慧合約是在以太坊被提出來的，發展至今天已經成為了區塊鏈世界的一個必備的技術。從BTC/" target="_blank"">BTC到ETH的轉變上，正是出現了智慧合約的概念，導致了區塊鏈能理所當然地成為了作業系統概念。正是智慧合約的出現，區塊鏈公鏈才能自己定義需要的交換的資料、何時交換。
在ETH上，智慧合約被譽為圖靈完備的。學過計算機的人都知道，圖靈完備的意思就是說讓計算機有了類似人類的智慧，使得人類難以分別是機器人還是人類。在以太坊上，為什麼稱智慧合約是圖靈完備的呢？因為從使用者的角度而言，這個“合約”是程式語言撰寫的，計算機執行的，它實際上是一個無需人來操作、自動擔保的狀態機，只要當滿足的條件達到了，那麼這個合約就會釋放對應的代幣。如果以幣乎為例，幣乎背後的KEY分發機制就是撰寫在以太坊上的智慧合約。正是這個智慧合約，它表示了無需徵得幣乎官方同意，在KEY釋放上規定了一天釋放量是1200餘萬個key，你的點贊量達到多少，7天后就根據這個點贊量給你釋放對應的KEY。這個過程都是無需幣乎官方來執行的，只需要一個以太坊上的智慧合約就可以完成的。
因此在以太坊上，程式碼即法律的概念被提出。它正是因為無需人類來保證，完全交由機器規則來寫，一旦寫入，那就無人可以修改。透明與公正正是機器能完成的事情。
智慧合約的擔憂
正是智慧合約越來越重要，在區塊鏈世界裡，我們相當於將金融的分發權力都交給了機器，那麼智慧合約的安全越來越重要。但是目前而言，只要是程式碼，在剛剛出現的時候總是難以避免有安全漏洞。同樣的是，在區塊鏈早期，無人能保證智慧合約的軟體沒有安全性問題。
據白皮書透露，在軟體開發行業，平均每1000行程式碼含有一個安全問題。而支援圖靈完備的以太坊智慧合約也是具備類似的問題。其安全性和可靠性成了很大的問題。這在早期，ETH發展過程中，駭客就曾經利用ETh的程式碼漏洞，導致了ETH智慧分叉應對。
因此，目前程式碼容易產生漏洞，缺乏安全保障。
MIT的應對
MIT 區塊鏈將人工智慧中多種技術應用於智慧合約的設計，並給出解決當前 智慧合約各種缺陷的對策，主要包括:
• 基於規則知識庫的語法檢查 將合約文字檔案，透過內建編譯工具，將對合約構建一棵基於 BNF 正規化基 礎上的抽象語法樹(AST)，透過該語法抽象樹，便可以對合約內容展開語法 識別，進行簡單的合約安全識別。目前建議按照遞迴下降分析的方法，對語 法抽象樹進行基於知識規則庫的檢查，從而確定是否存在安全隱患。
• 基於語義分析 NLP 的交易模型識別與安全檢查
基於語法的安全檢查規則僅能靜態識別合約缺陷，而基於語義分析的交易模 型識別與安全檢查，則主要透過上下文相關審查，確定智慧合約中不滿足規 則或者不安全的操作。目前支援的安全檢查包括:型別檢查，控制流檢查和 一致性檢查。 透過上述靜態語義分析，能夠基本排除由於人為書寫智慧合約帶來的各種表 層的邏輯缺陷，但尚不能解決動態執行過程中出現的各種邏輯問題。
• AI 輔助的形式驗證以及動態約束
在合約驗證上，採用基於 AI 輔助的形式驗證以及動態約束檢查的方法，解決 上述安全問題。其核心思想包括:利用模式匹配獲得使用者真實需求約束、對 靜態語義分析形成的抽象樹，按照貝葉斯分類器進行模型分類，確定樹中的 各段分支屬於對應的類屬，根據模式匹配結果和人工智慧分類結果，獲得當 前合約的全部靜態與動態約束，基於該約束即可生成合約程式碼的斷言，並基 於該結果進行形式驗證和動態驗證。
• 基於 AI 形式驗證的智慧合約安全性檢查
MIT 區塊鏈使用形式驗證技術對智慧合約的安全性進行自動化檢查。其中， 形式驗證模型使用 F*函式程式語言(Functional Programming Language) 建立，該語言整合了 Z3 求解工具，輸入格式是 SMT-LIB2.0 標準，擁有豐 富的型別和條件檢查功能。 使用人工智慧方法自動識別程式語義並發現其中的典型模式，從而根據模式 自行產生為了滿足安全要求而需要的屬性。當使用者提供智慧合約以及翻譯後 的執行程式碼後，MIT 的 AI 引擎將自動完成程式碼的區域性相似性匹配和全域性相 似性匹配，從而推測程式碼的行為模型。根據 AI 獲得行為模型，生成對應的形 式驗證約束，從而進行深層次的行為驗證，實現程式碼安全性。
