# Exploring Leo: A Primer on Aleo Program Security

- **Authors**: Suneal Gong
- **Date**: August 07, 2024
- **Tags**: security, zk, audit, aleo

Aleo is a blockchain platform that utilizes zero-knowledge cryptography to enable private and scalable decentralized applications. Central to Aleo is Leo, a high-level programming language tailored for developing private applications. Leo allows developers to focus on creating applications with strong privacy without needing to consider the intricacies of zero-knowledge proofs.

Understanding and utilizing the unique features of Leo is essential for developers aiming to build robust and secure solutions. This article provides a brief introduction to Leo, with a focus on its security features and practical tips for developers. It aims to help developers understand how to leverage Leo's capabilities to write more secure programs on Aleo. All the programs in this article are written in Leo version 2.1.0.

## Leo Language Basics

Leo is a statically typed language with similar syntax to Rust. Below is an example program that would give you a first impression on Leo language:

```rust
program example_program1.aleo {

    mapping data_map: address => u8;

    // transition is executed off-chain
    async transition save_sum(private a: u8, private b: u8) -> (u8, Future) {
        let sum: u8 = a + b;
        return (sum, finalize_save_sum(self.caller, sum));
    }

    // finalize is executed on-chain
    async function finalize_save_sum(caller: address, sum: u8) {
        data_map.set(caller, sum);
    }
}
```

The syntax of Leo is quite straightforward. In the `example_program1.aleo` program above, it defines a map `data_map` that stores key as `address` type and value as `u8` type. In the `save_sum` transition, it takes two inputs, calculates the sum and passes it to `finalize_save_sum` function. Then, in the `finalize_save_sum` function, it sets the sum value to the `data_map` under the key of the caller address.

The unique part of Leo is that it separates `transition` and `function`. The `transition` is executed off-chain with privacy. The correctness of the execution is proved by a zero-knowledge proof and verified by the network. All the inputs (`a` and `b`) and the intermediate variables are hidden by default. The `function` is executed publicly on-chain so that it can read and write the public state on-chain.

## Record Model

As the `transition` can only be executed off-chain, it cannot touch on-chain states. Instead, it can create and consume `Record` that encapsulate the state and data of a contract. The `Record` is a special struct that represents UTXO data model on Aleo. A `Record` can have self-defined fields. The private fields are encrypted and stored on the ledger. Only the creator and owner are able to decrypt the private fields. A `transition` can create a record by outputting it and consume a record by inputting it.

```rust
program example_program2.aleo {

    record Token {
        owner: address,
        amount: u128
    }

    transition private_transfer_token(private receiver: address, private token: Token) -> Token {
        let new_token: Token = Token {
            owner: receiver,
            amount: token.amount
        };
        return new_token;
    }
}

```

In the code above, it defines a record called `Token` with `owner` and `amount` fields. The `private_transfer_token` transition takes `Token` record as input, consumes it, and outputs a new token with the same amount and a new owner. All the fields in the `Token` record are private by default. As `private_transfer_token` is executed off-chain and the input and output is private, others won't know the sender, receiver, and amount.

## Potential Vulnerabilities of Aleo Program

Aleo provides simple and powerful primitives for building private applications. Nonetheless, it may introduce unintuitive behavior and vulnerabilities without caution. In this section we look at the coding patterns and potential vulnerabilities of Aleo program.

### Underflow and Overflow

For integer types (e.g., `i8` and`u8`), underflow and overflow will always be caught in Leo. In a `transition`, the prover won't be able to create a proof if underflow or overflow happens. In a `function`, the whole transaction will be reverted if that happens.

For example, in the previous `example_program1.aleo` program, it will panic if we run the `save_sum` with `128u8` and `128u8`.

```sh
$ leo run save_sum 128u8 128u8
       Leo ✅ Compiled 'example_program1.aleo' into Aleo instructions

Failed constraint at :
        (256 * 1) != 0
Error [ECLI0377012]: Failed to execute the `run` command.
Error: 'example_program1.aleo/save_sum' is not satisfied on the given inputs (14652 constraints).
```

Also, an impossible cast will cause panic:

```rust
    // input a as 256 will panic because it cannot cast
    transition cast_number(private a: u32) -> u8 {
        return a as u8;
    }
```

For `field` type, there won't be underflow and overflow because it is modular arithmetic.

```rust
program example_program3.aleo {
    transition sub_field(private a: field, private b: field) -> field {
        return a - b;
    }
}
```

Run the program above with `sub_field(0field,1field)` will get the modulo result:

```sh
$ leo run sub_field 0field 1field
       Leo ✅ Compiled 'example_program3.aleo' into Aleo instructions

⛓  Constraints

 •  'example_program3.aleo/sub_field' - 0 constraints (called 1 time)

➡️  Output

 • 8444461749428370424248824938781546531375899335154063827935233455917409239040field

       Leo ✅ Finished 'example_program3.aleo/sub_field'
```

### Program Initialization

Leo does not provide a default function to initialize a program after deployment (like `constructor` function in Solidity). This means the developer need to provide the initialize function on their own. It is crucial that the initialization function is properly guarded to prevent unauthorized call or repeated call.

In the program below, the `initialize` can be repeatedly called. Then anyone can call the function to set themselves as admin and then successfully call `mint` function.

```rust
program example_program4.aleo {
    const ADMIN_KEY: u8 = 0u8;
    mapping admin: u8 => address;

    // This is NOT safe!
    async transition initialize() -> Future {
        return finalize_initialize(self.caller);
    }

    async function finalize_initialize(caller: address) {
        admin.set(ADMIN_KEY, caller);
    }

    async transition mint() -> Future {
        return finalize_mint(self.caller);
    }

    async function finalize_mint(caller: address) {
        let current_admin: address = admin.get(ADMIN_KEY);
        assert(current_admin == caller);
        // mint token
    }  
}
```

### Record Can Only Be Consumed by The Program Defines It

In an Aleo program, a `Record` can be defined in program A and passed into program B. However, it is restricted that the `Record` can only be created or consumed by the program that defines it (i.e., program A).

For example, if we want to implement a program that burns a credits record and issues a certificate, the following program will not burn the credit record.

```rust
import credits.aleo;

program example_program5.aleo {
    record BurnerCertificate {
        owner: address,
        amount: u64
    }

    // credit won't be consumed in this transition
    transition burn(credit: credits.aleo/credits) -> BurnerCertificate {
        let certificate: BurnerCertificate = BurnerCertificate {
            owner: credit.owner,
            amount: credit.microcredits
        };
        return certificate;
    }
}
```

The `burn` transition takes `credits.aleo/credits` as input. However, the credit won't be consumed in the transition because it is not defined in the current program (i.e., the credit is an external record).

The right way is to call a function in `credits.aleo` to burn the credit:

```rust
    transition burn(credit: credits.aleo/credits) -> BurnerCertificate {
        let certificate: BurnerCertificate = BurnerCertificate {
            owner: credit.owner,
            amount: credit.microcredits
        };
        // call `credits.aleo/transfer_private` to burn credit
        credits.aleo/transfer_private(credit, ZERO_ADDRESS, credit.microcredits);
        return certificate;
    }
```

In the code above, the `credit` record is passed into `credits.aleo/transfer_private`. The record will be burned because the record and function are defined in the same program.

### Record Transferred to Program Will be Lost

When a `Record` is created, its private fields are encrypted using the owner's address secret key. When the owner consumes the `Record`, it needs to be authorized using the owner's private key. As a program doesn't have a private key, it's impossible for it to consume a `Record`. This means that any `Record` transferred to a program will be lost.

The developer should handle this carefully to ensure that the record won't be sent to a program. Currently, there is no direct way to tell if an address is a program address except that it requires the owner to be `self.signer`.

### Leak Information in Function

In an Aleo program, `function` is executed on-chain and is totally public. The developer should be cautious about what is passed to the `function`.

The code below is an example that may leak information about the `Record`:

```rust
program example_program6.aleo {
    record Token {
        owner: address,
        amount: u128,
        expire_at: u32
    }

    async transition transfer(private receiver: address, private token: Token) -> (Token, Future) {
        let new_token: Token = Token {
            owner: receiver,
            amount: token.amount,
            expire_at: token.expire_at
        };
        return (new_token, finalize_transfer(token.expire_at));
    }

    // It may leak information because the `expire_at` field is public.
    async function finalize_transfer(expire_at: u32) {
        assert(expire_at > block.height);
    }
}
```

In the `transfer` transition, it will pass the `expire_at` field of the `Token` into the `finalize_transfer` function. If some records have distinct `expire_at` values, others will be able to reason about which `Token` is being transferred.

One way to mitigate this issue is to avoid passing the exact `expire_at` field to the function. Instead, we can input an intermediate value `intermediate_height` and make sure `intermediate_height &lt; height` and `token.expire_at &lt;= intermediate_height` in the transition:

```rust
program example_program6.aleo {
    record Token {
        owner: address,
        amount: u128,
        expire_at: u32
    }

    async transition transfer(private receiver: address, private token: Token, intermediate_height: u32) -> (Token, Future) {
        assert(token.expire_at >= intermediate_height);
        let new_token: Token = Token {
            owner: receiver,
            amount: token.amount,
            expire_at: token.expire_at
        };
        return (new_token, finalize_transfer(intermediate_height));
    }

    // Only compare the `intermediate_height` in the public function
    async function finalize_transfer(intermediate_height: u32) {
        assert(intermediate_height > block.height);
    }
}
```

### The Ternary Conditional Operator Will Evaluate Both Sides

Leo supports the ternary conditional operator. However, the conditional will evaluate both sides. Consider the following code to calculate the absolute value of sub:

```rust
program example_program7.aleo {
    transition abs_sub(private a: u32, private b: u32) -> u32 {
        return a > b ? a - b : b - a;
    }
}
```

This function will always panic when `a != b`. This is because both `a - b` and `b - a` will be evaluated and one of them will underflow:

```sh
$ leo run abs_sub 2u32 1u32
       Leo ✅ Compiled 'example_program7.aleo' into Aleo instructions

Failed constraint at :
        (0 * 1) != 1
Error [ECLI0377012]: Failed to execute the `run` command.
Error: 'example_program7.aleo/abs_sub' is not satisfied on the given inputs (13834 constraints).
```

To avoid the underflow, we can cast the unsigned integer to a signed integer. Then, cast the result back to unsigned integer:

```rust
    transition abs_sub(private a: u32, private b: u32) -> u32 {
        // use i64 to ensure a successful cast
        let ai: i64 = a as i64;
        let bi: i64 = b as i64;
        let ci: i64 = ai > bi ? ai - bi : bi - ai;
        return ci as u32;
    }
```

### Program Identified by Name Might Cause Issues

In Aleo, a program is identified by its program name, regardless of the program content. A program imports another program by name. This means the developer should verify the program manually after deploying it.

For example, suppose you want to deploy a multisig program (let's say `my_secure_multisig.aleo`) to hold your funds. The usual steps are first deploying the `my_secure_multisig.aleo` program and then sending funds to the program by name. However, the attacker may be able to front-run your deployment and deploy a program with the same name but totally different content. Then the `my_secure_multisig.aleo` program will be controlled by the attacker. You will immediately lose all the funds once you send them.

Another example is about program import. Suppose that you have two programs: `programA.aleo` and `programB.aleo`. `programA.aleo` imports `programB.aleo`. You need to first deploy `programB.aleo` and then deploy `programA.aleo`. It is possible that an attacker front-run to deploy a fake `programB.aleo` before your transaction. Then your `programA.aleo` will import the fake `programB.aleo`. This will make the whole program unsafe.

To avoid such attacks, we recommend always verifying if the program is deployed by you after your deployment transaction.

## Conclusion

As a new blockchain platform, Aleo provides simple yet powerful primitives for building private applications. Nevertheless, these new primitives may introduce unintuitive behavior and vulnerabilities without caution. In this article, we discussed the potential vulnerabilities of Aleo programs. As Aleo evolves, we will keep an eye on its developments and continue to provide insights on maintaining security in this innovative space.

---

This article was published on the [ZK/SEC Quarterly](https://blog.zksecurity.xyz) blog by [ZK Security](https://www.zksecurity.xyz), a leading security firm specialized in zero-knowledge proofs, MPC, FHE, and advanced cryptography. ZK Security has audited some of the most critical ZK systems in production, discovered vulnerabilities in major protocols including Aleo, Solana, and Halo2, and built open-source tools like [Clean](https://github.com/Verified-zkEVM/clean) for formally verified ZK circuits. For more articles, see the [full list of posts](https://blog.zksecurity.xyz/llms.txt).
