P-Token是SPL Token的Pinocchio重实现，减少约95%计算单元消耗，作为直接替代品。Certora使用形式化验证证明P-Token与SPL Token在共享指令上的等价性：无panic、成功时状态字节一致、失败时错误相同（除三个有意行为差异）。验证覆盖所有共享指令，未发现可利用漏洞。

Certora获得Canton开发基金资助，将为Canton Network上的Daml项目构建开源静态分析工具。该工具分析编译后的.dar文件，检测跨包交互并可视化，帮助金融机构在部署前理解智能合约的隐私和安全影响。工具将集成到dpm命令行工具中，以Apache 2.0许可发布，降低安全与合规团队的审计负担。

本文介绍了威胁建模在智能合约安全中的重要性，重点阐述了Certora开发的4A框架（资产、参与者、假设、攻击向量）和STRIDE框架（欺骗、篡改、否认、信息泄露、拒绝服务、权限提升），并说明如何结合使用这两种方法提升DeFi项目的安全性。文章强调威胁建模应尽早开始、持续更新，并与审计流程结合，以最小开销获得最大安全可见性。

文章深入分析了 Kelp DAO 在 LayerZero 协议上的 rsETH 安全事件。由于 Kelp 错误地采用了 1-of-1 的 DVN（去中心化验证网络）配置，导致单一故障点。攻击者通过替换 RPC 节点的二进制文件并配合 DDoS 攻击，成功伪造了跨链消息，窃取约 2.9 亿美元。文章强调，跨链桥安全不仅在于合约逻辑，更在于底层基础设施的去中心化与冗余。建议开发者采用 N-of-M 多重验证、异构 RPC 节点及完善的熔断机制，以应对针对基础设施的复杂攻击。

这篇文章主要介绍了 Certora Prover 的新更新，包括 CVL 中新增的 links 块，用于更直观、类型安全地把合约存储变量绑定到目标合约；TAC dump 的可视化诊断能力增强，支持前进后退、变量联动高亮和数据流图；以及 requireInvariant 在强不变量场景下的语义改进，降低外部调用后出现误报反例的概率。同时，文章还说明了 GitHub App 的评论配置新选项 gh-review 与 gh-review-jobs，并给出升级到 8.11.3 的方式。

本文是针对在 Stellar 平台上开发 Soroban 智能合约项目的安全审计准备指南。内容涵盖了从设计阶段的威胁建模（STRIDE）、编写易于验证的 Rust 代码、进行模糊测试，到利用自动化工具（如 Scout 和 Sunbeam）进行预审计的完整流程，旨在帮助开发者在申请 Stellar 审计银行资助前提升代码安全性。

文章深入探讨了跨链资产交换中的承诺-揭示协议（如HTLC），指出在区块链存在延迟最终性和重组风险时，若参与者“仓促”操作而不等待区块确认，协议的“去信任”属性将失效。作者通过分析PreHTLC的逻辑漏洞，证明了在缺乏跨链最终性证明的情况下，完全去信任的原子交换在现实中难以实现。

Certora 对 Sui 链上的借贷协议 Suilend 进行了形式化验证，重点分析了系统级不变量。验证涵盖了偿付能力、账户健康度以及清算盈利性三个维度，识别并修复了包括双重舍入漏洞、算术舍入漂移以及特定 LTV 条件下清算导致资产状况恶化等技术问题，确保了协议的整体安全性。

文章探讨了BLS签名聚合中的一个关键漏洞，即共轭签名问题，该问题可能导致验证错误，并影响区块链协议中的不可抵赖性和消息绑定。通过一个具体案例分析了签名聚合被误用作批量验证时的潜在风险。

本文作者分享了在Web3领域工作八个月以来，在DeFi安全方面的一些经验教训，并强调了OpSec的重要性。文章提出了OpSec的五个关键步骤，包括多因素身份验证（MFA）、端点检测与响应（EDR）、密码管理、管理账户使用以及冷存储根账户，同时还提供了在安全事件发生时的应对措施。