How records work in Aleo: The foundation of private state in Leo | Smart contract audits from Veridise

How records work in Aleo: The foundation of private state in Leo

Jan 13

| 12 read

This is the first article in our series exploring records in Leo, the programming language of the Aleo Network.

Records in Leo blog series:
📚 Part I: How records work in Aleo? The foundation of private state in Leo
📚 Part II: Common Pitfalls handling records in Aleo – Validations, parity, and privacy (published next week)

How records work in Aleo: The foundation of private state in Leo (1/2)

Aleo is a Layer-1 blockchain for private applications, powered by zero-knowledge proofs (zkSNARKs) and the Leo programming language. It utilizes the record model, akin to the UTXO model, to gain privacy and scalability. In the traditional account model, all of the data for an application or user is tied to an address, which makes activity easy to trace. Even if balances are hidden with commitments, information can still leak through addresses, and shared state becomes a bottleneck for concurrency.

On Aleo, transactions and state have both private and public parts; public data the network verifies directly, and private data whose correctness is proven without revealing its contents. Public state lives in mappings and is visible to everyone, while private state is carried in records. Aleo indexes programs by program IDs, and storing state as records improves privacy and allows many users to update program state in parallel.

What is a record?

On Aleo, a record is the fundamental unit of private state used for encoding user assets and application state. In this model, application state and owner are encrypted and kept on-chain, which allows preserving user privacy while also letting programs read and update their own state.

A record can encode arbitrary application state; think of many small fragments that together describe a user’s balance or an application’s state. Each fragment is a record. Aleo serializes records with fields such as the owner, the program’s data fields, record version, and a nonce.

Record on the Aleo Network:

The record owner is an account address, and specifies the party that is authorized to spend the record. The amount is the application data we are interested in recording and represents the quantity of tokens in the users balance in this specific record. Note that the visibility of the all fields are private, therefore the data will be encrypted and stored on the ledger, and it will not be publicly visible. The record version determines how the record commitment is derived and what privacy features are available, and the _nonce is a unique identifier derived from the owner’s secret key which lets the network mark the record as spent once consumed.

An actual record defined in a Leo program looks very different in practice to a serialized record. The fields _nonce and version are handled by the AleoVM implicitly. Therefore, in the context of a Leo program, the above record would be defined as follows, containing only the owner and amount fields.

Record as defined in Leo

Note that records in Aleo must always possess an owner component, that designates the public key of the address allowed to spend the record. The compiler does not allow creating a record without an owner field. Additionally, records are not limited to just the owner field; they can contain multiple arbitrarily named inputs.

How are records used?

In the record model, state advances by consuming old records and creating new ones. When a record is consumed, the execution reveals a unique serial number, otherwise known as a nullifier, derived from the owner’s secret and the record’s nonce. The network rejects any duplicate serial number, which prevents a record from being used twice.

These changes occur inside transitions. A transition privately proves that the caller owns the input records and that the program’s rules are satisfied, while keeping the private fields hidden. It can also emit new records, and optionally write to public mappings when the application needs public state. Transactions bundle one or more transitions and include a dedicated fee transition. The network permits up to thirty-two transitions per transaction, with one slot reserved for the fee.

When a transition creates a record, it sets the owner and the data fields to be recorded. If that record is later provided as an input, the transition consumes it and may emit one or more new records. Therefore each transition can be viewed as a transformation of inputs into outputs. Hence, records can only be produced within a transition, and they can only be used once.

Whenever a record is provided as input to a transition, the system performs some implicit validations. These include:

  • Validating that the input record’s commitment corresponds to a commitment contained within the ledger.
  • Verifying that the record is being consumed by the right function (i.e the function lies in the same program that produced it).
  • Ensuring that the record’s serial number is unique to prevent double spending.
  • Checking the spender possesses the secret keys for the address in the record’s owner field (confirming authorization to spend the record).

Record consumption in practice

Let’s look at two different examples of record consumption, to understand how records are utilized to maintain application state.

Consider Alice is trying to privately spend a token she owns through a transfer_private() transition. She proves locally that she owns the input record and that it covers the amount, producing a serial number and the two output records. One output returns the change to the sender. The other delivers the transferred amount to the recipient. The serial number produced is disclosed on the ledger to publicly announce that the record has been spent, preventing double-spending while maintaining privacy.

These steps occur privately in the transition function, whereas any public state updates (if any) such as updates to mappings, occur in the program’s finalize() function, which must be invoked so the ledger reflects the changes. Since our operation in question involves a private transfer, no public state updates are made and therefore there is no need to declare or call trigger a corresponding onchain call to finalize(). See the Aleo documentation to learn more about transitions.

transfer_private() consumes the input record and creates two output records.

In contrast, a transfer_priv_to_public() transition moves values from private records to public on-chain state. The sender provides a token record with the specific token amount they want to turn into public tokens. The transition consumes the input, creates a new private record with the remainder for the sender, and increases the receiver’s public balance in finalize(). Although this function preserves privacy for the sender’s record, it publicly reveals the token receiver and the token amount.

transfer_private_to_public consumes a private record, and updates public balance

In conclusion, we examined Aleo’s record model, why it favors records over Ethereum’s account model to improve privacy and scalability, and how records manage private state before being consumed by onchain transitions when they’re spent. Next, we will look at the common pitfalls that tend to surface in Aleo and the checks that can help avoid them.

Author:

Mark Anthony, Security Analyst at Veridise

More by Veridise

Subscribe to our blog

Be the first to get the latest from Veridise — including educational articles on ZK and smart contracts, audit case studies, and updates on our tool development. Delivered twice a month.

smart contract audit cloud

Contact us for a security audit quote

Secure an earlier audit slot by reaching out early.