近期，筆者注意到一款智能合約自動形式化驗證工具Beosin—VaaS推出了離線免費版。所謂“離線免費版”，相較于之前該公司推出的在線免費版、企業(yè)版而言，亮點自然不言而喻。對于開發(fā)者來說，離線版的驗證工具將提供一個不聯(lián)網(wǎng)的測試環(huán)境，在很大程度上能從根源上將黑客攻擊的可能拒之門外。
經(jīng)筆者測試，雖然這次推出的版本為免費版，但功能毫不遜色，依然能有效檢測出智能合約的常規(guī)安全漏洞，并精確定位到有風險的代碼位置，以及導開發(fā)者修改合約代碼。對大多數(shù)智能合約的安全性而言，需求都已經(jīng)滿足。
盡管筆者認為離線免費版Beosin—VaaS的功能已足夠強大，但根據(jù)官方發(fā)布的消息，對于一些復雜類型的業(yè)務合約、以及對安全性要求高的業(yè)務合約，比如數(shù)字金融類（如DeFi）、物流供應鏈類、跨境支付類、防偽溯源類等等，還是建議選擇企業(yè)版Beosin—VaaS或人工審計服務更好。
下面筆者將針對這款離線免費版Beosin—VaaS工具進行簡單展述。
1. 什么是形式化驗證技術(shù)？
其實，形式化驗證技術(shù)最早是應用于航空、軍事等領(lǐng)域的安全關(guān)鍵軟件中的技術(shù)，本身受眾范圍沒那么廣。當成都鏈安最早嘗試將形式化驗證技術(shù)應用在驗證智能合約的安全性上，最后發(fā)現(xiàn)審計效果比起傳統(tǒng)的驗證方式，更具備優(yōu)勢。
形式化驗證技術(shù)是一種基于數(shù)學和邏輯學的方法。具體來講，在智能合約部署之前，對其代碼和文檔進行形式化建模，然后通過數(shù)學的手段對代碼的安全性和功能正確性進行嚴格的證明，可有效檢測出智能合約是否存在安全漏洞和邏輯漏洞。
該方法可有效彌補傳統(tǒng)靠人工經(jīng)驗查找代碼邏輯漏洞的缺陷，其優(yōu)勢在于，用傳統(tǒng)的測試等手段無法窮舉所有可能輸入，而用數(shù)學證明的角度，就能克服這一問題，提供更加完備的安全審計。
2. 什么是Beosin—VaaS工具？
Beosin—VaaS相關(guān)工具就是將形式化驗證技術(shù)應用在對智能合約安全性驗證的集大成者。Beosin—VaaS能夠面向EVM和WASM智能合約，自動化檢測智能合約的10大項32小項常規(guī)安全漏洞，為智能合約提供“軍事級”的安全保護；并精準定位風險代碼位置并給出修改建議；檢測準確率>97%，全球最高；從源碼到字節(jié)碼完備的形式化驗證；支持多個智能合約編程語言，如Solidity、Go、C++、Python等。
3. 一些Beosin—VaaS的測試實例
筆者選取了655個測試問題進行檢測，Beosin—VaaS工具總計檢測出635個問題，命中率為96.9%；誤報共115個，誤報率為15.3%。因此，Beosin—VaaS工具可檢測出業(yè)務類大多合約案例，具體檢測項如下：
通過大體測試，離線免費版自動形式化驗證工具Beosin—VaaS在很大程度上都能夠滿足大多數(shù)開發(fā)者的驗證需要。歡迎大家進行體驗。
申請創(chuàng)業(yè)報道，分享創(chuàng)業(yè)好點子。點擊此處，共同探討創(chuàng)業(yè)新機遇！
