文章 视频 课程 百科图谱 集训营
更多
  • 问答
  • 提问
  • 发表文章
  • 专栏
  • 活动
  • 文档
  • 工作
  • 集市
  • 发现
  • 文章
  • 问答
  • 视频
  • 课程
  • 集训营
  • 专栏
  • 活动
  • 工作
  • 文档
  • 集市
搜索
  • 登录/注册
Certora
  • 文章
  • 专栏
  • 问答
  • 视频
  • 课程
  • 集市作品
  • 活动
  • 招聘
TA的文章 TA购买的 TA喜欢的 TA收藏的
Concordance:利用 LLM 安全地简化复杂智能合约

Certora 发布了一款名为 Concordance 的开源工具,它利用 LLM 自动简化复杂的智能合约代码,同时使用 Concord 等价性检查器来保证代码行为不变。Concordance 通过迭代地简化代码,并使用 Concord 验证 LLM 提出的修改方案,从而帮助开发者更容易地理解和审计复杂的智能合约。

智能合约  LLM  形式化验证  代码审计  Concordance  等价性检查 
发布于 2025-09-13 13:18 阅读(384) 点赞(0) ( 21 )
分享
Twitter分享
微信扫码分享
Rust智能合约安全竞赛 - 赛后感

Certora举办了首次针对Rust的形式化验证竞赛,并与Code4rena和Cantina合作,为Soroban智能合约举办了两次社区竞赛。文章介绍了如何使用Certora的工具(如Sunbeam)和Rust库(如CVLR)进行形式化验证,并通过Blend v2和Aquarius两个竞赛的例子展示了形式化验证在发现智能合约漏洞中的应用。

形式化验证  Rust  智能合约  Soroban  Certora Prover  CVLR 
发布于 2025-09-12 09:20 阅读(354) 点赞(0) ( 17 )
分享
Twitter分享
微信扫码分享
Certora 竞赛报告:Aquarius

本文是 Certora 对 Aquarius 项目进行的形式化验证竞赛报告,通过引入代码突变来评估参赛者编写的规范质量。报告详细列举了在 AccessControl、FeesController 和 Upgrade 等合约中发现的突变,展示了参赛者提交的高质量属性,并强调了发现的真实漏洞,如 Pending Upgrade 的 Code Hash 未被清除等问题。

形式化验证  智能合约  Certora Prover  代码突变  AccessControl  FeesController  漏洞 
发布于 2025-08-27 19:42 阅读(158) 点赞(0) ( 7 )
分享
Twitter分享
微信扫码分享
Coinbase 2025 年 5 月事件中的运营安全教训

Coinbase 遭受了一起数据泄露事件,起因是不良行为者收买海外客服人员出售客户数据,攻击者利用获取的信息进行进一步的社会工程攻击。文章强调了零信任架构的重要性,以及数据分类和权限管理在保护敏感数据方面的作用。Web3 技术需要采用更严格的安全措施,才能吸引传统机构和主流投资者。

数据泄露  社会工程攻击  零信任架构  数据分类  权限管理  Web3 安全 
发布于 2025-08-21 09:06 阅读(267) 点赞(0)
分享
Twitter分享
微信扫码分享
Certora验证器8.1.0版本发布,包含新功能和重大变更

Certora Prover v8.1.0 版本发布,引入了多项重大变更,包括最低 Java 和 Python 版本要求提升、默认启用健全性检查、requireInvariant 语义更新、Solana 和 Soroban 验证需使用专用命令、默认报告链接改为私有、CVL 函数支持 revert 处理等。

形式化验证  Certora Prover  breaking changes  Solana  Soroban  CVL 
发布于 2025-08-12 08:28 阅读(344) 点赞(0) ( 9 )
分享
Twitter分享
微信扫码分享
Certora 通过形式化验证技术确保智能合约安全

本文讨论了Web3应用安全问题,特别关注智能合约的形式化验证。Certora通过形式化验证技术确保智能合约安全,并总结了五个Rust智能合约开发最佳实践,包括保持代码模块化、利用编译器检查、简化数据结构、减少trap value状态以及分离核心逻辑与副作用,以提高代码的可验证性和安全性。

Web3  智能合约  正式验证  Rust语言  Soroban  Solana 
发布于 2025-08-07 09:14 阅读(487) 点赞(0) ( 14 )
分享
Twitter分享
微信扫码分享
使用 Certora Prover 形式化验证确保 infiniFi 中公平的赎回

infiniFi 是一个 DeFi 平台,旨在优化收益,但其 iUSD 赎回机制存在漏洞,可能导致用户在赎回队列中被跳过,从而面临不公平的惩罚。Certora Prover 发现了这一问题,并通过形式化验证确保了修复后的系统符合 FIFO 原则,维护了用户信任和 DeFi 协议的公平性。

DeFi  形式化验证  Certora Prover  FIFO  智能合约  iUSD 
发布于 2025-07-01 10:44 阅读(641) 点赞(0) ( 13 )
分享
Twitter分享
微信扫码分享
利用形式化验证查找编译器 Bug

本文介绍了Certora团队开发的一款用于验证编译器优化的等价性检查工具,该工具通过比较优化前后程序的行为来检测编译器bug。文章还分享了该工具在Vyper编译器中发现的一个优化bug,该bug导致局部变量被错误地映射到相同的堆栈位置,从而改变了程序的行为。该bug已在Vyper 0.4.2版本中修复。

编译器优化  等价性检查  形式化验证  Vyper  Certora Prover  bug检测 
发布于 2025-07-01 09:43 阅读(606) 点赞(0) ( 3 )
分享
Twitter分享
微信扫码分享
使用 Certora Prover 形式验证确保 infiniFi 中公平的赎回

infiniFi 是一个 DeFi 平台,通过管理 Pendle、AAVE 和 Ethena 等协议上的存款来优化收益。

DeFi  iUSD  Certora Prover  FIFO  赎回队列  形式化验证 
发布于 2025-07-01 09:42 阅读(835) 点赞(0) ( 13 )
分享
Twitter分享
微信扫码分享
Silo Finance 杠杆合约攻击事件事后分析

Silo Finance 的一个新杠杆合约模块在测试阶段遭到攻击,由于过于宽泛的批准设置导致借款操控漏洞。该模块与核心Silo协议隔离,因此核心协议、金库、市场或用户资金未受影响。Certora 此前对该合约进行了安全审查,但未发现此漏洞,事后进行了风险评估和补救措施,并确认现有Silo代码是安全的。

Silo Finance  杠杆合约  安全漏洞  Certora  风险评估  形式化验证  智能合约 
发布于 2025-06-28 09:40 阅读(611) 点赞(0) ( 5 )
分享
Twitter分享
微信扫码分享
  • ‹
  • 1
  • 2
  • 3
  • 4
  • 5
  • ›
文章删除后将不可恢复 !
删除 取消
一键转载
转载文章不用复制粘贴和编辑,输入原文链接,交给后台发布!
暂只支持: 微信公众号、Mirror、Medium的文章链接
提交后可在个人主页查看文章发布状态
提交
提交成功!
系统处理完成后将直接进入审核发布流程,可在个人主页关注文章状态。
Certora
Certora
贡献值: 485 学分: 171
Securing DeFi through smart contract audits, formal verification, and protocol design reviews.
0 关注 3 粉丝
关于
关于我们
社区公约
学分规则
Github
伙伴们
DeCert
ChainTool
GCC
UpChain
合作
广告投放
发布课程
联系我们
友情链接
关注社区
Discord
Twitter
Youtube
B 站
公众号

关注不错过动态

微信群

加入技术圈子

©2025 登链社区 版权所有 | Powered By Tipask3.5|
粤公网安备 44049102496617号 粤ICP备17140514号 粤B2-20230927 增值电信业务经营许可证

发送私信

请将文档链接发给晓娜,我们会尽快安排上架,感谢您的推荐!

提醒

检测到你当前登录的账号还未绑定手机号
请绑定后再发布
去绑定
编辑封面图
封面预览