CertiK是一家区块链安全公司,以其在智能合约审计方面的专业知识和全面的安全工具套件而闻名。CertiK成立于2018年,专注于提高区块链网络和智能合约的安全性和可靠性。
CertiK由耶鲁大学和哥伦比亚大学的计算机科学教授于2018年创立。[22] 联合创始人Ronghui Gu教授于2022年获得VMware系统研究奖[23],并且是新加坡金融管理局国际技术咨询委员会成员[24]。
CertiK提倡一种全面的安全方法,包括智能合约审计、形式化验证、渗透测试和高级安全监控工具。该公司还积极参与研发,为包括苹果[20]、三星[21]和Sui[30]在内的主要公司的区块链安全做出贡献。
CertiK已与超过4,000家企业客户合作,保护了超过3600亿美元的数字资产,并在区块链代码中发现了超过60,000个漏洞。该公司的客户包括Aave[27]、Polygon[26]、BNB Chain[25]、Aptos[28]和WEMIX[29]等项目。
CertiK免费公开所有审计报告,以努力提高Web3的安全性和透明度。在项目的Skynet页面上可以找到所有已识别漏洞的完整分解以及它们是否已得到解决。
CertiK提供许多其他工具,旨在帮助项目方和投资者采取充分知情且端到端的安全和尽职调查方法。
CertiK的安全评分排行榜根据项目的安全评分对其进行列表和排名。安全评分是使用专有算法生成的,该算法考虑了项目的代码安全、基本健康、运营弹性、社区信任、市场稳定性和治理强度。
已验证团队排行榜根据其CertiK KYC徽章的状态列出并排名项目。成功通过背景调查的项目团队将获得CertiK KYC徽章,该徽章分为金、银和铜三种。
影响者得分排行榜列出并根据Web3影响者的影响力得分对其进行排名,该得分反映了他们的内容和在线形象的影响力和覆盖范围。对于有兴趣识别正在塑造Web3对话的影响者的用户来说,此排行榜很有帮助。
交易所审计允许用户通过显示中心化交易所 (CEX)控制的钱包地址中的链上资产持有量,对中心化交易所 (CEX) 进行尽职调查。这是储备金证明验证的重要第一步。
Skynet Alerts 是一个系统,可以及时通知加密货币领域的退出诈骗和漏洞利用。Skynet Alerts 不断监控各种信息来源,以识别和报告可能发生的 rugpull 和漏洞利用。
Smart Money Wizard是Wallet Analyzer功能的入口点,使用户可以直接搜索钱包地址、查看热门钱包搜索、顶级聪明钱钱包和顶级流动性对。Wallet Analyzer功能提供关于钱包地址的见解,并通过显示关键钱包特征、可视化钱包关系和代币交易活动,轻松解读钱包之间的链上交易。
SkyInsights是一个综合性的加密货币合规和风险管理平台。它提供钱包筛选、实时交易监控、风险评分和可定制的警报,以帮助金融机构、中小型企业和加密原生平台有效地管理合规复杂性。SkyInsights帮助暴露于加密货币的组织高效地应对监管环境,同时保持高效的流程并增强客户信任。
CertiK KYC 为项目团队提供全面且私密的身份验证。CertiK 与每位团队成员进行实时视频通话,以验证其身份和其他必要参数。由于团队匿名性日益助长高风险行为,CertiK 的 KYC 有助于建立项目责任制,使投资者能够更有信心地前进。获得铜牌、银牌或金牌 KYC 徽章的项目向其社区表明,他们愿意公开支持他们的项目。
渗透测试是确保加密应用程序在运行时环境中安全性的综合方法的最后组成部分。CertiK的渗透测试服务利用专有工具,并由经验丰富的道德黑客团队提供支持,从而发现漏洞。
CertiK的漏洞赏金计划通过众包顶级道德黑客的智慧,在恶意行为者利用漏洞之前发现它们。CertiK的安全工程师筛选并评估提交的内容,并与客户合作实施正确的修复。0%的费用模式减轻了项目的支付压力,并允许白帽黑客获得全额赏金。
SkyTrace是一个追踪工具,旨在帮助分析和可视化跨以太坊和BNB链钱包的交易数据。 该工具提供可操作的见解,用于识别和追踪可疑的资金流动,无论这些流动是进出个人钱包还是项目团队钱包。
CertiK咨询提供一个分析师团队,他们提供技术评估、专有研究和战略建议。
CertiK 的安全服务适用于所有区块链上的所有项目。该公司合作过的生态系统列表包括:
形式化验证涉及对智能合约或区块链协议的功能进行数学证明,确保其按预期运行,不会遗漏任何漏洞[31]。CertiK 的形式化验证方法比单纯的人工分析能发现更广泛的漏洞。
该公司的形式化验证过程优先考虑可扩展性、精确性和覆盖范围。对于像 ERC-20 和 ERC-721 这样的流行智能合约,CertiK 已经实现了常见安全属性的自动化验证,并在审计阶段成功地将其应用于数百个项目。CertiK 的形式化验证通过指定和证明高级自定义安全性和正确性属性(例如自动做市商 (AMM) 的 increase-K 属性)来增强常规审计,适用于复杂的智能合约。此外,CertiK 的形式化验证还扩展到其他区块链构建块,包括共识协议,甚至像 HyperEnclave TEE 这样的基本系统基础设施[32]。
CertiK 的安全审计方法的定义是使用人工代码审查、自动验证和自定义形式化验证。虽然人工代码审查和自动验证在行业中很常见,但自定义形式化验证提高了审计的有效性。在此过程中,安全专家创建机器可读的规范,然后由 CertiK 的自定义形式化验证系统进行数学验证。这种方法确保了更有效的安全评估,针对每个项目的独特功能和语言量身定制。
对于区块链协议,CertiK 通过智能合约和去中心化应用程序 (dApp)的形式化验证提供定制的解决方案,旨在培育一个更具功能性和值得信赖的区块链生态系统。该公司的学术界、研究人员和工程师团队为每个项目开发高度定制的解决方案,确保彻底有效的审计过程。
DeepSEA是由CertiK开发的智能合约的形式化验证编译器。它是Web3形式化验证领域的一项先进解决方案。它旨在解决两个关键问题:编译器中的潜在错误,这可能导致正确编写的智能合约中出现安全漏洞;以及验证工具链中的不准确性,这可能会使形式化验证的保证失效。DeepSEA的创建基于这样的认识:随着验证对程序本身的逻辑给予更多的信心,确保周围执行环境的准确性变得越来越重要。
DeepSEA通过获取用高级语言(如Solidity、Rust、Vyper等)编写的合约源代码,并将其翻译成区块链平台(EVM、WebAssembly等)的可执行字节码来运行。该项目源于改进执行环境的研究,特别是关注编译器方面。DeepSEA是用Coq的内置编程语言(Gallina)编写的,并分为多个细粒度阶段,以提高验证效率。
DeepSEA支持两个目标:EVM字节码和以太坊风格的WebAssembly(eWASM)。它能够编译DeepSEA表面语言,并作为其他智能合约编程语言的后端。编译器正确性的验证包括定义输入和输出的编程语言及其语义,发明和定义输入和输出语言中程序状态之间的“match_states”关系,并证明编译后的程序状态与原始程序的状态一致。
DeepSEA还集成了编译和形式化验证。这种集成使得可以在高层次上验证程序,同时确保验证的安全属性与编译后的字节码一致。随着技术的进步,CertiK对DeepSEA的愿景是让编译器和验证工具都在一个统一的核心语言上运行,并具有形式化验证的编译器后端。
CertiK 与领先的数字资产交易所建立了战略合作伙伴关系,例如 Binance[34]、OKX[35]、KuCoin[36] 和 Huobi[33]。
2023 年,Sui 向 CertiK 奖励了 50 万美元的赏金,以表彰其发现了一个名为“HamsterWheel”的关键漏洞,该漏洞对整个区块链构成风险。
CertiK 验证了 The Open Network (TON) 的每秒交易记录,证明了该链处理高吞吐量区块链项目的能力[37]。
该公司成功地对蚂蚁集团 Trust Native Technology 团队的 HyperEnclave 进行了形式验证,并审计了 XLS-30d[38],这是一个建立在 XRP Ledger 上的 自动化做市商 (AMM)。
CertiK 还与阿里云建立了战略合作伙伴关系[39],旨在加强云计算领域的区块链安全。此外,该公司与 Finschia 合作,在进行全面的安全审查后,担任治理成员和节点验证器[40]。
在人道主义努力中,CertiK 与 Coala Pay 合作,简化资金筹集,将区块链技术与社会责任相结合[41]。
该公司将其专业知识扩展到 OKX[43] 和 ZenGo[42] 等领先的交易所和钱包提供商,协助他们解决安全漏洞。Skyfall 团队的移动安全研究得到了三星的认可,多个 CVE 证明了这一点,突显了 CertiK 在更广泛的网络安全领域的影响力。
CertiK还致力于在Web3领域提供深入且易于理解的教育内容。通过其博客和各种出版物,CertiK旨在启发行业专家和爱好者,了解区块链技术和网络安全的复杂性和不断发展的动态。
CertiK还发布年度和季度Hack3d报告,其中提供了全面的统计数据和详细的案例研究。这些报告对于理解区块链安全的当前状态至关重要,突出了区块链领域的趋势、漏洞和事件。CertiK的Hack3d报告是开发者、投资者和政策制定者的重要资源,为他们提供可操作的情报和对区块链安全领域挑战和机遇的更深入见解。