Details on Formal Verification

Any call of the form `transfer(recipient, amount)` must fail if the recipient address is the zero address.

ERC-20

We verified properties of the public interface of those token contracts that implement the ERC-20 interface. This covers
* Functions `transfer` and `transferFrom` that are widely used for token transfers,
* functions `approve` and `allowance` that enable the owner of an account to delegate a certain subset of her tokens to another account (i.e. to grant an allowance), and
* the functions `balanceOf` and `totalSupply`, which are verified to correctly reflect the internal state of the contract.

The properties that were considered within the scope of this audit are as follows:

`transfer` Prevents Transfers to the Zero Address

All non-reverting invocations of `transfer(recipient, amount)` that return `true` must subtract the value in `amount` from the balance of `msg.sender` and add the same value to the balance of the `recipient` address.

`transfer` Transfers the Correct Amount in Non-self Transfers

All self-transfers, i.e. invocations of the form `transfer(recipient, amount)` where the `recipient` address equals the address in `msg.sender` must succeed and return `true` if
* the value in `amount` does not exceed the balance of `msg.sender` and
* the supplied gas suffices to complete the call.

`transfer` Succeeds on Admissible Self Transfers

All invocations of the form `transfer(recipient, amount)` must succeed and return `true` if
* the `recipient` address is not the zero address,
* `amount` does not exceed the balance of address `msg.sender`,
* transferring `amount` to the `recipient` address does not lead to an overflow of the recipient's balance, and
* the supplied gas suffices to complete the call.

`transfer` Succeeds on Admissible Non-self Transfers

All non-reverting invocations of `transfer(recipient, amount)` that return `true` and where the `recipient` address equals `msg.sender` (i.e. self-transfers) must not change the balance of address `msg.sender`.

`transfer` Transfers the Correct Amount in Self Transfers

All non-reverting invocations of `transfer(recipient, amount)` that return `true` must only modify the balance entries of the `msg.sender` and the `recipient` addresses.

`transfer` Has No Unexpected State Changes

Any transfer of an amount of tokens that exceeds the balance of `msg.sender` must fail.

`transfer` Fails if Requested Amount Exceeds Available Balance

Any invocation of `transfer(recipient, amount)` must fail if it causes the balance of the `recipient` address to overflow.

`transfer` Prevents Overflows in the Recipient's Balance

If the `transfer` function in contract `ERC20` fails by returning `false`, it must undo all state changes it incurred before returning to the caller.

If `transfer` Returns `false`, the Contract State Is Not Changed

The transfer function must never return `false` to signal a failure.

`transfer` Never Returns `false`

All calls of the form `transferFrom(from, dest, amount)` where the `from` address is zero, must fail.

`transferFrom` Fails for Transfers From the Zero Address

All calls of the form `transferFrom(from, dest, amount)` where the `dest` address is zero, must fail.

`transferFrom` Fails for Transfers To the Zero Address

All invocations of `transferFrom(from, dest, amount)` that succeed and that return `true` subtract the value in `amount` from the balance of address `from` and add the same value to the balance of address `dest`.

`transferFrom` Transfers the Correct Amount in Non-self Transfers

All non-reverting invocations of `transferFrom(from, dest, amount)` that return `true` and where the address in `from` equals the address in `dest` (i.e. self-transfers) do not change the balance entry of the `from` address (which equals `dest`).

`transferFrom` Performs Self Transfers Correctly

All invocations of `transferFrom(from, dest, amount)` must succeed and return `true` if
* the value of `amount` does not exceed the balance of address `from`,
* the value of `amount` does not exceed the allowance of `msg.sender` for address `from`,
 * transferring a value of `amount` to the address in `dest` does not lead to an overflow of the recipient's balance, and
* the supplied gas suffices to complete the call.

`transferFrom` Succeeds on Admissible Non-self Transfers

All invocations of `transferFrom(from, dest, amount)` where the `dest` address equals the `from` address (i.e. self-transfers) must succeed and return `true` if:
* The value of `amount` does not exceed the balance of address `from`,
* the value of `amount` does not exceed the allowance of `msg.sender` for address `from`, and
* the supplied gas suffices to complete the call.

`transferFrom` Succeeds on Admissible Self Transfers

Any call of the form `transferFrom(from, dest, amount)` with a value for `amount` that exceeds the balance of address `from` must fail.

`transferFrom` Fails if the Requested Amount Exceeds the Available Balance

All non-reverting invocations of `transferFrom(from, dest, amount)` that return `true` must decrease the allowance for address `msg.sender` over address `from` by the value in `amount`.

`transferFrom` Updated the Allowance Correctly

Any call of the form `transferFrom(from, dest, amount)` with a value for `amount` that exceeds the allowance of address `msg.sender` must fail.

`transferFrom` Fails if the Requested Amount Exceeds the Available Allowance

All non-reverting invocations of `transferFrom(from, dest, amount)` that return `true` may only modify the following state variables:
* The balance entry for the address in `dest`,
* The balance entry for the address in `from`,
* The allowance for the address in `msg.sender` for the address in `from`.

`transferFrom` Has No Unexpected State Changes

The function `totalSupply` must always succeeds, assuming that its execution does not run out of gas.

`totalSupply` Always Succeeds

Any call of `transferFrom(from, dest, amount)` with a value in `amount` whose transfer would cause an overflow of the balance of address `dest` must fail.

`transferFrom` Prevents Overflows in the Recipient's Balance

If `transferFrom` returns `false` to signal a failure, it must undo all incurred state changes before returning to the caller.

If `transferFrom` Returns `false`, the Contract's State Is Unchanged

The `transferFrom` function must never return `false`.

`transferFrom` Never Returns `false`

The `totalSupply` function must return the value that is held in the corresponding state variable of contract ERC20.

`totalSupply` Returns the Value of the Corresponding State Variable

The `totalSupply` function in contract ERC20 must not change any state variables.

`totalSupply` Does Not Change the Contract's State

Function `balanceOf` must always succeed if it does not run out of gas.

`balanceOf` Always Succeeds

Invocations of `balanceOf(owner)` must return the value that is held in the contract's balance mapping for address `owner`.

`balanceOf` Returns the Correct Value

Function `balanceOf` must not change any of the contract's state variables.

`balanceOf` Does Not Change the Contract's State

Function `allowance` must always succeed, assuming that its execution does not run out of gas.

`allowance` Always Succeeds

Invocations of `allowance(owner, spender)` must return the allowance that address `spender` has over tokens held by address `owner`.

`allowance` Returns Correct Value

Function `allowance` must not change any of the contract's state variables.

`allowance` Does Not Change the Contract's State

All calls of the form `approve(spender, amount)` must fail if the address in `spender` is the zero address.

`approve` Prevents Approvals For the Zero Address

All calls of the form `approve(spender, amount)` must succeed, if
* the address in `spender` is not the zero address and
* the execution does not run out of gas.

`approve` Succeeds for Admissible Inputs

All non-reverting calls of the form `approve(spender, amount)` that return `true` must correctly update the allowance mapping according to the address `msg.sender` and the values of `spender` and `amount`.

`approve` Updates the Approval Mapping Correctly

All calls of the form `approve(spender, amount)` must only update the allowance mapping according to the address `msg.sender` and the values of `spender` and `amount` and incur no other state changes.

`approve` Has No Unexpected State Changes

If function `approve` returns `false` to signal a failure, it must undo all state changes that it incurred before returning to the caller.

If `approve` Returns `false`, the Contract's State Is Unchanged

The function `approve` must never returns `false`.

`approve` Never Returns `false`

ERC20

In the following Solidity code snippet, there is a loop intended to iterate through an array of minters and delete specific elements based on a condition. However, the code has a critical flaw that leads to an infinite loop.

```solidity
while (i < minters.length) {
    _minter = minters[i];

    if (!minter[_minter]) {
        minters[i] = minters[minters.length - 1];
        delete minters[minters.length - 1];
        // minters.length--;
    } else {
        i++;
    }
}
```

The issue arises from the use of the `delete` keyword on the last element of the array. While this does reset the value at the specified index to its default value, it does not change the length of the array. As a result, if the last element of the array meets the deletion condition, the loop will continue to iterate over the last element indefinitely, leading to an infinite loop.

Potential Infinite Loop


In the contract `HasMinters` the role `_owner` has authority over the functions shown in the diagram below.
Any compromise to the `_owner` account may allow the hacker to take advantage of this authority and change the configuration of minter.
![](https://accelerator-tasks-prod.acc.corp.certik.com/11ee-3ea1-b83434f0-b86c-c1381b4571cc/diagrams/centralization_IAISocietyToken-HasMinters-_owner.svg)

In the contract `IAISocietyToken` the role `minter` has authority over the functions shown in the diagram below.
Any compromise to the `minter` account may allow the hacker to take advantage of this authority and mint current tokens.
![](https://accelerator-tasks-prod.acc.corp.certik.com/11ee-3ea1-b83434f0-b86c-c1381b4571cc/diagrams/centralization_IAISocietyToken-IAISocietyToken-minter.svg)


In the contract `IAISocietyToken` the role `_owner` has authority over the functions shown in the diagram below.
Any compromise to the `_owner` account may allow the hacker to take advantage of this authority, change the `_maxSupply` and prevent the token transfer.
![](https://accelerator-tasks-prod.acc.corp.certik.com/11ee-3ea1-b83434f0-b86c-c1381b4571cc/diagrams/centralization_IAISocietyToken-IAISocietyToken-_owner.svg)

In the contract `Ownable` the role `_owner` has authority over the functions shown in the diagram below.
Any compromise to the `_owner` account may allow the hacker to take advantage of this authority and change the ownership.
![](https://accelerator-tasks-prod.acc.corp.certik.com/11ee-3ea1-b83434f0-b86c-c1381b4571cc/diagrams/centralization_Ownable-Ownable-_owner.svg)

Centralization Related Risks

All of the `AIS` tokens are sent to the contract deployer or one or several externally-owned account (EOA) addresses. This is a centralization risk because the deployer or the owner(s) of the EOAs can distribute tokens without obtaining the consensus of the community. Any compromise to these addresses may allow a hacker to steal and sell tokens on the market, resulting in severe damage to the project. 

Initial Token Distribution

In the contract `AIS`, the role `_owner` has authority to update the status of the `_paused` and further pause/resume the functionality of the `transfer()` and `transferFrom()` functions.

Any compromise to the private key of the `_owner` may allow hackers to take advantage of this authority and allow/prevent external user access to the sensitive functionalities controlled by the `_paused`.

Pausing Centralization Risks

Reading, initializing, and modifying storage variables cost more gas than operating local variables, and this gas cost can significantly increase when these operations are performed inside a loop.

Reference: https://docs.soliditylang.org/en/latest/introduction-to-smart-contracts.html#storage-memory-and-the-stack


Costly Operation Inside Loop

AI Society - Audit

AIS.sol

Context.sol

ERC20.sol

IAISocietyToken.sol

IERC20.sol

IERC20Metadata.sol

Ownable.sol

Pausable.sol

Top 10% Code Security Score

Top 10% Fundamental Score

https://images.ctfassets.net/jqfm0se0f03r/1Jk3Rm6fdp2CJMqpJLm1cI/e0af9009a4778adcfdc4c58c055e8c76/6459f5e3ef42078172db40d8_ais_logo-p-500.png

In the AI.Society metaverse, users can engage with AI-driven NPCs that offer intelligent assistance in areas like healthcare, legal advice, and education. These NPCs use advanced language processing and machine learning to provide personalized guidance and enhance the user experience within the metaverse.

AI Society

Audit History

Security Assessment

2023/08/22

Solidity

2023/08/25

Skynet

Project Owner?
Activate Today!