正式验证Hedera Hashgraph的稳定币框架。

Quantstamp Labs
October 28, 2020

Since 2017, over a quarter billion USD worth of digital assets have been lost or stolen due to errors in smart contract development. In order for enterprises to be comfortable leveraging the benefits of stablecoins, rigorous software verification and extensive auditing should be conducted. Quantstamp, the leader in blockchain security, developed a formal specification for stablecoins built on Hedera Hashgraph and deployed using the Hedera Consensus Service, rather than smart contracts or the Hedera Token Service, in order to provide security guarantees for all stablecoins on the platform. 

The formal verification of a specification is one of the most comprehensive ways to ensure software performs as intended. Formal verification is used to secure software whose successful operation keeps people alive and / or is responsible for hundreds of millions of dollars worth of capital. For example, formal verification is used by NASA for code operating space flights as well as in the operation of commercial flights. Stablecoins also need formal verification because the various mechanisms that control them currently manage over 17 billion USD worth of digital assets.

Quantstamp’s experience includes securing over 5 billion USD worth of digital assets and working with over 140 startups, foundations, and enterprises. Quantstamp chose to develop the Hedera Hashgraph stablecoin standard in the K framework because it is robust, extensible, and widely adopted amongst developers. 

The framework shortens development time, provides formal guarantees about the correctness of functions, removes the need to develop new tests, and creates a shared understanding amongst developers concerning the architecture and functionality of implemented stablecoins. When stablecoins follow a secure framework, the framework facilitates the integration of implemented stablecoins into other financial applications. This type of modularity is the ideal environment to encourage the development of a healthy stablecoin ecosystem for enterprises. 

Composability allows developers to create powerful financial applications by allowing smart contracts to easily integrate with one another. While the benefits of composability are clear, when smart contracts integrate with one another, they may inherit vulnerabilities from each other. By standardizing stablecoins built on Hedera Hashgraph, developers considering integrating a stablecoin implementation into their platforms have certain security guarantees that allow them to quickly evaluate the safety of the stablecoin and integrate the stablecoin into their platform.  

Background

Developers and organizations have multiple ways to approach smart contract scaling to build decentralized applications with the trust of a public network, and the privacy and controls of a permissioned network using the Hedera Consensus Service. Previously Hedera discussed ways to explore tokenized assets on Hedera, including mapping an erc20 token to HCS. 

In this blog we’ll be applying this logic to an update in the Hedera Stablecoin Github repo. Hedera partnered with Quantstamp to build an HCS-based stablecoin demo application and associated Formal Model to accelerate time to value for stablecoin issuers.

Motivation

Hedera and its ecosystem partners set out to build an enterprise stablecoin, which could achieve thousands of transactions per second with low latency and ABFT security. The stablecoin codified a set of roles and behaviors including supply management, regulatory compliance, and decentralized access in line with enterprise and consumer scale requirements.

A stablecoin is a type of digital token that is pegged to the value of another asset. The asset can be a fiat currency, a cryptocurrency, a basket of fiat or cryptocurrencies, or any other asset. The peg can be maintained via off-chain collateral holding or algorithmic methods to control token and collateral supply. 

Stablecoins present a compelling opportunity for consumers and businesses to access and use a digital token which provides price protection compared to tokens which may fluctuate in value. It can also operate with low fees, low latency, and high performance when built on Hedera. This opens opportunities for use in retail, B2B, and cross-border payments as well as a new industry of Decentralized Finance (DeFi).

Stablecoins can be extended to enable issuer based discount networks, peer-to-peer payments, retailer based onramps and offramps, similar to cashback for debit transactions, as well as programmable payments based on digitally recognized events. 


Approach

Hedera and its ecosystem partners began with a specification, based on the Interwork Alliance (IWA) Token Taxonomy Framework (TTF), and incorporated enterprise requirements that focus on compliance. 

By using the TTF, Hedera begins with a strong definition that classifies tokens by characteristics 

and defines their properties as well as behaviours in a way that allows tokens to be understood and designed in common language. This gives a token the ability to be constructed across Blockchain/DLT networks, which may be desirable in a case where interoperability is a requirement, as we showed in this demonstration

The specification was then formally verified for correctness, as well as audited by Quantstamp. This level of rigor enables issuers using the specification, formal verification, and audit to insure the security of the stablecoin and avoid costly errors that lead to hacks or locking of funds. 

Hedera then developed a front end user interface showing both how a consumer would interact with the stablecoin and a stablecoin issuer could manage their network. We deployed the front end along with the audited stablecoin implementation to verify the performance of the stablecoin implementation at scale. Hedera achieved over 2,700 tps with low latency over long test runs at multiple points.

The token implementation, front-end, formal model, and audit report are all open sourced in our Github repo for you to try out yourself.

Implementation

We defined a set of key roles necessary to deliver a decentralized and compliant stablecoin. These roles included: 

These stakeholders form the core actors in the stablecoin network as the; administrator, token holder, compliance, supply, and enforcement. 


These roles all are represented in the token contract written in Java and running on a token node, which receives token messages from an HCS topic, validates the message, and mutates the state according to the logic of the IWA specification. 

As shown in the software design description, the architecture also includes:


Building Safer Financial Applications

The power of financial applications using blockchain technology is their ability to easily integrate with one another: however, without standardizing processes such as the implementation of stablecoins, financial applications using blockchain technology face higher security risks. While enterprises are aware of the potential of blockchain technology, security issues have kept them on the sidelines.  

By creating stablecoins through the Hedera Hashgraph framework, developers seeking to integrate Hedera Hashgraph stablecoins into their platforms have specific security guarantees that reduce complexity and create a predictable environment. For enterprises, this means it is easier for them to create safe and compliant stablecoins and easier for partners to safely incorporate their stablecoin into their own platforms. 


About Hedera

Hedera is a decentralized public network on which developers can build secure, fair applications with near real-time finality. The platform is owned and governed by a council of the world's leading organizations including Avery Dennison, Boeing, Deutsche Telekom, DLA Piper, FIS (WorldPay), Google, IBM, LG Electronics, Magalu, Nomura, Swirlds, Tata Communications, University College London (UCL), Wipro, and Zain Group.

For more information, visit www.hedera.com, or follow us on Twitter at @hashgraph, Telegram at t.me/hederahashgraph, or Discord at www.hedera.com/discord. The Hedera whitepaper can be found at www.hedera.com/papers.


About Quantstamp

Quantstamp is the leader in blockchain security, having performed over 140 audits and secured over $5 billion of value. Our mission is to facilitate the mainstream adoption of blockchain technology through our security services. Quantstamp services include securing Layer 1 blockchains such as Ethereum 2.0 and Avalanche, securing smart contract powered applications such as Curve and Idle Finance, and formally verifying financial blockchain primitives. Enterprise companies and NGOs such as Siemens, Toyota, and World Economic Forum also trust Quantstamp to secure their blockchain ecosystems. 

Quantstamp 实验室
2020年10月28日

自2017年以来,由于智能合约开发的错误,已经有价值超过25亿美元的数字资产丢失或被盗。为了让企业能够自如地利用稳定币的优势,应该进行严格的软件验证和广泛的审计。Quantstamp ,区块链安全领域的领导者,为建立在Hedera Hashgraph上的稳定币制定了正式的规范,并使用Hedera共识服务,而不是智能合约或Hedera代币服务进行部署,以便为平台上的所有稳定币提供安全保障。 

规范的形式化验证是确保软件按预期运行的最全面的方法之一。形式核查用于确保软件的安全,因为软件的成功运行使人们得以生存,并且/或者负责价值数亿美元的资本。例如,形式化验证被NASA用于操作太空飞行的代码以及商业飞行的操作。稳定币也需要形式化验证,因为控制稳定币的各种机制目前管理着价值超过170亿美元的数字资产。

Quantstamp的经验包括确保价值超过50亿美元的数字资产,并与140多家初创公司、基金会和企业合作。Quantstamp 选择在K框架中开发Hedera Hashgraph稳定币标准,是因为它是稳健的、可扩展的,并在开发人员中被广泛采用。

该框架缩短了开发时间,提供了关于函数正确性的形式化保证,消除了开发新测试的需要,并在开发人员之间建立了关于已实现稳定币的架构和功能的共同理解。当稳定币遵循一个安全框架时,该框架有利于将已实现的稳定币集成到其他金融应用中。这种类型的模块化是鼓励企业发展健康稳定币生态系统的理想环境。 

可组合性允许开发人员通过让智能合约轻松地相互集成来创建强大的金融应用。虽然可组合性的好处显而易见,但当智能合约相互集成时,它们可能会相互继承漏洞。通过对建立在Hedera Hashgraph上的稳定币进行标准化,考虑将稳定币实现集成到其平台中的开发者有了一定的安全保障,可以快速评估稳定币的安全性,并将稳定币集成到其平台中。  

背景资料

开发者和组织有多种方法来接近智能合约的扩展,以建立去中心化的应用程序,并使用Hedera共识服务的公共网络的信任,以及许可网络的隐私和控制。之前Hedera讨论了在Hedera上探索代币化资产的方法,包括将erc20代币映射到HCS。

在本篇博客中,我们将把这个逻辑应用到Hedera稳定币Github repo的更新中。Hedera与Quantstamp 合作,构建了一个基于HCS的稳定币演示应用和相关的形式化模型,以加速稳定币发行者的价值时间。

动机

Hedera及其生态系统合作伙伴着手打造一个企业稳定币,它可以实现每秒数千笔交易,且具有低延迟和ABFT安全性。该稳定币根据企业和消费者的规模需求,编纂了一系列角色和行为,包括供应管理、监管合规和去中心化访问。

稳定币是一种与另一种资产价值挂钩的数字代币。该资产可以是一种货币、一种加密货币、一篮子货币或加密货币,或任何其他资产。可以通过链外抵押品持有或算法方法来维持挂钩,以控制代币和抵押品的供应。 

稳定币为消费者和企业提供了一个引人注目的机会,让他们可以访问和使用一种数字代币,与可能会在价值上波动的代币相比,它提供了价格保护。当它建立在Hedera上时,它还可以以低费用、低延迟和高性能的方式运行。这为零售、B2B、跨境支付以及去中心化金融(DeFi)新行业的使用提供了机会。

稳定币可以扩展到实现基于发行人的折扣网络、点对点支付、基于零售商的onramps和offramps,类似于借记交易的现金回馈,以及基于数字识别事件的可编程支付。 


办法

Hedera及其生态系统合作伙伴从规范入手,基于Interwork联盟(IWA)的代币分类框架(TTF),并纳入了注重合规性的企业需求。

通过使用TTF,Hedera首先给出了一个强有力的定义,按照特征对代币进行分类。 

并定义了它们的属性以及行为,使代币可以用通用语言来理解和设计。这使得代币有能力在区块链/DLT网络中构建,这在要求互操作性的情况下可能是可取的,正如我们在这次演示中所展示的那样。

然后,该规范被正式验证为正确性,以及由Quantstamp.进行审计。这种严格程度使使用规范、正式验证和审计的发行者能够保证稳定币的安全性,避免代价高昂的错误导致黑客攻击或资金锁定。

然后,Hedera开发了一个前端用户界面,展示了消费者如何与稳定币互动,以及稳定币发行商如何管理他们的网络。我们将前端与经过审核的稳定币实现一起部署,以验证稳定币实现的大规模性能。Hedera在多点的长时间测试运行中,实现了超过2700 tps的低延迟。

代币实现、前端、正式模型和审计报告都是。 在我们的Github repo中开源。让你自己去尝试。

执行情况

我们定义了一套提供去中心化和合规的稳定币所必需的关键角色。这些角色包括: 

这些利益相关者构成了稳定币网络中的 核心角色,作为;管理员、代币持有者、合规、供应和执行。 


这些角色都用Java编写的令牌合约来表示,并在令牌节点上运行,令牌节点接收来自HCS主题的令牌消息,验证消息,并根据IWA规范的逻辑进行状态突变。 

软件设计说明中所示,该架构还包括。


构建更安全的金融应用

使用区块链技术的金融应用的强大之处在于它们能够轻松地相互整合:然而,如果没有标准化的流程,如稳定币的实施,使用区块链技术的金融应用就会面临较高的安全风险。虽然企业已经意识到区块链技术的潜力,但安全问题却让他们一直处于观望状态。  

通过Hedera Hashgraph框架创建稳定币,寻求将Hedera Hashgraph稳定币整合到其平台中的开发人员拥有特定的安全保障,从而降低了复杂性并创造了一个可预测的环境。对于企业来说,这意味着他们更容易创建安全、合规的稳定币,合作伙伴也更容易将其稳定币安全地纳入自己的平台。 


关于Hedera

Hedera是一个去中心化的公共网络,开发者可以在这个网络上以近乎实时的终局性构建安全、公平的应用。该平台由全球领先组织的理事会拥有和管理,包括艾利丹尼森、波音、德国电信、DLA Piper、FIS(WorldPay)、谷歌、IBM、LG电子、Magalu、野村、Swirlds、塔塔通信、伦敦大学学院(UCL)、Wipro和Zain集团。

更多信息,请访问www.hedera.com,或在Twitter上关注我们@hashgraph,在Telegram上关注t.me/hederahashgraph,或在Discord上关注www.hedera.com/discord。Hedera白皮书可在www.hedera.com/papers。


关于况思探

Quantstamp是区块链安全领域的领导者,已进行了140多次审计,并确保了超过50亿美元的价值。我们的使命是通过我们的安全服务促进区块链技术的主流应用。Quantstamp 服务包括确保第一层区块链(如Ethereum 2.0和Avalanche)的安全,确保智能合约驱动的应用(如Curve和Idle Finance)的安全,以及正式验证金融区块链基元。西门子、丰田和世界经济论坛等企业公司和非政府组织也信任Quantstamp ,以确保其区块链生态系统的安全。

第二层解决方案正在扩大区块链技术的规模
了解更多
November 11, 2020

Quantstamp Community Update - October 2020

‍Audit of Ethereum 2.0 client Teku, blockchain insurance, Open DeFi, virtual events, and more media coverage... here’s what happened at Quantstamp in October.‍

November 5, 2020

Why Bitcoin is Capturing Enterprise Attention

MicroStrategy made headlines this summer as the first publicly-traded company to buy Bitcoin as part of its capital allocation strategy. Since then, other companies have followed suit. Learn how current economic conditions and the unique properties of Bitcoin have driven these decisions.

October 27, 2020

Quantstamp Completes Audit of 2nd ETH 2.0 Implementation

Quantstamp has now completed its audit of Teku, the Ethereum 2.0 client developed by ConsenSys. Quantstamp also audited Prysm by Prysmatic Labs.

October 20, 2020

The Status of Insurance in the Blockchain Industry

Audits do not eliminate the possibility of bugs in code. Learn how insurance can be used to mitigate this risk.