> ## Documentation Index
> Fetch the complete documentation index at: https://docs.phylax.systems/llms.txt
> Use this file to discover all available pages before exploring further.

# Vestra DAO Hack

> Unchecked isActive flag in maturity

This case study explains how the Vestra DAO hack worked and which assertion pattern could have constrained the invalid state transition.

## What Happened

In December 2024, VestraDAO was hacked. The hacker exploited a vulnerability in the `unStake` function which allowed users to stake and unstake without waiting for the maturity period.
For an in-depth analysis of the hack, you can read this [post](https://x.com/_czepluch/status/1866112404242743590).

In a nutshell, there was an `isActive` flag that was set to `false` correctly in the `unStake` function. However, the `isActive` flag was never checked if someone called the `unStake` function again.
This resulted in an attacker being able to repeatedly call `unStake` and get additional yield from the protocol until it was drained.

It should be noted that there were no tests for the code base and the code was not audited. However, with an assertion it would be possible to patch the vulnerability until a new version of the code is deployed.
The assertion would simply check if the `isActive` flag is `false` before calling the `unStake` function.

## Why This Matters

In this hack, a simple require statement would have been enough to prevent the vulnerability. Usually, a contract redeployment is needed to fix a vulnerability like this.
With an assertion, it is possible to patch this directly and make sure that all calls to the `unStake` function check the `isActive` flag.

This is a very powerful concept and can be useful in many situations. Imagine a security researcher reports a vulnerability in a protocol before anyone has exploited it.
In that case the protocol can publish an assertion that guards against the vulnerability until the team has had the time to fix the vulnerability in the best way possible.

## Assertion Pattern

This assertions checks if the `isActive` flag is `false` before calling the `unStake` function if it's false the transaction will not be included in the block.
Alternatively, there could be an assertion that checks that the `totalStaked` is always equal to the sum of all `stakeAmount` in the `stakes` mapping.
This would require a way to iterate over all the stakes and sum them up, which is not yet supported by a cheatcode.

```solidity theme={null}
// SPDX-License-Identifier: MIT
pragma solidity 0.8.28;

import {Assertion} from "../lib/credible-std/Assertion.sol";
import {AssertionSpec} from "../lib/credible-std/SpecRecorder.sol";

// VestraDAO interface
interface IVestraDAO {
    struct Stake {
        uint64 startTime;
        uint256 stakeAmount;
        uint256 yield;
        uint256 penalty;
        uint64 endTime;
        bool isActive;
    }

    mapping(address => mapping(uint8 => Stake)) public stakes;

    function unStake(uint8 maturity) external;
}

contract VestraDAOHack is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    IVestraDAO public vestraDAO = IVestraDAO(address(0xbeef));

    function triggers() external view override {
        registerFnCallTrigger(this.assertionExample.selector, vestraDAO.unStake.selector);
    }

    // Check that user was actively staked before unstaking
    // This prevents double-unstaking by ensuring isActive was true before the call
    function assertionExample() external view {
        PhEvm.CallInputs[] memory unStakes = ph.getCallInputs(address(vestraDAO), vestraDAO.unStake.selector);

        for (uint256 i = 0; i < unStakes.length; i++) {
            uint8 maturity = abi.decode(unStakes[i].input, (uint8));
            address from = unStakes[i].caller;

            // Check BEFORE the unstake that the stake was active
            PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: unStakes[i].id});
            (,,,,,bool wasActive) = vestraDAO.stakes(from, maturity);
            require(wasActive, "User was not actively staked for this maturity");
        }
    }
}
```