Move is a smart contract language for manipulating digital assets and was originally designed to be developed from a security perspective. To ensure its security, Move has been designed with a large number of security features at the language level, as described in the previous section. Beosin Audit Service has integrated Move Prover into Move’s auditing service.

The main steps of the Besoin Security Audit Service when auditing a Move contract are as follows.

1. Understand the project architecture, purpose and framework used

2. Smart contract code review and manual walk-through to find logical vulnerabilities

3. Thorough investigation of vulnerabilities related to mathematical operations

4. Test coverage review (aptos move test)

5. On-chain testing of core functionality (aptos-cli)

6. Deployment of smart contracts (aptos devnet)

7. Formal verification of core code (move prover)

Install

Application

1. Permission Control

Enforcing explicit access control policies at the specification level can effectively prevent privilege abuse.

For example, in std::offer, we can see that the function is terminated when the recipient is not in the whitelist.

2. Invariants of the Data

Formal validation provides the best environment to verify that certain variables or resources do not exceed the expected bounds. For example, the following example ensures that the balance of (target) does not exceed MAX_BALANCE.

We can even write a global data invariant to guarantee that balance does not exceed MAX_BALANCE anywhere in the program.

invariant forall a: address where exists<Account>(a):

balance(a) <= MAX_BALANCE;

3. Fund Conservation

Verifying fund conservation can ensure security in complex Defi protocols. For example, in an exchange via AMM, if the funds of one side of the pool do not increase, the other side cannot decrease. This means that there is no “free” money. An example is shown below.

Other fund conservation includes debit and credit agreements should always be fully collateralized after a series of deposit, borrowing and withdrawal instructions; order books should not have book changes when an order is placed and then cancelled, etc.

Move is still in the development stage and the Move ecosystem is still some distance away from maturity. Move-related developers are inexperienced and not many of them are really skilled in developing Move contracts, so they are more prone to some business-level vulnerabilities. This requires developers to be more proficient in the design and development of Move contracts, and in the features of the Move language and business, in order to reduce the number of security vulnerabilities.

In the next article, we will introduce the vulnerability points and examples that tend to appear in the audit of Move programs.

Contact

If you have need any blockchain security services, please contact us:

Website Email Official Twitter Alert Telegram LinkedIn