Formally Verifying Hedera Hashgraph's Stablecoin Framework

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 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. 

Layer 2 solutions are scaling blockchain technology
Learn more
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.