TOCTOU race synthesizer

Four detectors flag check-then-act races: the check and the act sit in the same function with no atomic guard between them. They run in every vulkro scan.

Rule	Shape	Severity
`TOCTOU-DB-001`	`SELECT` then `UPDATE` on the same row with no `FOR UPDATE`, lock, version stamp or isolation level	High
`TOCTOU-BALANCE-001`	`balance >= amount` check, then a subtract, without the check in the `UPDATE`'s `WHERE`	Critical
`TOCTOU-QUEUE-001`	Select pending jobs, then mark one running without `WHERE status = 'pending'`	High
`TOCTOU-IDOR-ACL-001`	`can_access` / `is_owner` / `has_permission` check, then a change to the same id without a recheck in a transaction	Medium

File-system races are covered by a separate detector.

Example: double spend

async def pay(user_id, amount):
    if balance >= amount:        # check
        balance -= amount        # act
        db.execute("UPDATE wallets SET balance = ? WHERE id = ?", (balance, user_id))

Two requests at once both pass the check, so the user gets two purchases. Fix it by putting the check inside the update:

async def pay(user_id, amount):
    result = db.execute(
        "UPDATE wallets SET balance = balance - $1 WHERE id = $2 AND balance >= $1",
        (amount, user_id),
    )
    if result.rowcount != 1:
        raise InsufficientBalance()

The database's row lock now makes the check and the act one step.

To see which routes can reach a flagged pair, open the finding's Entry Points tab in the local console (reverse reach).

Example: double spend​

Example: double spend