Runtime Verification audits the Rewards Contracts of Algorand’s Community Governance

Runtime Verification is thrilled to announce the audit completion of the Rewards Contracts, which are part of Algorand’s Community Governance. The Rewards Contracts are a key component of the newly launched Algorand Community Governance, a new model granting the community voting power and rights to participate in the decision-making process on how the Algorand Ecosystem Resource Pool (AERP) will be utilized and distributed.

A Community Governance Model

Algorand’s Community Governance is a new decentralized model of governance launched last October 1st, 2021. Community Governance allows Algo holders the opportunity to participate in the decision-making process, which involves different matters related to the growth and development of the Algorand ecosystem. Participation is not mandatory, but it’s encouraged with a designated reward pool for the involved individuals in each period.

Each Governor (the designated name for any individual participating in the governance) needs to lock their preferred quantity of Algos for a fixed period of time in order to be granted permission to vote on any open proposal taking place on the designated period. When a period ends, the Algorand Foundation will check off-chain which Governors fulfilled the minimum requirements and who is eligible for rewards.

To be eligible at the end of the period, each Governor must show initiative and vote or delegate their vote to the Algorand Foundation. Inactive Governors, or those who unlocked their Algos in the middle of the period, won’t be eligible for any rewards. Eligible Governors will be able to claim their rewards once the period is over, and will have the chance to join again in the next period.

Rewards’ Contracts Audit Scope

Algorand’s Governance is an intricate model consisting of smart contracts and off-chain flows presented to the public in a simple, easy-to-use platform where anyone can participate without prior technical knowledge.

This audit scope is limited to a key part of the governance model: the Rewards Smart Contracts. As the name implies, these contracts are in charge of the Algo rewards for each period on Algorand’s Community Governance. Let’s take a better look at each contract and its functions to understand the scope and limitations of the audit:

  • The Rewards Application Contract is the first of the two audited contracts. Its main function is to maintain a list of Governors and track their rewards claims. This contract ensures that only eligible Governors can claim the right amount of tokens depending on how much Algo they staked at the beginning of that period.
  • The Stateless Governance Escrow is the second audited smart contract. It’s an escrow account holding the rewards for each period and it’s in charge of verifying payment transactions to eligible Governors to prevent unauthorized payments.

The Rewards Contracts are an essential component and, maintaining their integrity and security is vital for a successful transition towards a decentralized community governance.

Methodology

Runtime Verification team lead Georgy Lukyanov conducted Algorand’s Governance Rewards audit and published a detailed report on September 30th, 2021.

The starting point for the audit consisted of compiling the contracts to TEAL, a low-level language used to write smart contracts and smart signatures in the Algorand blockchain. The smart contracts to be audited were written with PyTeal, a Python language binding for Algorand Smart Contracts. Smart contracts on the Algorand blockchain will always compile to TEAL and that’s the main reason why it was decided to audit the compiled code and look for vulnerabilities in it instead of the high-level source code.

Security audit of compiled code is a laborious process that requires deep analysis of every possible execution scenario. At Runtime Verification, we use formal methods to make our audits as rigorous as possible, even under tight time constraints. We built a formal model of the contracts based on their control-flow graphs and employed the K Framework to analyze all possible execution paths in the compiled TEAL code of the contracts. A series of attack vectors were constructed using modelling and manual code review. Once we had those vectors, they were attempted using different inputs to rule out possible scenarios where an attack could occur.

Results

The audit identified several possible attack scenarios along with a number of informative findings related to the contracts’ design and implementation (see the report for details).

The possible attack scenarios were related to stealing the funds from the rewards escrow, disrupting the operation of the governance contracts, and partially burning the funds of the escrow via fees of the malicious transactions. At the time of writing this blog post, all of these possible attacks have been proved to be impossible or have been addressed and fixed by Algorand’s team.

We would like to highlight the rigorous work conducted by the Algorand team and the dedication put into coding and designing the Rewards Contracts and the new community governance model.

About Algorand Foundation

​​The Algorand Foundation is dedicated to fulfilling the global promise of blockchain technology by leveraging the Algorand protocol and open source software, which was initially designed by Silvio Micali and a team of leading scientists. With core beliefs in the establishment of an open, public and permissionless blockchain, the Algorand Foundation has a vision for an inclusive ecosystem that provides an opportunity for everyone to harness the potential of an equitable and truly borderless economy.

About Runtime Verification

Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services and products to improve the safety, reliability, and correctness of software systems in the blockchain field.

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.