形式化验证

一个案例说明高层属性形式化验证

Beosin-VaaS的业务逻辑验证软件，是一款用来检测智能合约上层业务逻辑漏洞的软件。

• 成都链安
• 发布于 2020-01-10
• 阅读 ( 3133 )
• ( 16 )

成都链安推出全球首个Fabric链码自动形式化验证工具--Beosin-VaaS for Fabric

近日，成都链安推出全球首个Fabric链码自动形式化验证工具--Beosin-VaaS for Fabric，为链码提供“军事级”的安全验证。

• 成都链安
• 发布于 2019-12-26
• 阅读 ( 3095 )
• ( 2 )

关于形式化验证两大工具(Vass & Mythril) 测试对比

随着以智能合约（Smart Contract）及区块链应用（DApp）为核心的区块链2.0时代逐渐成为主流，智能合约及区块链应用的安全性也越发成为业界备受关注的焦点。尤其是，在经历过诸如THE DAO、币安被盗等事件，智能合约及区块链应用的安全性究竟应该如何得到验证和保障，业已成为当前区块链业界亟待解决的痛点。

• 成都链安
• 发布于 2019-10-15
• 阅读 ( 10093 )
• ( 20 )

基于VS-Code插件的智能合约自动形式化验证工具Beosin-Vaas离线免费版

• 成都链安
• 发布于 2019-11-05
• 阅读 ( 8225 )
• ( 20 )

Move智能合约的形式化验证工具

“程序测试能证明错误的存在, 但不能证明错误不存在” – Edsger Dijkstra。智能合约是一个对安全性要求非常高的领域，一个不经意的小 bug 很可能会导致不可估量的损失。

• Young Rocks
• 发布于 2022-01-20
• 阅读 ( 4379 )
• ( 10 )

技术详解 | 如何对Cosmos SDK标准模块进行形式化验证

    in  Web3.0安全开发实践

CertiK完成了针对CosmosSDK形式化验证。形式化验证是一项运用数学逻辑来确保系统符合规范，使其在所有可能的输入和条件下都如预期表现的技术。本文将介绍形式化验证CosmosSDKBank模块的具体步骤，以及一些验证结果。

• CertiK
• 发布于 2024-12-03
• 阅读 ( 281 )
• ( 13 )