近期，筆者注意到一款智能合約自動形式化驗證工具Beosin—VaaS推出了離線免費版。所謂“離線免費版”，相較于之前該公司推出的在線免費版、企業(yè)版而言，亮點自然不言而喻。對于開發(fā)者來說，離線版的驗證工具將提供一個不聯(lián)網(wǎng)的測試環(huán)境，在很大程度上能從根源上將黑客攻擊的可能拒之門外。

經(jīng)筆者測試，雖然這次推出的版本為免費版，但功能毫不遜色，依然能有效檢測出智能合約的常規(guī)安全漏洞，并精確定位到有風(fēng)險的代碼位置，以及導(dǎo)開發(fā)者修改合約代碼。對大多數(shù)智能合約的安全性而言，需求都已經(jīng)滿足。

盡管筆者認(rèn)為離線免費版Beosin—VaaS的功能已足夠強(qiáng)大，但根據(jù)官方發(fā)布的消息，對于一些復(fù)雜類型的業(yè)務(wù)合約、以及對安全性要求高的業(yè)務(wù)合約，比如數(shù)字金融類（如DeFi）、物流供應(yīng)鏈類、跨境支付類、防偽溯源類等等，還是建議選擇企業(yè)版Beosin—VaaS或人工審計服務(wù)更好。

下面筆者將針對這款離線免費版Beosin—VaaS工具進(jìn)行簡單展述。

1.?什么是形式化驗證技術(shù)？

其實，形式化驗證技術(shù)最早是應(yīng)用于航空、軍事等領(lǐng)域的安全關(guān)鍵軟件中的技術(shù)，本身受眾范圍沒那么廣。當(dāng)成都鏈安最早嘗試將形式化驗證技術(shù)應(yīng)用在驗證智能合約的安全性上，最后發(fā)現(xiàn)審計效果比起傳統(tǒng)的驗證方式，更具備優(yōu)勢。

形式化驗證技術(shù)是一種基于數(shù)學(xué)和邏輯學(xué)的方法。具體來講，在智能合約部署之前，對其代碼和文檔進(jìn)行形式化建模，然后通過數(shù)學(xué)的手段對代碼的安全性和功能正確性進(jìn)行嚴(yán)格的證明，可有效檢測出智能合約是否存在安全漏洞和邏輯漏洞。

該方法可有效彌補(bǔ)傳統(tǒng)靠人工經(jīng)驗查找代碼邏輯漏洞的缺陷，其優(yōu)勢在于，用傳統(tǒng)的測試等手段無法窮舉所有可能輸入，而用數(shù)學(xué)證明的角度，就能克服這一問題，提供更加完備的安全審計。

2.?什么是Beosin—VaaS工具？

Beosin—VaaS相關(guān)工具就是將形式化驗證技術(shù)應(yīng)用在對智能合約安全性驗證的集大成者。Beosin—VaaS能夠面向EVM和WASM智能合約，自動化檢測智能合約的10大項32小項常規(guī)安全漏洞，為智能合約提供“軍事級”的安全保護(hù)；并精準(zhǔn)定位風(fēng)險代碼位置并給出修改建議；檢測準(zhǔn)確率>97%，全球最高；從源碼到字節(jié)碼完備的形式化驗證；支持多個智能合約編程語言，如Solidity、Go、C++、Python等。

3.?一些Beosin—VaaS的測試實例

筆者選取了655個測試問題進(jìn)行檢測，Beosin—VaaS工具總計檢測出635個問題，命中率為96.9%；誤報共115個，誤報率為15.3%。因此，Beosin—VaaS工具可檢測出業(yè)務(wù)類大多合約案例，具體檢測項如下：

通過大體測試，離線免費版自動形式化驗證工具Beosin—VaaS在很大程度上都能夠滿足大多數(shù)開發(fā)者的驗證需要。歡迎大家進(jìn)行體驗。