形式化驗證工具之離線免費版beosin—vaas
儘管筆者認為離線免費版beosin—vaas的功能已足夠強大，但根據官方發布的訊息，對於一些複雜型別的業務合約、以及對安全性要求高的業務合約，比如數字金融類（如defi）、物流**鏈類、跨境支付類、防偽溯源類等等，還是建議選擇企業版beosin—vaas或人工審計服務更好。
下面筆者將針對這款離線免費版beosin—vaas工具進行簡單展述。
1.什麼是形式化驗證技術？
其實，形式化驗證技術最早是應用於航空、軍事等領域的安全關鍵軟體中的技術，本身受眾範圍沒那麼廣。當成都鏈安最早嘗試將形式化驗證技術應用在驗證智慧型合約的安全性上，最後發現審計效果比起傳統的驗證方式，更具備優勢。
**形式化驗證技術是一種基於數學和邏輯學的方法。**具體來講，在智慧型合約部署之前，對其**和文件進行形式化建模，然後通過數學的手段對**的安全性和功能正確性進行嚴格的證明，可有效檢測出智慧型合約是否存在安全漏洞和邏輯漏洞。
該方法可有效彌補傳統靠人工經驗查詢**邏輯漏洞的缺陷，其優勢在於，用傳統的測試等手段無法窮舉所有可能輸入，而用數學證明的角度，就能克服這一問題，提供更加完備的安全審計。
2.什麼是beosin—vaas工具？
beosin—vaas相關工具就是將形式化驗證技術應用在對智慧型合約安全性驗證的集大成者。beosin—vaas能夠面向evm和wasm智慧型合約，自動化檢測智慧型合約的10大項32小項常規安全漏洞，為智慧型合約提供**「軍事級」的安全保護**；並精準定位風險**位置並給出修改建議；檢測準確率》97%，全球最高；從原始碼到位元組碼完備的形式化驗證；支援多個智慧型合約程式語言，如solidity、go、c++、python等。
3.一些beosin—vaas的測試例項
筆者選取了655個測試問題進行檢測，beosin—vaas工具總計檢測出635個問題，命中率為96.9%；誤報共115個，誤報率為15.3%。因此，beosin—vaas工具可檢測出業務類大多合約案例，具體檢測項如下：
beosin—vaas工具檢測項
漏洞檢測項
beosin—vaas工具
erc20 標準規範
√fake recharge vulnerability（假充值）
√transfertozeroaddress（目標零位址檢測）
√re entrancy（重入）
√txoriginauthentication（tx.origin使用錯誤）
√invoke low level calls（call呼叫,delegatecall呼叫,自殺函式呼叫）
√blockmembers manipulation（區塊引數依賴）
√invoke extcodesize（呼叫extcodesize函式）
√invoke ecrecover（呼叫ecrecover函式）
√unchecked call or send return values
√（call和send的返回值檢測）
√redefine variable from base contracts（合約繼承中的變數覆蓋）
√unprotected ether withdrawal（無保護的轉賬）
×check this balance（合約資金受到嚴格限制）
√arbitraryjumpwith function（具有函式型別變數的任）
√overload assert（重寫assert函式）
√compilerversiondeclaration（編譯器版本宣告）
√constructor mistyping（建構函式失配）
√unary operation（+= 寫成=+ ）
√no return（返回值適配）
√unchecked api return values（沒檢查api返回值）
√emit event beforerevert(事件在revert前觸發了)
√integer overflow（整數溢位）
√exception state(異常檢測，包括陣列越界、除0、assert失敗等)）
√call problem
√function problem
√require fail
√通過大體測試，離線免費版自動形式化驗證工具beosin—vaas在很大程度上都能夠滿足大多數開發者的驗證需要。大家可以前往進行體驗，不吝賜教。
關於軟體形式化驗證
軟體開發中一般使用 測試 來找bug，這種方法只能找到bug，不能證明程式沒有bug。形式化驗證是用邏輯來驗證程式的可靠性，就是把一段程式用邏輯的方法證明一遍，證明它能得到預期的結果，沒有bug。一般這類研究主要應用於昂貴的航天器材的作業系統 危險的醫療裝置的程式之中。因為航天器材 醫療裝置牽扯到人...
區塊鏈時代 形式化驗證的應用
區塊鏈時代，智慧型合約的安全性被無限放大，乙個小小的bug就能導致上億美元的損失。美鏈 bec 近日被爆出安全漏洞，被黑客用以太坊erc 20智慧型合約中batchoverflow漏洞攻擊，引發 閃崩，當日幣價幾乎歸0。除了美鏈，據英國和新加坡的研究人員統計，超過34000個智慧型合約都有可被利用的...
智慧型合約形式化驗證工具真能解決問題麼？
在智慧型合約的形式化驗證過程中，需要專業的程式設計人員對不同模板的智慧型合約進行特徵分析 模型建立和模型驗證。現在市場上出現了一些一鍵式的智慧型合約形式化驗證工具，據說可以最大程度的減少驗證程式 發現bug，提高工作效率。這種一鍵式的智慧型合約形式化驗證工具真的有效麼？為了求真筆者做了乙個測試。本次...