伦敦金融科技公司Aesthetic Integration为基于区块链智能合约推出形式化验证平台 ...

暴走时评：“形式化验证”分析金融市场算法的安全性和公平性的伦敦金融科技公司Aesthetic Integration，最近宣布推出Imandra Contracts平台，这是世界首个为区块链智能合约进行形式化验证的平台，智能合约背后的代码是Imandra Contracts的一个非常令人兴奋的应用领域。随着主流行业越来越多的参与到区块链技术应用中，需要有安全的协议，来审查这些创造出来的算法的安全性，不然算法设计中的未知错误的代价十分高昂。

翻译：Nicole

伦敦金融科技公司Aesthetic Integration，这是一家用“形式化验证”分析金融市场算法的安全性和公平性的公司，最近宣布推出Imandra Contracts平台，公司称该解决方案是世界首个为区块链智能合约进行形式化验证的平台。

该声明在Devcon2会议上发布，Devcon2也是上海区块链国际周内容的一部分。

Imandra Contracts可以应用到人工智能、数学运算、计算机科学，让电子金融市场和其他行业更加严谨，而这是通过为智能合约的开发和监管提供更好的透明度而达成。

最初供以太坊使用

该新型基于云服务的平台最初是供以太坊使用的，以太坊是一个去中心化的运行智能合约的区块链应用程序平台。

Aesthetic Integration的联合首席执行官兼联合创始人Grant Passmore博士对CCN说：

“Imandra是分析智能合约的工具，可以帮助个人了解他们所做的事情，这样做的原因，以及可能出错的地方。Imandra是由形式化验证最近的进展所驱动，这个领域是计算机科学、数学运算和人工智能的交叉领域，专注于推算出算法的可能行为。”

该平台可以让用户确定及修复金融算法中的异常现象，此外还可以保护用户交易免受负面影响。消费者隐私通过行业的最佳实践（包括虚拟私有云）得到保障。

银行已经在使用Imandra

Passmore 指出，Imandra已经在一些顶级的投资银行中得到应用，用于分析它们的金融算法的安全性和公平性。Aesthetic Integration在2015年度瑞士联合银行金融挑战的未来中获胜，获胜项目是Imandra，它可以分析黑池的监管属性。

他补充说：

“Imandra Contracts首次把这些技术带给区块链智能合约，所有的在云中都是可用的。”

Passmore认为，平台的互操作性是Aesthetic Integration的主要关注焦点。

“我们正在开发可用于多个区块链智能合约平台的Imandra Contracts版本。然而，我们选择从以太坊开始，是因为以太坊虚拟机有详细的说明（如以太坊黄皮书），同时，考虑到最近的活动，以太坊社区强烈意识到形式化验证的重要性。”

该平台允许用户审查合约的设计和算法，包括托管在去中心化智能合约平台和应用程序上的，如以太坊。审查设计和算法可用确保它们满足了议定的规格，并且不会产生不必要的故障。

那DAO漏洞呢？

Passmore说：

“The DAO，使用以太坊区块链的分布式自治组织中出现的漏洞，强调了在金融服务中更加严谨的分析智能合约的迫切需求。我们从DAO中得到的经验教训是显而易见的：智能合约开发必须无限趋于严谨，相比于搭建一个网络一会管用程序，这更像是搭建一个苛求安全的控制算法。”

Imandra Contracts将阻止DAO漏洞出现吗？

Passmore对CCN提出的问题作出了回应：

“这很难说。如果我们把问题变成‘Imandra Contracts本来就可以阻止DAO漏洞的出现吗？’那么答案显然是‘可以’。例如，我们可以把这些译成编码，把DAO漏洞当作Imandra中的验证目标，让Imandra自动检查大量的智能合约，旨在确保这些智能合约不会出现同样的问题。”

金融行业引导智能合约的投资

Grant Passmore

Passmore对金融领域首先投资智能合约并不惊讶。

他说：

“从清算到自动化管理以及结构化产品组合定价，金融领域发现了构建更加稳健、高效和自动化分析的系统架构的需求。衍生物的定价是一个主要问题，如果一家银行所有的数据都运行在智能合约上，三年后，他们会有成千上万的智能合约投资组合。”

Passmore继续说：

“他们要了解他们的风险、计算曝光等等。你无法不去计算智能合约背后的代码，这是Imandra Contracts的一个非常令人兴奋的应用领域，也是我们一直在研究的工作。”

Passmore指出其他苛求安全的行业如硬件制造和航空电子设备，一直都非常依赖形式化验证，因为这可以确保算法的安全。他指出：

“随着主流行业越来越多的参与到区块链技术应用中，需要有安全的协议，来审查这些创造出来的算法。”

此外，Aesthetic Integration已经提供了Imandra Markets和Imandra Venues形式化验证解决方案。Imandra Markets是一个面向用户算法规范的基于云的生态系统，可以简化交易系统的设计、测试和合规流程。

Imandra Venues分析了交易场地的监管属性，在最近发现越来越多的故障和罚款之后，Imandra Venues为实现交易所和黑池的稳定性和透明性，建立了一种新的标准。这些意外事件表明，算法设计中的未知错误的代价是高昂的。

Aesthetic Integration计划推出Imandra Contracts的预售项目，早期的采用者在10月的第一个礼拜可以以折扣价获得该平台的使用权。用户可以用手机设备远程分析并审查智能合约设计。

作者：Elliot Maras | 编译者：Nicole | 来源：Cryptocoinsnews