# ExtcallChecker

The idea is to include in every audit report a listing of all external call sites and classify each as safe or unsafe, as determined by the Prover. The Security Researcher (SR) can then consider each finding carefully. 

**What is a safe call?**

A safe call is one where the target contract and function selector are 'deterministic' in user input (i.e., in storage or in code). This can be checked by calling the containing function of the callsite twice with different inputs (so-called `calldataargs`) on the same state. On the first execution we 'save' the call target and selector in a ghost, and on the second execution we check that it is the same.

## Usage

Use the generation script to create checker configurations:

```bash
# Generate simple checker configuration
./scripts/generate_extcall_checker.py --simple Contract1.sol Contract2.sol MainContract

# Generate advanced checker configuration with target non-zero assertions
./scripts/generate_extcall_checker.py --advanced --check-non-zero-targets Contract1.sol Contract2.sol MainContract
```

**Arguments:**
- `--simple` or `--advanced`: Choose checker variant (required)
- `--check-non-zero-targets`: Assert that call targets are non-zero (optional)
- List of `.sol` files: All Solidity contract files to include
- Contract name: Name of the main contract (without `.sol` extension)

The script generates a `certora_extcall_checker/` directory with:
- Configuration file with your contract files and settings
- Specification file with appropriate checks
- Runner script for easy execution

**Run the checker:**
```bash
certoraRun certora_extcall_checker/ExtcallCheckerSimple.conf
# or
./certora_extcall_checker/run_checker.sh
```

You can copy `certora_extcall_checker` to the relevant repo to quickly get it running. 

## Current Implementation

There are 2 variants of the code, simple and advanced.

The simple variant assumes that one PC will map to a single pair of target and selector.

The advanced one will allow a PC to map to a list of such pairs, and it will also guarantee order (which is undesirable for the check, but a set implementation in spec is overkill).

### Unused Extra

The implementations for both simple and advanced contain support for two kinds of checks:

1. "Stable data": The main check we are using by default, the stability of target and selector at a particular callsite as identified by the EVM PC.
2. "Stable path": The stronger check ensures that the same PC is encountered in both arbitrary runs and has the same target and selector (there is full symmetry).


## Files

- `specs/extcall_checker_simple.template.spec` - Basic checker implementation template
- `specs/extcall_checker_advanced.template.spec` - Advanced checker with list support template
- `confs/ExtcallCheckerSimple.template.conf` - Configuration template for simple checker
- `confs/ExtcallCheckerAdvanced.template.conf` - Configuration template for advanced checker
- `scripts/generate_extcall_checker.py` - Script to generate checker configuration from templates


## Potential Future De-Noising

(For Cursor IDE):
Given this output result (link to calltrace json for each of the violated rules), determine whether the flagged external calls in each violation are indeed dangerous, or if there are conditions that make the call less suspicious. For example, the callee contract is checked earlier in the flow to be part of some registry or validated in some other way. Or, if the call is the last thing that is happening in the call, meaning there are no state changes later, reducing the risk of reentrancy attacks. Provide a short 1-2 lines of narrative on each failure.