Microsoft Azure推出用于验证基于以太网的Solidity智能合约的开源工具

 
 
据悉，智能合约审计与常规代码审计基本相同 – 在代码公开部署之前，它会仔细调查代码以查找安全漏洞和漏洞。这就像在向公众开放之前测试一座桥梁。在这两种情况下，建筑商都要对其产品的安全性和安全性负责。
Azure是Microsoft创建的云计算服务，用于通过Microsoft管理的数据中心构建，测试，部署和管理应用程序和服务。宣布该产品的博客说：
“为了加强Azure Blockchain中的智能合约，该团队找到了Microsoft Research研究人员的合作伙伴，致力于确保软件程序正确性的先进技术。此次合作产生了VeriSol，这是一种由研究人员开发的全新的开源形式验证工具。 VeriSol是Verifier for Solidity的缩写 – 开发人员可以开始表达在流行的Solidity语言的子集中编写的智能合约的理想行为，然后使用数学逻辑机制严格检查这些规范与实现。“
使用VeriSol，开发人员可以开始以之前不可行的方式指定和证明其工作的安全性。更传统的测试依赖于开发人员准确预测产品如何使用的能力，这种练习涉及一些被忽视的角落案例，因为人类只能想到这么多不同的逻辑测试案例。但是，形式验证会自动识别代码可能违反给定不变量的不同方式，包括开发人员无法预测的情况。
微软首席研究员Shuvendu Lahiri说：
“我们设想不仅能够为Azure区块链开发人员和客户提供支持，还能为完整的区块链生态系统做出贡献，这种生态系统更安全，帮助人们充分发挥技术的潜力，而不会受到智能合同中代价高昂的错误的困扰。”