区块链女侠杨霞：为区块链代码提供军事级的安全检测丨蚂蚁区块链大赛成都站火热报名...
轉自巴比特
原文作者：邱祥宇
智能合約允許在沒有第三方的情況下進行可信交易，這些交易可追蹤且不可逆轉。那么智能合約程序存在哪些安全問題？出了安全問題，怎么辦？如何用形式化驗證的方法給智能合約程序提供（軍事級）的安全驗證，提高智能合約代碼的安全性？
5月30日晚間，螞蟻區塊鏈創新大賽安全合作伙伴、有著區塊鏈安全領域“女俠”稱號的成都鏈安科技創始人兼CEO楊霞，在大賽直播群中就以上問題分享了解決方案，同時也分享了如何與螞蟻區塊鏈BaaS平臺共建安全生態。
數據顯示，2011年至2018年發生的安全事件造成的資金損失高達42億美元，其中由于智能合約安全事件造成的損失占據1/3，由此可以看出智能合約安全問題的嚴重性。而隨著區塊鏈落地應用的大量爆發，潛在的安全問題更是不容忽視。
以以太坊為例，智能合約安全漏洞就有數十大類，30多小類。
智能合約的初衷是建立人與人之間的信任基礎，如果自身的安全性和功能的正確性得不到保障，這個程序就很難值得信任。如何有效解決智能合約的安全問題，是行業值得深入探討的。
作為一家專門從事區塊鏈安全的公司，成都鏈安科技采用形式化驗證的方法對智能合約安全進行一鍵式安全檢測。
形式化驗證，是根據某個或某些形式規范或屬性，使用數學的方法證明其正確或非正確。它是一個系統化的過程，將使用數學推理來驗證設計意圖（用戶功能需求）在實現（智能合約）中是否得以正確貫徹。
此前，形式化驗證通常被用于對航空、航天、軍事控制系統的關鍵程序的功能正確性和安全性驗證，以確保系統可以通過極其苛刻的安全級別認證。由于區塊鏈系統涉及大量的資金交易，采用形式化驗證技術為區塊鏈系統的代碼提供“軍事級”的安全檢測就顯得至關重要了。
在對代碼安全性檢測方面，與形式化驗證對立的是“測試”。
測試的弊端是沒辦法窮舉，只能顯示已經存在的bug，但永遠不能證明bug一定不存在。形式化驗證是通過數學推理的證明方法，能夠保證一定不存在指定屬性的安全問題，并且能夠證明程序是否正確地滿足功能需求和設計目標。
形式化驗證通常分三個步驟：
第一步，對系統功能需求和設計建立形式化的規范； 第二步，對代碼實現進行形式化的建模，包括對系統的狀態進行形式化的描述，還有每個函數的功能要進行描述，并且給出每一個功能所需要滿足的前后的條件； 第三步，通過定理輔助證明器，證明代碼實現是否正確滿足形式化規范，以此證明功能是否符合預期。
但實際上，這里邊有大量的人工參與，效率是非常低的，同時成本也是非常高的。
據楊霞透露，此前她在給軍事領域做形式化驗證的時候是按照代碼行數收費的，在給區塊鏈系統做形式化驗證的時候，剛開始用的是人工手段，驗證一個600-700行的智能合約就花了一周左右的時間。
顯然，這樣做根本無法實現工程化的需要。為此，成都鏈安科技經過近兩年的潛心研發，推出了自動形式化驗證平臺VaaS，能夠把代碼自動進行建模，自動推理證明。
VaaS在驗證智能合約的時候，分兩部分，一部分是安全屬性驗證，一部分是功能正確性驗證。
對安全屬性驗證，首先把智能合約代碼自動化進行建模，然后對常規智能合約的安全漏洞建立模型。
對功能正確性驗證，必需要人工參與，目前業界還達不到脫離人工參與的水平。VaaS在對工程正確性驗證的部分，先對用戶的代碼和功能的描述進行抽象，自動化建模。之后再通過形式化驗證專家進行前置條件后置條件的定義，然后用輔助證明器去證明。
有了這兩個基礎之后，就能夠實現一鍵式的自動化形式化驗證。
據楊霞介紹，VaaS是目前國際上最領先的形式化驗證產品，可以支持以太坊、Fabric、BCOS、螞蟻BaaS等多個區塊鏈平臺，精確率可以達到95%以上。而且可以一鍵式自動化精確定位出代碼的漏洞以及所在位置。
此外，成都鏈安科技還推出了鷹眼安全態勢感知系統（Beosin-Eagle Eye），采用大數據、人工智能的方法，為區塊鏈上的數據和資產提供安全實時預警和監控，保護用戶的資產安全。 另外推出了智能合約開發平臺（Beosin-IDE），為區塊鏈平臺定制化智能合約的開發環境。
可以看出，成都鏈安科技從區塊鏈開發、安全檢測到運行時的安全監控，構筑了一體化的完整防護體系。
憑借在區塊鏈安全領域過硬的技術實力，成都鏈安科技贏得了大廠的青睞，螞蟻區塊鏈的專家禁不住盛贊：
“可以毫不夸張的說，你們的安全產品的確是全球范圍內最好的！”
成都鏈安科技也順利成為螞蟻區塊鏈創新大賽的安全合作伙伴，為螞蟻BaaS平臺定制智能合約自動化形式驗證的平臺，可以一鍵式檢測常規安全問題，為螞蟻BaaS平臺的區塊鏈應用程序提供深度的安全審計和服務。
據楊霞透露，這個新的平臺預計會在6月份開發出來，并且入駐螞蟻BaaS平臺。
同時，在6月6日，成都鏈安科技參與協辦螞蟻區塊鏈創新大賽成都站Road Show（報名鏈接：活動報名鏈接：https://www.huodongxing.com/event/3494458774400），歡迎各界對區塊鏈感興趣的朋友使用螞蟻BaaS平臺進行區塊鏈的應用開發，可以掃描下面的二維碼進群交流。
（釘釘掃碼進入大賽群）
歡迎大家體驗：
一、智能合約自動形式化驗證平臺VaaS精簡版，準確率達到95%以上
Beosin（成都鏈安科技）已向全球發布VaaS平臺，全球首個同時支持ETH、EOS、Fabric、ONT、TRON等多個區塊鏈平臺的智能合約形式化驗證平臺，準確率達到95%以上。
VaaS（精簡版）系統為所有區塊鏈從業者提供方便而免費的智能合約安全審計服務，對智能合約安全漏洞進行形式化驗證，從容應對常規合約安全問題。歡迎大家登陸官方網址體驗：
官方網址：
https://beosin.com/vaas/index.html#/audit/ptsj
▲VaaS 精簡版平臺
二、在線 Beosin-IDE 免費版本
Beosin-IDE 是一款免費的面向BOS、EOS區塊鏈平臺的智能合約在線集成開發環境，可同時支持合約開發、部署、測試和源碼調試等功能的在線區塊鏈應用開發集成環境。
歡迎大家免費體驗：通過瀏覽器訪問
https://beosin.com/BEOSIN-IDE/index.html#/
（如下圖，推薦Chrome瀏覽器）。
▲Beosin EOS-IDE
Beosin官方發表正式聲明：
為了全球化市場戰略需要，公司發布全新英文品牌 “Beosin”。作為深耕區塊鏈安全領域的公司，“Beosin”力求為行業保駕護航，以打造區塊鏈全生態安全為宗旨，竭誠為客戶提供包括智能合約安全審計、智能合約開發審計一條龍、錢包安全審計、DApp安全加固與審計、區塊鏈平臺安全審計、交易所安全檢測、安全產品定制化服務、企業級安全服務等。但公司英文名稱更名并不涉及業務架構或公司所有權變化。新品牌的Logo如下圖：
近期，有XX鏈安科技與成都鏈安科技重名，且Logo及宣傳語相似。成都鏈安科技是一家由分布式資本、界石資本、盤古創富投資的專門從事區塊鏈安全的公司，與其他XX鏈安科技無任何關聯。請大家認準成都鏈安科技唯一指定商標品牌，謹防上當受騙，一切消息以官網及官方公眾號為準。
成都鏈安科技官方公眾號名稱：Beosin成都鏈安
成都鏈安科技官方網址：
www.lianantech.com
——Beosin
關于Beosin：
Beosin（成都鏈安）成立于2018年，公司位于四川省成都市，專注于區塊鏈生態安全。公司由楊霞和郭文生兩位教授共同創建，團隊核心成員由來自海內外知名高校和實驗室留學經歷的教授、博士后、博士及阿里、華為等知名企業精英組成。已獲得分布式資本、界石資本、盤古創富等著名投資機構的兩輪股權投資。其核心技術為形式化驗證，是全球最早一批將此技術應用到區塊鏈安全領域的公司。
公司首批入選Etherscan智能合約審計推薦名單及普華永道創新加速器，榮獲全國首屆中小微企業SaaS應用創新創業大賽冠軍，獲得OKEx最佳安全審計合作伙伴獎等榮譽，參加工信部多項區塊鏈安全標準的撰寫，入選工信部“2018區塊鏈白皮書”，作為唯一安全公司入選“2018中國區塊鏈企業百強榜”，榮膺金色財經“2018年度最專業安全服務機構”、“2019中國區塊鏈安全領軍企業”稱號，榮獲火星財經“最佳區塊鏈數據安全團隊”獎項，成為2019年區塊鏈技術與數據安全工業和信息化部重點實驗室成員單位。已與Huobi、OKEx、KuCoin、CoinBene、CoinTiger、ONT、Qtum、比原鏈、Wanchain、BOS、Scry、布比區塊鏈、云象區塊鏈、QuarkChain、麥子錢包、EOSPark等共計超過50家區塊鏈公司建立戰略合作關系，審計報告被國內外各大知名交易所認可，為助力本體智能合約安全發布形式化驗證平臺VaaS-ONT。公司審計智能合約超500份，獨立發現區塊鏈安全漏洞幾十種，獲得行業及客戶的一致好評和認可。讓區塊鏈生態更安全，是我們的美好愿景！
「Beosin」
作為Huobi、OKEx、KuCoin
CoinBene、CoinTiger等
著名交易所指定的合約審計公司。?
入選Etherscan智能合約安全審計名單。
歡迎聯系Beosin，了解智能合約安全審計
智能合約開發審計一條龍
錢包安全審計
DApp安全加固與審計
區塊鏈平臺安全審計
交易所安全檢測
安全產品定制化服務
企業級安全服務
?·
電話：028-83262585
網站：www.lianantech.com
郵箱：vaas@lianantech.com
地址：成都市世紀城南路599號
天府軟件園D7座504室
官網：
https://www.lianantech.com
GitHub網址：
https://github.com/Lianantech/VCA
Facebook網址：
https://www.facebook.com/BeosinChengdu/
twitter網址：
https://twitter.com/Beosin_com
Telegram中文群：
https://t.me/LiananTech_cn
Telegram英文群：
https://t.me/LiananTech_en
微博：
https://weibo.com/u/6566884467
CSDN博客：
https://blog.csdn.net/CDLianan
知乎專欄：
??點擊了解更多
總結
以上是生活随笔為你收集整理的区块链女侠杨霞：为区块链代码提供军事级的安全检测丨蚂蚁区块链大赛成都站火热报名...的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： itextpdf 怎么下划线_java
- 下一篇： 优秀的WEB应用程序