Formal Verification

Formal Verification of Lighting Cat

Salus Lighting Cat tool utilizes formal verification for smart contract vulnerability detection. It performs formal verification on the bytecode of smart contracts. By carefully inspecting the bytecode, the Lighting Cat tool ensures accuracy of behavior, correctness of interactions, and consistency of execution flows. This approach allows it to identify potential errors or vulnerabilities easier. Compared to other static analysis tools, Lighting Cat offers higher accuracy and lower false positive rates.

The Lighting Cat tool can detect a variety of smart contract security vulnerabilities, including but not limited to these.

Analyzing Formal Verification Results

The following example will use the contract with the address 0xc916f4cf156b0bf2681272Ec597b6aE31B739199 from ethereum-sepolia. The Lightning Cat tool will be used to perform formal verification on this contract. The diagram below shows that 7 vulnerabilities have been detected, which have been categorized into five severity levels: High Severity, Medium Severity, Low Severity, Informational, and Optimization. The corresponding number of vulnerabilities for each severity level is 1, 0, 4, 2, 0.

Here's a breakdown of the severity levels as described:

● High Severity: The issue puts a large number of users’ sensitive information at risk, or is reasonably likely to lead to catastrophic impact for clients’ reputations or serious financial implications for clients and users.

● Medium Severity: The issue puts a subset of users’ sensitive information at risk, would be detrimental to the client’s reputation if exploited, or is reasonably likely to lead to a moderate financial impact.

● Low Severity: The risk is relatively small and could not be exploited on a recurring basis, or is a risk that the client has indicated is low impact in view of the client’s business circumstances.

● Informational: The risk is relatively small and could not be exploited on a recurring basis, or is a risk that the client has indicated is low impact in view of the client’s business circumstances.

● Optimization: This category doesn't necessarily imply vulnerabilities. It refers to issues or suggestions related to contract performance and resource utilization. These recommendations aim to improve the efficiency and performance of the contract.

Let's take one of the vulnerabilities as an example to explain the formal verification detection results of Lightning Cat:

Vulnerability: Reentrancy

Vulnerability Category: High.

Vulnerability Description: One of the major dangers of calling external contracts is that they can take over the control flow. In the reentrancy attack (a.k.a. recursive call attack), a malicious contract calls back into the calling contract before the first invocation of the function is finished. This may cause the different invocations of the function to interact in undesirable ways.

Recommendation: The best practices to avoid Reentrancy weaknesses are: - Make sure all internal state changes are performed before the call is executed. This is known as the [Checks-Effects-Interactions pattern](https://solidity.readthedocs.io/en/latest/security-considerations.html#use-the-checks-effects-interactions-pattern) - Use a reentrancy lock (ie. [OpenZeppelin's ReentrancyGuard](https://github.com/OpenZeppelin/openzeppelin-contracts/blob/master/contracts/utils/ReentrancyGuard.sol).

Contract file containing the vulnerability：This can help you quickly pinpoint the contract file where the vulnerability is located.

Vulnerability Location：This can help you quickly locate the line of code where the vulnerability is present.