CertiK推形式化驗證 助數資企業合規 數學方法識別安全漏洞 區塊鏈與傳統金融融合提供安全保障
香港數字資產持牌機構首要挑戰向來是合規，近期開始有區塊鏈安全公司自行研發驗證技術，提升數字資產企業的合規效率。區塊鏈安全企業CertiK聯合創始人兼CEO顧榮輝表示，形式化驗證技術正成為提升區塊鏈安全與合規效率的關鍵利器。該技術以數學方法證明代碼與設計規範完全一致，能精準發現漏洞，更可確保項目符合監管要求。目前CertiK已在香港針對本地政策推出數字資產形式化驗證服務，幫助企業以更高確定性通過牌照審批。傳統測試能發現「已知漏洞」，但不能證明錯誤不存在。而形式化驗證則是通過數學方法證明「設計與實現無歧義」，為區塊鏈與傳統金融融合提供更可靠的安全保障。
●香港文匯報記者 黃安琪
顧榮輝在接受香港文匯報訪問時表示，安全技術形式化驗證在提升區塊鏈安全性方面具有重要作用，能夠為香港監管機構和持牌方減輕合規負擔，提升合規效率。顧榮輝稱，該公司正與多家企業在多個鏈上項目中展開形式化驗證合作。形式化驗證的技術通過數學的方法去證明這個代碼它滿足某個性質，從而可抵禦相應類型的攻擊。相比於傳統測試手段，儘管形式化驗證的成本相對較高，但一旦完成某個性質的證明，系統的防護能力將顯著增強。
突破傳統安全技術局限
顧榮輝補充，最初該技術主要用於驗證代碼符合設計規範並識別漏洞；而現在它不僅能夠識別安全漏洞，還能有效查明不符合監管要求的地方。他解釋，傳統安全方法通常採用多種輸入和運行環境進行測試，以識別系統中的異常。因此，傳統安全手段主要用於發現現有漏洞，證明這些漏洞的存在。然而，如果沒有找到漏洞，並不能證明漏洞不存在。即使系統已運行多年，依然可能潛藏未被發現的問題，這正是傳統安全技術的局限所在。
他又解釋，形式化驗證的核心思路在於確保軟件系統的設計與其實現代碼之間的一致性。具體來說，軟件開發者首先根據特定的合規要求制定設計方案。然而，在將設計轉化為實際代碼的過程中，可能會出現偏差，導致實現與原設計不完全一致。這種不一致性可能會引發安全漏洞或合規性問題。因此，形式化驗證通過數學方法確保設計和實現之間的對齊，從而提高系統的安全性與合規性。
他進一步解釋，形式化驗證的過程包括將設計轉換為數學計算模型，並將實現代碼同樣轉化為計算模型。通過應用數學方法，對這兩個計算模型進行比較，以證明它們是否一致。如果兩個計算模型不一致，則可識別出潛在漏洞；反之，若證明它們是一致的，即表明實現代碼與原設計在邏輯上是相符的，從而確認代碼中未出現漏洞。因此，所謂漏洞的定義在於實現與設計之間存在的差異。
已識別逾18萬個安全漏洞
顧榮輝表示，作為全球最大的區塊鏈安全公司，CertiK於2021年成為獨角獸，現估值超過20億美元，全球市場份額估計達到30%至40%。公司至今已通過形式化驗證技術等工具，識別出超過18萬個安全漏洞，成為許多傳統機構和銀行在研究區塊鏈技術以進行業務升級時的首選合作夥伴。越來越多的金融機構，包括不同地區的銀行，成為CertiK的客戶。
他強調，區塊鏈與傳統金融體系的區別顯現，帶來了諸多新風險，包括智能合約風險、鏈本身的風險及合規性風險，如洗錢和制裁等問題。這些風險對新進入的企業構成障礙，因為它們往往缺乏充分的理解。而CertiK的目標是通過提供技術產品和服務，幫助企業識別、理解並預防這些風險，從而使其能夠更專注於核心業務的發展。
