From 34e5ae782ee4d10ef085b558e85161a1382d26c5 Mon Sep 17 00:00:00 2001 From: Fathia Oyinloye Date: Thu, 30 Jul 2026 09:45:22 +0000 Subject: [PATCH] feat(cli): add static formal invariant checker for cross-chain state --- .../check-invariants.command.spec.ts | 190 ++++++ .../commands/__tests__/command-runner.spec.ts | 3 + .../src/commands/__tests__/run-all-tests.ts | 2 + .../src/commands/check-invariants.command.ts | 178 ++++++ apps/cli/src/commands/command-runner.ts | 3 + apps/cli/src/commands/commands.module.ts | 3 + apps/cli/src/commands/index.ts | 1 + .../__tests__/state_verifier.spec.ts | 296 +++++++++ apps/cli/src/invariants/index.ts | 3 + apps/cli/src/invariants/solidity-parser.ts | 568 ++++++++++++++++++ apps/cli/src/invariants/state_verifier.ts | 426 +++++++++++++ apps/cli/src/invariants/types.ts | 142 +++++ apps/cli/src/main.ts | 22 + 13 files changed, 1837 insertions(+) create mode 100644 apps/cli/src/commands/__tests__/check-invariants.command.spec.ts create mode 100644 apps/cli/src/commands/check-invariants.command.ts create mode 100644 apps/cli/src/invariants/__tests__/state_verifier.spec.ts create mode 100644 apps/cli/src/invariants/index.ts create mode 100644 apps/cli/src/invariants/solidity-parser.ts create mode 100644 apps/cli/src/invariants/state_verifier.ts create mode 100644 apps/cli/src/invariants/types.ts diff --git a/apps/cli/src/commands/__tests__/check-invariants.command.spec.ts b/apps/cli/src/commands/__tests__/check-invariants.command.spec.ts new file mode 100644 index 00000000..79543c62 --- /dev/null +++ b/apps/cli/src/commands/__tests__/check-invariants.command.spec.ts @@ -0,0 +1,190 @@ +import { CheckInvariantsCommand } from '../check-invariants.command'; +import * as fs from 'fs'; +import * as path from 'path'; +import * as os from 'os'; + +describe('CheckInvariantsCommand', () => { + let command: CheckInvariantsCommand; + let tempDir: string; + + beforeEach(() => { + command = new CheckInvariantsCommand(); + tempDir = fs.mkdtempSync(path.join(os.tmpdir(), 'bridgewise-invariants-test-')); + }); + + afterEach(() => { + // Cleanup temp directory + try { + fs.rmSync(tempDir, { recursive: true, force: true }); + } catch { + // ignore cleanup errors + } + }); + + function writeSolFile(fileName: string, content: string): string { + const filePath = path.join(tempDir, fileName); + const dir = path.dirname(filePath); + if (!fs.existsSync(dir)) { + fs.mkdirSync(dir, { recursive: true }); + } + fs.writeFileSync(filePath, content, 'utf-8'); + return filePath; + } + + it('should return error if path option is missing', async () => { + const result = await command.execute([], {}); + expect(result.success).toBe(false); + expect(result.error).toContain('Contract path is required'); + }); + + it('should return error if path does not exist', async () => { + const result = await command.execute([], { path: '/nonexistent/path' }); + expect(result.success).toBe(false); + expect(result.error).toContain('Path does not exist'); + }); + + it('should return error if no .sol files found', async () => { + // Create empty temp dir + const result = await command.execute([], { path: tempDir }); + expect(result.success).toBe(false); + expect(result.error).toContain('No Solidity (.sol) files found'); + }); + + it('should analyze a valid Solidity contract file', async () => { + const solContent = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract TestBridge { + uint256 public lockedReserves; + uint256 public mintedSupply; + + function bridgeIn(address to, uint256 amount) external { + lockedReserves += amount; + mintedSupply += amount; + } +} +`; + writeSolFile('TestBridge.sol', solContent); + + const result = await command.execute([], { + path: tempDir, + 'fail-on-violations': false, + }); + expect(result.success).toBe(true); + expect(result.data).toBeDefined(); + expect(result.data!.contractsAnalyzed).toBe(1); + expect(result.data!.functionsAnalyzed).toBeGreaterThan(0); + }); + + it('should detect invariant violations in a vulnerable contract', async () => { + const solContent = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract VulnerableBridge { + uint256 public totalMinted; + + // VULNERABILITY: public mint with no access control and no lock + function mint(address to, uint256 amount) public { + _mint(to, amount); + totalMinted += amount; + } + + function _mint(address to, uint256 amount) internal { + // simplified + } +} +`; + writeSolFile('VulnerableBridge.sol', solContent); + + const result = await command.execute([], { path: tempDir }); + expect(result.success).toBe(false); // fail-on-violations defaults to true + expect(result.data).toBeDefined(); + expect(result.data!.violations.length).toBeGreaterThan(0); + }); + + it('should analyze .sol files recursively in subdirectories', async () => { + const subDir = path.join(tempDir, 'tokens'); + fs.mkdirSync(subDir, { recursive: true }); + fs.writeFileSync( + path.join(subDir, 'Token.sol'), + ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; +contract Token { + function foo() external pure returns (uint256) { return 42; } +} +`, + 'utf-8', + ); + + const result = await command.execute([], { + path: tempDir, + 'fail-on-violations': false, + }); + expect(result.success).toBe(true); + expect(result.data!.contractsAnalyzed).toBe(1); + }); + + it('should support the --severity filter option', async () => { + const solContent = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract TestContract { + uint256 public totalMinted; + + function mint(address to, uint256 amount) public { + _mint(to, amount); + totalMinted += amount; + } + + function _mint(address to, uint256 amount) internal {} +} +`; + writeSolFile('TestContract.sol', solContent); + + // With severity=critical, the access-control violation should still appear + const resultCritical = await command.execute([], { + path: tempDir, + severity: 'critical', + }); + + expect(resultCritical.data).toBeDefined(); + const criticalViolations = resultCritical.data!.violations.filter( + (v) => v.severity === 'critical', + ); + // All returned violations should be critical + expect( + resultCritical.data!.violations.every((v) => v.severity === 'critical'), + ).toBe(true); + }); + + it('should accept path as first positional argument', async () => { + const solContent = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; +contract Simple { function foo() external pure returns (uint256) { return 1; } } +`; + writeSolFile('Simple.sol', solContent); + + const result = await command.execute([tempDir], { + 'fail-on-violations': false, + }); + expect(result.success).toBe(true); + expect(result.data!.contractsAnalyzed).toBe(1); + }); + + it('should handle files with no valid contracts gracefully', async () => { + fs.writeFileSync( + path.join(tempDir, 'Empty.sol'), + '// SPDX-License-Identifier: MIT\npragma solidity ^0.8.20;\n// No contract here\n', + 'utf-8', + ); + + const result = await command.execute([], { path: tempDir }); + expect(result.success).toBe(false); + expect(result.error).toContain('No valid Solidity contracts found'); + }); +}); diff --git a/apps/cli/src/commands/__tests__/command-runner.spec.ts b/apps/cli/src/commands/__tests__/command-runner.spec.ts index 048e5fd5..a121362d 100644 --- a/apps/cli/src/commands/__tests__/command-runner.spec.ts +++ b/apps/cli/src/commands/__tests__/command-runner.spec.ts @@ -5,6 +5,7 @@ import { CongestionCommand } from '../congestion.command'; import { CompareCommand } from '../compare.command'; import { StatusCommand } from '../status.command'; import { HelpCommand } from '../help.command'; +import { CheckInvariantsCommand } from '../check-invariants.command'; describe('CommandRunner', () => { let runner: CommandRunner; @@ -16,6 +17,7 @@ describe('CommandRunner', () => { const compareCommand = new CompareCommand(); const statusCommand = new StatusCommand(); const helpCommand = new HelpCommand(); + const checkInvariantsCommand = new CheckInvariantsCommand(); runner = new CommandRunner( historyCommand, @@ -24,6 +26,7 @@ describe('CommandRunner', () => { compareCommand, statusCommand, helpCommand, + checkInvariantsCommand, ); runner.onModuleInit(); }); diff --git a/apps/cli/src/commands/__tests__/run-all-tests.ts b/apps/cli/src/commands/__tests__/run-all-tests.ts index 37bdd7d4..e815dfce 100644 --- a/apps/cli/src/commands/__tests__/run-all-tests.ts +++ b/apps/cli/src/commands/__tests__/run-all-tests.ts @@ -5,6 +5,7 @@ import { CompareCommand } from '../compare.command'; import { StatusCommand } from '../status.command'; import { CommandRunner } from '../command-runner'; import { HelpCommand } from '../help.command'; +import { CheckInvariantsCommand } from '../check-invariants.command'; declare const process: { exit(code?: number): void }; @@ -91,6 +92,7 @@ async function runAllTests() { new CompareCommand(), new StatusCommand(), new HelpCommand(), + new CheckInvariantsCommand(), ); runner.onModuleInit(); diff --git a/apps/cli/src/commands/check-invariants.command.ts b/apps/cli/src/commands/check-invariants.command.ts new file mode 100644 index 00000000..0a533cad --- /dev/null +++ b/apps/cli/src/commands/check-invariants.command.ts @@ -0,0 +1,178 @@ +import * as fs from 'fs'; +import * as path from 'path'; +import { CLICommand, CommandDefinition, CommandResult, Injectable, ParsedOptions } from './types'; +import { parseSolidityFiles, StateVerifier, InvariantCheckResult } from '../invariants'; + +@Injectable() +export class CheckInvariantsCommand implements CLICommand { + readonly definition: CommandDefinition = { + name: 'check-invariants', + description: + 'Run static formal invariant checks on bridge contracts to verify accounting invariants (e.g. locked reserves >= minted wrapped tokens).', + usage: + 'bridgewise check-invariants --path [--severity critical|warning|info|all] [--format json|text]', + aliases: ['invariants', 'verify-invariants'], + options: [ + { + name: 'path', + alias: 'p', + description: 'Path to directory or file containing Solidity (.sol) contracts to analyze.', + required: true, + type: 'string', + }, + { + name: 'severity', + alias: 's', + description: 'Minimum severity threshold for reporting violations.', + defaultValue: 'warning', + type: 'string', + }, + { + name: 'fail-on-violations', + alias: 'f', + description: 'Exit with non-zero code if violations are found (useful for CI/CD).', + defaultValue: true, + type: 'boolean', + }, + ], + }; + + private readonly verifier = new StateVerifier(); + + async execute( + args: string[], + options: ParsedOptions, + ): Promise> { + const targetPath = options.path || args[0]; + if (!targetPath) { + return { + success: false, + command: this.definition.name, + error: + 'Contract path is required. Specify via --path or as first argument.', + timestamp: new Date().toISOString(), + }; + } + + // Resolve and validate the input path + const resolvedPath = path.resolve(targetPath); + if (!fs.existsSync(resolvedPath)) { + return { + success: false, + command: this.definition.name, + error: `Path does not exist: ${resolvedPath}`, + timestamp: new Date().toISOString(), + }; + } + + try { + // Collect all .sol files from the path + const solFiles = this.collectSolFiles(resolvedPath); + if (solFiles.length === 0) { + return { + success: false, + command: this.definition.name, + error: `No Solidity (.sol) files found in: ${resolvedPath}`, + timestamp: new Date().toISOString(), + }; + } + + // Read and parse each file + const sources = solFiles.map((filePath) => ({ + path: filePath, + content: fs.readFileSync(filePath, 'utf-8'), + })); + + const contracts = parseSolidityFiles(sources); + if (contracts.length === 0) { + return { + success: false, + command: this.definition.name, + error: `No valid Solidity contracts found in the provided files. Ensure files contain 'contract { ... }' declarations.`, + timestamp: new Date().toISOString(), + }; + } + + // Run invariant verification + const result = this.verifier.verify(contracts); + + // Filter by severity if requested + const severityFilter = (options.severity || 'all').toLowerCase(); + if (severityFilter !== 'all') { + const severityOrder = ['info', 'warning', 'critical']; + const minIndex = severityOrder.indexOf(severityFilter); + if (minIndex >= 0) { + result.violations = result.violations.filter((v) => { + const vIndex = severityOrder.indexOf(v.severity); + return vIndex >= minIndex; + }); + } + } + + // Recompute allInvariantsSatisfied after filtering — respect the severity threshold + const severityOrder = ['info', 'warning', 'critical']; + const minSeverityIndex = severityOrder.indexOf( + (options.severity || 'all').toLowerCase(), + ); + const effectiveMinIndex = minSeverityIndex >= 0 ? minSeverityIndex : 0; + + result.allInvariantsSatisfied = !result.violations.some((v) => { + const vIndex = severityOrder.indexOf(v.severity); + return vIndex >= effectiveMinIndex; + }); + + const failOnViolations = + options['fail-on-violations'] !== undefined + ? options['fail-on-violations'] !== false && + options['fail-on-violations'] !== 'false' + : true; + + const success = failOnViolations ? result.allInvariantsSatisfied : true; + + return { + success, + command: this.definition.name, + data: result, + message: result.summary, + timestamp: new Date().toISOString(), + }; + } catch (err: any) { + return { + success: false, + command: this.definition.name, + error: err?.message || 'Failed to analyze contracts', + timestamp: new Date().toISOString(), + }; + } + } + + /** + * Recursively collect all .sol files from a directory or single file path. + */ + private collectSolFiles(targetPath: string): string[] { + const stat = fs.statSync(targetPath); + if (stat.isFile()) { + return targetPath.endsWith('.sol') ? [targetPath] : []; + } + + const results: string[] = []; + const entries = fs.readdirSync(targetPath, { withFileTypes: true }); + for (const entry of entries) { + const fullPath = path.join(targetPath, entry.name); + if (entry.isDirectory()) { + // Skip common non-contract directories + if ( + ['node_modules', '.git', 'dist', 'build', 'cache', 'artifacts'].includes( + entry.name, + ) + ) { + continue; + } + results.push(...this.collectSolFiles(fullPath)); + } else if (entry.isFile() && entry.name.endsWith('.sol')) { + results.push(fullPath); + } + } + return results.sort(); + } +} diff --git a/apps/cli/src/commands/command-runner.ts b/apps/cli/src/commands/command-runner.ts index 8e1eb790..a7bd701b 100644 --- a/apps/cli/src/commands/command-runner.ts +++ b/apps/cli/src/commands/command-runner.ts @@ -5,6 +5,7 @@ import { CongestionCommand } from './congestion.command'; import { CompareCommand } from './compare.command'; import { StatusCommand } from './status.command'; import { HelpCommand } from './help.command'; +import { CheckInvariantsCommand } from './check-invariants.command'; @Injectable() export class CommandRunner { @@ -17,6 +18,7 @@ export class CommandRunner { private readonly compareCommand: CompareCommand, private readonly statusCommand: StatusCommand, private readonly helpCommand: HelpCommand, + private readonly checkInvariantsCommand: CheckInvariantsCommand, ) {} onModuleInit() { @@ -27,6 +29,7 @@ export class CommandRunner { this.compareCommand, this.statusCommand, this.helpCommand, + this.checkInvariantsCommand, ]); const definitions = Array.from(this.commandMap.values()) diff --git a/apps/cli/src/commands/commands.module.ts b/apps/cli/src/commands/commands.module.ts index 35354b0d..fc287fd1 100644 --- a/apps/cli/src/commands/commands.module.ts +++ b/apps/cli/src/commands/commands.module.ts @@ -4,6 +4,7 @@ import { CongestionCommand } from './congestion.command'; import { CompareCommand } from './compare.command'; import { StatusCommand } from './status.command'; import { HelpCommand } from './help.command'; +import { CheckInvariantsCommand } from './check-invariants.command'; import { CommandRunner } from './command-runner'; declare const require: any; @@ -23,6 +24,7 @@ try { CompareCommand, StatusCommand, HelpCommand, + CheckInvariantsCommand, CommandRunner, ], exports: [ @@ -32,6 +34,7 @@ try { CompareCommand, StatusCommand, HelpCommand, + CheckInvariantsCommand, CommandRunner, ], }) diff --git a/apps/cli/src/commands/index.ts b/apps/cli/src/commands/index.ts index 9d60ce8c..de141614 100644 --- a/apps/cli/src/commands/index.ts +++ b/apps/cli/src/commands/index.ts @@ -5,5 +5,6 @@ export * from './congestion.command'; export * from './compare.command'; export * from './status.command'; export * from './help.command'; +export * from './check-invariants.command'; export * from './command-runner'; export * from './commands.module'; diff --git a/apps/cli/src/invariants/__tests__/state_verifier.spec.ts b/apps/cli/src/invariants/__tests__/state_verifier.spec.ts new file mode 100644 index 00000000..5b474a1e --- /dev/null +++ b/apps/cli/src/invariants/__tests__/state_verifier.spec.ts @@ -0,0 +1,296 @@ +import { parseSolidityFiles } from '../solidity-parser'; +import { StateVerifier } from '../state_verifier'; +import { ParsedContract } from '../types'; + +// --------------------------------------------------------------------------- +// Sample Solidity sources for testing +// --------------------------------------------------------------------------- + +const BRIDGE_WRAPPED_TOKEN_SRC = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol"; +import {ERC20Burnable} from "@openzeppelin/contracts/token/ERC20/extensions/ERC20Burnable.sol"; +import {AccessControl} from "@openzeppelin/contracts/access/AccessControl.sol"; + +contract BridgeWrappedToken is ERC20, ERC20Burnable, AccessControl { + bytes32 public constant MINTER_ROLE = keccak256("MINTER_ROLE"); + bytes32 public constant BURNER_ROLE = keccak256("BURNER_ROLE"); + + uint256 public totalMinted; + + constructor( + string memory name_, + string memory symbol_, + address bridgeVault, + address admin + ) ERC20(name_, symbol_) { + _grantRole(DEFAULT_ADMIN_ROLE, admin); + _grantRole(MINTER_ROLE, bridgeVault); + _grantRole(BURNER_ROLE, bridgeVault); + } + + function mint(address to, uint256 amount) external onlyRole(MINTER_ROLE) { + _mint(to, amount); + totalMinted += amount; + } + + function burnFrom(address account, uint256 amount) public override onlyRole(BURNER_ROLE) { + super.burnFrom(account, amount); + totalMinted -= amount; + } +} +`; + +const BAD_MINT_CONTRACT_SRC = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract BadBridgeToken { + uint256 public totalMinted; + + // VULNERABILITY: public mint with no access control + function mint(address to, uint256 amount) public { + _mint(to, amount); + totalMinted += amount; + } + + function _mint(address to, uint256 amount) internal { + // simplified mint logic + } +} +`; + +const VAULT_HEALTH_SRC = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +interface IReserveVault { + function lockedReserves(address token) external view returns (uint256); +} + +contract VaultHealthEvaluator { + uint256 public constant BPS = 10_000; + uint256 public constant UNDERCOLLATERALIZED_THRESHOLD = 10_000; + uint256 public constant CRITICAL_THRESHOLD = 8_000; + + uint256 public totalLockedReserves; + uint256 public totalMintedSupply; + + function evaluate( + address reserveVault, + address wrappedToken + ) external view returns (uint256 ratioBps, uint256 health) { + uint256 totalLocked = IReserveVault(reserveVault).lockedReserves(wrappedToken); + uint256 totalMinted = 1000; + if (totalMinted == 0) { + return (0, 0); + } + ratioBps = (totalLocked * BPS) / totalMinted; + return (ratioBps, 0); + } +} +`; + +const MINT_BEFORE_LOCK_SRC = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract MintBeforeLockBridge { + uint256 public lockedReserves; + uint256 public mintedSupply; + + // VULNERABILITY: mints before locking + function bridgeIn(address token, uint256 amount, address to) external { + // Mint happens first - re-entrancy risk + mintedSupply += amount; + // Lock reserves after mint + lockedReserves += amount; + } +} +`; + +const CORRECT_BRIDGE_SRC = ` +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.20; + +contract CorrectBridge { + uint256 public lockedReserves; + uint256 public mintedSupply; + + // CORRECT: locks before minting + function bridgeIn(address token, uint256 amount, address to) external { + lockedReserves += amount; // lock first + mintedSupply += amount; // mint after lock + } +} +`; + +// --------------------------------------------------------------------------- +// Tests +// --------------------------------------------------------------------------- + +describe('StateVerifier', () => { + let verifier: StateVerifier; + + beforeEach(() => { + verifier = new StateVerifier(); + }); + + describe('Solidity Parser', () => { + it('should parse a contract with mint/burn functions', () => { + const contracts = parseSolidityFiles([ + { path: 'BridgeWrappedToken.sol', content: BRIDGE_WRAPPED_TOKEN_SRC }, + ]); + + expect(contracts.length).toBe(1); + const contract = contracts[0]; + expect(contract.name).toBe('BridgeWrappedToken'); + expect(contract.inherits).toContain('ERC20'); + expect(contract.inherits).toContain('AccessControl'); + + const funcNames = contract.functions.map((f) => f.name); + expect(funcNames).toContain('mint'); + expect(funcNames).toContain('burnFrom'); + + const mintFunc = contract.functions.find((f) => f.name === 'mint'); + expect(mintFunc).toBeDefined(); + expect(mintFunc!.transitions.length).toBeGreaterThan(0); + expect(mintFunc!.transitions.some((t) => t.operationName === '_mint')).toBe(true); + + const burnFunc = contract.functions.find((f) => f.name === 'burnFrom'); + expect(burnFunc).toBeDefined(); + }); + + it('should detect state variables with balance semantics', () => { + const contracts = parseSolidityFiles([ + { path: 'VaultHealthEvaluator.sol', content: VAULT_HEALTH_SRC }, + ]); + + expect(contracts.length).toBe(1); + const lockedVars = contracts[0].stateVariables.filter((v) => v.category === 'locked'); + const mintedVars = contracts[0].stateVariables.filter((v) => v.category === 'minted'); + + expect(lockedVars.length).toBeGreaterThan(0); + const lockedNames = lockedVars.map((v) => v.name); + expect(lockedNames.some((n) => /locked|reserve/i.test(n))).toBe(true); + }); + + it('should parse multiple contracts from multiple files', () => { + const contracts = parseSolidityFiles([ + { path: 'BridgeWrappedToken.sol', content: BRIDGE_WRAPPED_TOKEN_SRC }, + { path: 'VaultHealthEvaluator.sol', content: VAULT_HEALTH_SRC }, + ]); + + expect(contracts.length).toBe(2); + expect(contracts.map((c) => c.name)).toContain('BridgeWrappedToken'); + expect(contracts.map((c) => c.name)).toContain('VaultHealthEvaluator'); + }); + + it('should detect state transitions from compound assignments', () => { + const contracts = parseSolidityFiles([ + { path: 'CorrectBridge.sol', content: CORRECT_BRIDGE_SRC }, + ]); + + const bridgeFunc = contracts[0].functions.find((f) => f.name === 'bridgeIn'); + expect(bridgeFunc).toBeDefined(); + expect( + bridgeFunc!.transitions.some( + (t) => t.operation === 'add' && t.category === 'locked', + ), + ).toBe(true); + expect( + bridgeFunc!.transitions.some( + (t) => t.operation === 'add' && t.category === 'minted', + ), + ).toBe(true); + }); + }); + + describe('Invariant Checking', () => { + it('should detect missing access control on mint functions', () => { + const contracts = parseSolidityFiles([ + { path: 'BadBridgeToken.sol', content: BAD_MINT_CONTRACT_SRC }, + ]); + + const result = verifier.verify(contracts); + + const criticalViolations = result.violations.filter( + (v) => v.severity === 'critical', + ); + expect(criticalViolations.length).toBeGreaterThan(0); + expect( + criticalViolations.some((v) => v.category === 'access-control'), + ).toBe(true); + }); + + it('should not flag properly gated mint as access control violation', () => { + const contracts = parseSolidityFiles([ + { path: 'BridgeWrappedToken.sol', content: BRIDGE_WRAPPED_TOKEN_SRC }, + ]); + + const result = verifier.verify(contracts); + + const criticalAccessViolations = result.violations.filter( + (v) => v.severity === 'critical' && v.category === 'access-control', + ); + expect(criticalAccessViolations.length).toBe(0); + }); + + it('should detect mint-before-lock ordering violation', () => { + const contracts = parseSolidityFiles([ + { path: 'MintBeforeLockBridge.sol', content: MINT_BEFORE_LOCK_SRC }, + ]); + + const result = verifier.verify(contracts); + + const orderingViolations = result.violations.filter( + (v) => v.category === 'conservative-minting' && v.invariant.includes('Ordering'), + ); + expect(orderingViolations.length).toBeGreaterThan(0); + }); + + it('should not flag correctly ordered lock-then-mint', () => { + const contracts = parseSolidityFiles([ + { path: 'CorrectBridge.sol', content: CORRECT_BRIDGE_SRC }, + ]); + + const result = verifier.verify(contracts); + + const orderingViolations = result.violations.filter( + (v) => v.category === 'conservative-minting' && v.invariant.includes('Ordering'), + ); + expect(orderingViolations.length).toBe(0); + }); + + it('should detect mint without corresponding lock', () => { + const contracts = parseSolidityFiles([ + { path: 'BadBridgeToken.sol', content: BAD_MINT_CONTRACT_SRC }, + ]); + + const result = verifier.verify(contracts); + + const conservativeViolations = result.violations.filter( + (v) => v.category === 'conservative-minting', + ); + expect(conservativeViolations.length).toBeGreaterThan(0); + }); + + it('should produce a valid result structure', () => { + const contracts = parseSolidityFiles([ + { path: 'CorrectBridge.sol', content: CORRECT_BRIDGE_SRC }, + ]); + + const result = verifier.verify(contracts); + + expect(result.contractsAnalyzed).toBe(1); + expect(result.functionsAnalyzed).toBeGreaterThan(0); + expect(result.transitionsDetected).toBeGreaterThan(0); + expect(result.summary).toBeDefined(); + expect(result.summary.length).toBeGreaterThan(0); + expect(result.contractDetails).toBeDefined(); + expect(result.contractDetails.length).toBe(1); + }); + }); +}); diff --git a/apps/cli/src/invariants/index.ts b/apps/cli/src/invariants/index.ts new file mode 100644 index 00000000..1cd2d2e7 --- /dev/null +++ b/apps/cli/src/invariants/index.ts @@ -0,0 +1,3 @@ +export * from './types'; +export * from './solidity-parser'; +export * from './state_verifier'; diff --git a/apps/cli/src/invariants/solidity-parser.ts b/apps/cli/src/invariants/solidity-parser.ts new file mode 100644 index 00000000..61af35ab --- /dev/null +++ b/apps/cli/src/invariants/solidity-parser.ts @@ -0,0 +1,568 @@ +/** + * @module invariants/solidity-parser + * @description Lightweight regex-based Solidity source parser for static invariant analysis. + * + * Extracts: + * - Contract declarations & inheritance + * - State variables with balance semantics + * - Function definitions with visibility and body + * - State-modifying operations (mint, burn, lock, transfers) + */ + +import { + ContractFunction, + OperationMapping, + ParsedContract, + StateTransition, + StateVariable, +} from './types'; + +// --------------------------------------------------------------------------- +// Known operation signatures mapped to their invariant category +// --------------------------------------------------------------------------- + +/** + * Recognised state-modifying operations and their categories. + * When adding new bridge adapters / contracts, extend this table. + */ +const OPERATION_MAPPINGS: OperationMapping[] = [ + // --- Mint operations (increase minted supply) --- + { + signature: '_mint', + category: 'minted', + kind: 'add', + description: 'Mints new wrapped tokens, increasing total supply.', + }, + { + signature: '.mint', + category: 'minted', + kind: 'add', + description: 'Mints new wrapped tokens via ERC-20 mint.', + }, + // --- Burn operations (decrease minted supply) --- + { + signature: '_burn', + category: 'minted', + kind: 'subtract', + description: 'Burns wrapped tokens, decreasing total supply.', + }, + { + signature: 'burnFrom', + category: 'minted', + kind: 'subtract', + description: 'Burns wrapped tokens from a specific account.', + }, + { + signature: '.burn', + category: 'minted', + kind: 'subtract', + description: 'Burns wrapped tokens via ERC-20 burn.', + }, + // --- Lock operations (increase locked reserves) --- + { + signature: '.lock(', + category: 'locked', + kind: 'add', + description: 'Locks assets in the bridge vault, increasing locked reserves.', + }, + { + signature: 'safeTransferFrom', + category: 'locked', + kind: 'add', + description: 'Transfers tokens into the vault, increasing locked reserves.', + }, + { + signature: '.deposit', + category: 'locked', + kind: 'add', + description: 'Wraps native token (e.g. ETH → WETH), increasing locked token balance.', + }, + // --- Release operations (decrease locked reserves) --- + { + signature: '.release(', + category: 'locked', + kind: 'subtract', + description: 'Releases locked assets from the vault.', + }, + { + signature: '.unlock(', + category: 'locked', + kind: 'subtract', + description: 'Unlocks assets from the vault.', + }, +]; + +// --------------------------------------------------------------------------- +// State variable heuristics +// --------------------------------------------------------------------------- + +/** Patterns that suggest a state variable tracks locked reserves. */ +const LOCKED_PATTERNS = [ + /locked/i, + /reserve/i, + /holding/i, + /deposit/i, + /vault_?balance/i, +]; + +/** Patterns that suggest a state variable tracks minted/wrapped supply. */ +const MINTED_PATTERNS = [ + /minted/i, + /supply/i, + /wrapped/i, + /outstanding/i, + /totalsupply/i, +]; + +/** + * Classify a state variable name into a category. + */ +function classifyVariable(name: string): 'locked' | 'minted' | 'unknown' { + for (const pat of LOCKED_PATTERNS) { + if (pat.test(name)) return 'locked'; + } + for (const pat of MINTED_PATTERNS) { + if (pat.test(name)) return 'minted'; + } + return 'unknown'; +} + +// --------------------------------------------------------------------------- +// Source normalisation helpers +// --------------------------------------------------------------------------- + +/** + * Strip single-line (// ...) and multi-line (/* ... *​/) comments from + * Solidity source so they don't interfere with regex matching. + * + * Also normalises strings to avoid comment-like patterns inside them. + */ +function stripComments(source: string): string { + // Temporarily replace string literals to protect comment-like patterns inside them + const strings: string[] = []; + let cleaned = source.replace(/"(?:[^"\\]|\\.)*"/g, (match) => { + strings.push(match); + return `__STRING_${strings.length - 1}__`; + }); + cleaned = cleaned.replace(/'(?:[^'\\]|\\.)*'/g, (match) => { + strings.push(match); + return `__STRING_${strings.length - 1}__`; + }); + + // Remove multi-line comments first + cleaned = cleaned.replace(/\/\*[\s\S]*?\*\//g, ''); + // Remove single-line comments + cleaned = cleaned.replace(/\/\/.*$/gm, ''); + + // Restore string literals + cleaned = cleaned.replace(/__STRING_(\d+)__/g, (_, i) => strings[parseInt(i)] ?? ''); + + return cleaned; +} + +/** + * Collapse runs of whitespace into a single space for easier regex matching. + */ +function collapseWhitespace(s: string): string { + return s.replace(/\s+/g, ' ').trim(); +} + +// --------------------------------------------------------------------------- +// Parsing functions +// --------------------------------------------------------------------------- + +/** + * Extract the contract name from a contract declaration line. + * Handles: `contract Foo`, `abstract contract Foo`, `contract Foo is Bar, Baz` + */ +function extractContractName(line: string): string | null { + const m = /(?:abstract\s+)?contract\s+(\w+)/i.exec(line); + return m ? m[1] : null; +} + +/** + * Extract inherited contract names from the `is` clause. + */ +function extractInherits(line: string): string[] { + const m = /contract\s+\w+\s+is\s+([^{]+)/i.exec(line); + if (!m) return []; + return m[1] + .split(',') + .map((s) => s.trim()) + .filter((s) => /^\w+/.test(s)) + .map((s) => s.match(/^(\w+)/)?.[1] ?? s); +} + +/** + * Extract state variable declarations from a contract body. + * Matches common Solidity patterns including user-defined types: + * uint256 public lockedReserves; + * mapping(address => uint256) private _balances; + * IERC20 public token; + * MyStruct public myVar; + */ +function extractStateVariables( + body: string, + contractName: string, + filePath: string, + startLineOffset: number, +): StateVariable[] { + const vars: StateVariable[] = []; + + // Match state variable declarations (not inside functions). + // Pattern: type ... name visibility? (= defaultValue)? ; + const varRegex = + /(?:(?:mapping\s*\([^)]+\))|(?:uint(?:8|16|32|64|128|256)?)|(?:int(?:8|16|32|64|128|256)?)|(?:bool)|(?:address)|(?:bytes(?:32)?)|(?:string)|(?:\w+(?:\[\])?))\s+(?:public\s+|private\s+|internal\s+|constant\s+|immutable\s+)*(\w+)\s*(?:=\s*[^;]+)?\s*;/g; + + // Strip function bodies using balanced brace matching (same approach as extractFunctions) + const withoutFunctions = stripAllFunctionBodies(body); + + let m: RegExpExecArray | null; + while ((m = varRegex.exec(withoutFunctions)) !== null) { + const name = m[1]; + // Skip keywords and modifier-like names + if ( + ['public', 'private', 'internal', 'external', 'constant', 'immutable', 'view', 'pure', 'payable', 'memory', 'storage', 'calldata', 'indexed'].includes(name) + ) { + continue; + } + + const category = classifyVariable(name); + vars.push({ + name, + type: m[0].replace(/\s*;.*$/, '').replace(name, '').trim(), + category, + contractName, + filePath, + line: startLineOffset + withoutFunctions.slice(0, m.index).split('\n').length, + }); + } + + return vars; +} + +/** + * Strip all function bodies from source using balanced brace matching. + * This handles nested braces correctly (unlike a simple non-greedy regex). + */ +function stripAllFunctionBodies(source: string): string { + const funcRegex = + /function\s+(\w+)\s*\(([^)]*)\)/g; + let result = source; + const removals: Array<{ start: number; end: number }> = []; + + let m: RegExpExecArray | null; + while ((m = funcRegex.exec(source)) !== null) { + const sigEnd = m.index + m[0].length; + const remaining = source.slice(sigEnd); + + // Find opening brace (skip modifiers/returns) + const braceMatch = /[\s\S]*?\{/.exec(remaining); + if (!braceMatch) continue; + + const bracePos = sigEnd + braceMatch[0].length - 1; + + // Find matching closing brace + let depth = 1; + let endPos = bracePos + 1; + while (depth > 0 && endPos < source.length) { + if (source[endPos] === '{') depth++; + else if (source[endPos] === '}') depth--; + endPos++; + } + + removals.push({ start: m.index, end: endPos }); + } + + // Apply removals from end to start to preserve indices + removals.sort((a, b) => b.start - a.start); + for (const { start, end } of removals) { + result = result.slice(0, start) + result.slice(end); + } + + return result; +} + +/** + * Extract function definitions with their bodies from a contract body. + */ +function extractFunctions( + body: string, + contractName: string, + filePath: string, + startLineOffset: number, +): ContractFunction[] { + const functions: ContractFunction[] = []; + + // Match function definitions — capture the full signature up to (but not including) the opening brace + const funcRegex = + /function\s+(\w+)\s*\(([^)]*)\)/g; + + let m: RegExpExecArray | null; + while ((m = funcRegex.exec(body)) !== null) { + const funcName = m[1]; + + // Find the opening brace after the function signature + const sigEnd = m.index + m[0].length; + const remaining = body.slice(sigEnd); + + // Find opening brace while capturing the modifier text between ) and { + const braceMatch = /([\s\S]*?)\{/.exec(remaining); + if (!braceMatch) continue; + + const modifiersText = braceMatch[1].trim(); + const bracePos = sigEnd + braceMatch[0].length - 1; + + // Extract visibility from modifiers text + const visMatch = + /\b(public|external|internal|private)\b/.exec(modifiersText); + const visibility = visMatch ? visMatch[1] : 'internal'; + + const isReadOnly = + /\bview\b/.test(modifiersText) || /\bpure\b/.test(modifiersText); + + // Find matching closing brace + let depth = 1; + let endPos = bracePos + 1; + while (depth > 0 && endPos < body.length) { + if (body[endPos] === '{') depth++; + else if (body[endPos] === '}') depth--; + endPos++; + } + + const funcBody = body.slice(bracePos + 1, endPos - 1); + const bodyLines = funcBody.split('\n').length; + + // Calculate the line number of this function + const linesBefore = body.slice(0, m.index).split('\n').length; + + const transitions = extractTransitions( + funcBody, + funcName, + contractName, + filePath, + startLineOffset + linesBefore, + ); + + functions.push({ + name: funcName, + visibility, + isReadOnly, + modifiersText, + body: funcBody, + contractName, + filePath, + line: startLineOffset + linesBefore, + bodyLineCount: bodyLines, + transitions, + }); + } + + return functions; +} + +/** + * Detect state-modifying operations within a function body. + */ +function extractTransitions( + funcBody: string, + functionName: string, + contractName: string, + filePath: string, + baseLine: number, +): StateTransition[] { + const transitions: StateTransition[] = []; + + // Track which lines we've already assigned transitions to (avoid double-counting + // when a single line matches multiple patterns). + const matchedLines = new Set(); + + const lines = funcBody.split('\n'); + + for (let i = 0; i < lines.length; i++) { + const line = lines[i]; + + for (const mapping of OPERATION_MAPPINGS) { + if (!line.includes(mapping.signature)) continue; + + // Skip commented-out lines + const trimmed = line.trim(); + if (trimmed.startsWith('//')) continue; + if (trimmed.startsWith('/*')) continue; + + // Extract the amount expression from the operation arguments. + // For patterns like `_mint(to, amount)` or `vault.lock(chain, token, amount, recipient)`, + // we extract the relevant numeric argument. + const amountExpression = extractAmountExpression(line, mapping.signature); + + const lineNum = baseLine + i + 1; + matchedLines.add(lineNum); + + transitions.push({ + operation: mapping.kind, + category: mapping.category, + operationName: mapping.signature.replace(/^\./, ''), + amountExpression, + functionName, + contractName, + filePath, + line: lineNum, + context: trimmed, + }); + } + + // Also detect compound assignment on state variables (e.g. `totalLocked += amount`) + if (!matchedLines.has(baseLine + i + 1)) { + const compAssignMatch = /(\w+)\s*(\+|-)=\s*([^;]+)/.exec(line); + if (compAssignMatch) { + const varName = compAssignMatch[1]; + const cat = classifyVariable(varName); + if (cat !== 'unknown') { + transitions.push({ + operation: compAssignMatch[2] === '+' ? 'add' : 'subtract', + category: cat, + operationName: compAssignMatch[2] === '+' ? 'addTo' : 'subtractFrom', + amountExpression: compAssignMatch[3].trim(), + functionName, + contractName, + filePath, + line: baseLine + i + 1, + context: line.trim(), + }); + } + } + } + } + + return transitions; +} + +/** + * Extract the relevant amount argument from an operation call. + * + * For known signatures we know which argument position represents the amount: + * _mint(to, amount) → position 2 + * _burn(account, amount) → position 2 + * vault.lock(chainId, token, amount, recipient) → position 3 + * .burn(amount) → position 1 + * safeTransferFrom(from, to, amount) → position 3 + */ +function extractAmountExpression(line: string, signature: string): string { + // Find the call and its arguments + const callRegex = new RegExp( + signature.replace(/[.*+?^${}()|[\]\\]/g, '\\$&') + '\\s*\\(([^)]*)\\)', + ); + const m = callRegex.exec(line); + if (!m) return 'unknown'; + + const args = m[1].split(',').map((s) => s.trim()); + + // Determine which argument is the amount based on the signature + const sigClean = signature.replace(/^\./, ''); + switch (sigClean) { + case '_mint': + case '_burn': + return args[1] ?? 'unknown'; + case 'lock(': + case 'safeTransferFrom': + // For vault.lock(chainId, token, amount, ...) → index 2 + // For safeTransferFrom(from, to, amount) → index 2 + return args[2] ?? 'unknown'; + case 'burn': + case '.mint': + // .mint(to, amount) and .burn(amount) — multi-arity depends on context + // For ERC20.mint(to, amount) → index 1, for ERC20.burn(amount) → index 0 + return args[1] ?? args[0] ?? 'unknown'; + case 'release(': + case 'unlock(': + return args[1] ?? args[0] ?? 'unknown'; + case 'deposit': + // .deposit() wraps msg.value — no explicit amount argument + return 'msg.value'; + default: + // Best effort: return the last argument that looks numeric + for (let i = args.length - 1; i >= 0; i--) { + const arg = args[i]; + if (/\d+/.test(arg) || /amount|value|sum/i.test(arg)) { + return arg; + } + } + return args[args.length - 1] ?? 'unknown'; + } +} + +/** + * Parse a Solidity source file into a `ParsedContract` structure. + */ +export function parseSolidityFile( + source: string, + filePath: string, +): ParsedContract[] { + const cleaned = stripComments(source); + const contracts: ParsedContract[] = []; + + // Match contract declarations with their bodies using balanced braces + const contractRegex = + /(?:abstract\s+)?contract\s+(\w+)(?:\s+is\s+[^{]+)?\s*\{/g; + let m: RegExpExecArray | null; + while ((m = contractRegex.exec(cleaned)) !== null) { + const contractName = m[1]; + const declLine = cleaned.slice(m.index, m.index + m[0].length); + const inherits = extractInherits(declLine); + + // Find matching closing brace for the contract body + const contractOpenPos = m.index + m[0].length - 1; // position of { + let depth = 1; + let contractClosePos = contractOpenPos + 1; + while (depth > 0 && contractClosePos < cleaned.length) { + if (cleaned[contractClosePos] === '{') depth++; + else if (cleaned[contractClosePos] === '}') depth--; + contractClosePos++; + } + + const contractBody = cleaned.slice(contractOpenPos + 1, contractClosePos - 1); + const startLineOffset = cleaned.slice(0, m.index).split('\n').length; + + const stateVariables = extractStateVariables( + contractBody, + contractName, + filePath, + startLineOffset, + ); + + const functions = extractFunctions( + contractBody, + contractName, + filePath, + startLineOffset, + ); + + const lineCount = cleaned.split('\n').length; + + contracts.push({ + name: contractName, + filePath, + stateVariables, + functions, + inherits, + lineCount, + }); + } + + return contracts; +} + +/** + * Parse multiple Solidity source files. + */ +export function parseSolidityFiles( + sources: Array<{ path: string; content: string }>, +): ParsedContract[] { + const allContracts: ParsedContract[] = []; + for (const { path, content } of sources) { + allContracts.push(...parseSolidityFile(content, path)); + } + return allContracts; +} + +export { OPERATION_MAPPINGS }; diff --git a/apps/cli/src/invariants/state_verifier.ts b/apps/cli/src/invariants/state_verifier.ts new file mode 100644 index 00000000..5fcc64df --- /dev/null +++ b/apps/cli/src/invariants/state_verifier.ts @@ -0,0 +1,426 @@ +/** + * @module invariants/state_verifier + * @description Evaluates state transitions across parsed contracts against + * mathematical bridge invariants. + * + * Primary invariants checked: + * 1. SOLVENCY: TotalLockedReserves >= TotalMintedWrappedTokens + * 2. CONSERVATIVE-MINTING: ΔLocked >= ΔMinted on every execution path + * 3. ACCESS-CONTROL: Mint/burn operations are properly role-gated + */ + +import { + ContractFunction, + InvariantCheckResult, + InvariantViolation, + ParsedContract, + StateTransition, +} from './types'; + +/** + * Core invariant verifier. Accepts parsed contracts and produces a detailed + * report of invariant violations. + */ +export class StateVerifier { + // ----------------------------------------------------------------------- + // Public entry point + // ----------------------------------------------------------------------- + + /** + * Run all invariants against the parsed contracts and return a structured + * result suitable for CLI output or CI/CD consumption. + */ + verify(contracts: ParsedContract[]): InvariantCheckResult { + const violations: InvariantViolation[] = []; + let totalTransitions = 0; + let totalFunctions = 0; + + const contractDetails: InvariantCheckResult['contractDetails'] = []; + + for (const contract of contracts) { + const lockedVars = contract.stateVariables + .filter((v) => v.category === 'locked') + .map((v) => v.name); + const mintedVars = contract.stateVariables + .filter((v) => v.category === 'minted') + .map((v) => v.name); + + let contractTransitions = 0; + let contractFunctionsScanned = 0; + + for (const func of contract.functions) { + if (func.isReadOnly) continue; // view/pure functions don't modify state + + contractFunctionsScanned++; + totalFunctions++; + contractTransitions += func.transitions.length; + totalTransitions += func.transitions.length; + + // Check invariants on each state-modifying function + violations.push( + ...this.checkConservativeMinting(func, contracts), + ...this.checkAtomicLockMint(func, contracts), + ...this.checkAccessControl(func), + ); + } + + const contractViolations = violations.filter( + (v) => v.sourceLocation.startsWith(contract.filePath), + ); + + contractDetails.push({ + contractName: contract.name, + filePath: contract.filePath, + functionsScanned: contractFunctionsScanned, + lockedVariables: lockedVars, + mintedVariables: mintedVars, + transitions: contractTransitions, + violations: contractViolations.length, + }); + } + + // Check cross-contract solvency + violations.push(...this.checkCrossContractSolvency(contracts)); + + const criticalCount = violations.filter((v) => v.severity === 'critical').length; + const allSatisfied = criticalCount === 0; + const warningCount = violations.filter((v) => v.severity === 'warning').length; + const infoCount = violations.filter((v) => v.severity === 'info').length; + + const summary = allSatisfied + ? `✅ All invariants satisfied across ${contracts.length} contract(s), ${totalFunctions} function(s), ${totalTransitions} transition(s).` + : `❌ Found ${criticalCount} critical, ${warningCount} warning, ${infoCount} info violation(s) across ${contracts.length} contract(s).`; + + return { + allInvariantsSatisfied: allSatisfied, + contractsAnalyzed: contracts.length, + functionsAnalyzed: totalFunctions, + transitionsDetected: totalTransitions, + violations, + summary, + contractDetails, + }; + } + + // ----------------------------------------------------------------------- + // Invariant 1: Conservative Minting + // + // For every function that mints, there must be a corresponding lock + // operation whose amount is >= the mint amount on the same execution + // path (or a prior lock that has been verified on-chain). + // ----------------------------------------------------------------------- + + private checkConservativeMinting( + func: ContractFunction, + allContracts: ParsedContract[], + ): InvariantViolation[] { + const violations: InvariantViolation[] = []; + + const mints = func.transitions.filter( + (t) => t.category === 'minted' && t.operation === 'add', + ); + const locks = func.transitions.filter( + (t) => t.category === 'locked' && t.operation === 'add', + ); + const burns = func.transitions.filter( + (t) => t.category === 'minted' && t.operation === 'subtract', + ); + + // If there are mint operations but no lock operations in the same function, + // flag it as a potential violation (needs further cross-function analysis). + for (const mint of mints) { + // Check if there's a corresponding lock in this function + const hasLocalLock = locks.length > 0; + + // Check if this function is called by a function that locks + // (e.g. a vault's lock function calls an internal _deposit) + const callerLocks = this.findCallersWithOperation( + func, + allContracts, + 'locked', + 'add', + ); + + // Check if the mint is gated by a role that only the vault can call + // (which implies the vault already did the lock) + const isPrivilegedMint = this.isPrivilegedContext(func, mint); + + if (!hasLocalLock && callerLocks.length === 0 && !isPrivilegedMint) { + violations.push({ + invariant: 'Conservative Minting (ΔLocked >= ΔMinted)', + description: `Function '${func.name}' mints tokens (via '${mint.operationName}') without a corresponding lock operation in the same execution path. This could allow minting without backing reserves.`, + path: `${func.contractName} → ${func.name}()`, + sourceLocation: `${func.filePath}:${mint.line}`, + severity: 'critical', + category: 'conservative-minting', + }); + } else if (hasLocalLock) { + // Verify the amounts: lock amount should be >= mint amount + // This is a symbolic check — we note it but don't flag as critical + // since runtime values may differ. + const mintExpr = mint.amountExpression; + const lockExprs = locks.map((l) => l.amountExpression); + + // If mint uses a different variable than locks, that's suspicious + const allMatch = lockExprs.some( + (le) => + le === mintExpr || + le.includes(mintExpr) || + mintExpr.includes(le), + ); + + if (!allMatch && !isPrivilegedMint) { + violations.push({ + invariant: 'Conservative Minting (ΔLocked >= ΔMinted)', + description: `Function '${func.name}' mints with expression '${mintExpr}' but locks with '${lockExprs.join(', ')}'. The lock amount may not cover the mint amount.`, + path: `${func.contractName} → ${func.name}()`, + sourceLocation: `${func.filePath}:${mint.line}`, + severity: 'warning', + category: 'conservative-minting', + }); + } + } + } + + return violations; + } + + // ----------------------------------------------------------------------- + // Invariant 2: Atomic Lock-Mint Pairs + // + // Lock and mint operations on the same logical transfer should appear + // as an ordered pair: lock → mint. If mint appears before lock, + // there's a re-entrancy / ordering risk. + // ----------------------------------------------------------------------- + + private checkAtomicLockMint( + func: ContractFunction, + _allContracts: ParsedContract[], + ): InvariantViolation[] { + const violations: InvariantViolation[] = []; + + const transitions = func.transitions; + + // Find the first mint and last lock in the function body + let firstMintLine: number | null = null; + let lastLockLine: number | null = null; + + for (const t of transitions) { + if (t.category === 'minted' && t.operation === 'add') { + if (firstMintLine === null || t.line < firstMintLine) { + firstMintLine = t.line; + } + } + if (t.category === 'locked' && t.operation === 'add') { + if (lastLockLine === null || t.line > lastLockLine) { + lastLockLine = t.line; + } + } + } + + // If mint happens before the lock operation, flag it + if ( + firstMintLine !== null && + lastLockLine !== null && + firstMintLine < lastLockLine + ) { + violations.push({ + invariant: 'Atomic Lock-Mint Ordering', + description: `Function '${func.name}' mints tokens (line ${firstMintLine}) before locking assets (line ${lastLockLine}). Mint should occur after the lock to prevent re-entrancy and ensure backing reserves exist first.`, + path: `${func.contractName} → ${func.name}()`, + sourceLocation: `${func.filePath}:${firstMintLine}`, + severity: 'warning', + category: 'conservative-minting', + }); + } + + return violations; + } + + // ----------------------------------------------------------------------- + // Invariant 3: Access Control on Mint/Burn + // + // Mint and burn functions must be guarded by role checks or access + // modifiers. Unguarded mint functions are a critical vulnerability. + // ----------------------------------------------------------------------- + + private checkAccessControl(func: ContractFunction): InvariantViolation[] { + const violations: InvariantViolation[] = []; + // Check both the modifiers text (function signature) and the body + const combinedText = `${func.modifiersText} ${func.body}`; + + const hasMintOrBurn = func.transitions.some( + (t) => t.category === 'minted', + ); + + if (!hasMintOrBurn) return violations; + + // Check for common access control patterns in modifiers + body + const hasRoleCheck = + /\bonlyRole\b/.test(combinedText) || + /\brequire\s*\(\s*(?:msg\.sender\s*==|hasRole)/.test(combinedText) || + /\brequire\s*\(\s*.+\s*==\s*owner/.test(combinedText) || + /\bonlyOwner\b/.test(combinedText) || + /\bonlyVault\b/.test(combinedText) || + /\bonlyBridge\b/.test(combinedText); + + // Check if function visibility is external/public (less safe if unguarded) + const isPublic = + func.visibility === 'public' || func.visibility === 'external'; + + if (!hasRoleCheck && isPublic) { + violations.push({ + invariant: 'Access Control on Mint/Burn', + description: `Function '${func.name}' performs mint/burn operations with '${func.visibility}' visibility but no access control modifier (onlyRole, onlyOwner, etc.) was detected. This could allow unauthorized token minting.`, + path: `${func.contractName} → ${func.name}()`, + sourceLocation: `${func.filePath}:${func.line}`, + severity: 'critical', + category: 'access-control', + }); + } else if (!hasRoleCheck && !isPublic) { + violations.push({ + invariant: 'Access Control on Mint/Burn', + description: `Function '${func.name}' performs mint/burn operations with '${func.visibility}' visibility but no explicit access control was detected. Verify that callers enforce access control.`, + path: `${func.contractName} → ${func.name}()`, + sourceLocation: `${func.filePath}:${func.line}`, + severity: 'info', + category: 'access-control', + }); + } + + return violations; + } + + // ----------------------------------------------------------------------- + // Cross-contract solvency check + // + // Across all contracts, ensure there is at least one contract that + // enforces the solvency invariant (locked >= minted) at the system + // level — typically a VaultHealthEvaluator or equivalent. + // ----------------------------------------------------------------------- + + private checkCrossContractSolvency( + contracts: ParsedContract[], + ): InvariantViolation[] { + const violations: InvariantViolation[] = []; + + // Check if any contract explicitly enforces the locked >= minted invariant + const hasHealthCheck = contracts.some((c) => { + const allBodyText = c.functions.map((f) => f.body).join(' '); + return ( + /\blockedReserves\b.*\btotalSupply\b/.test(allBodyText) || + /\btotalLocked\b.*\btotalMinted\b/.test(allBodyText) || + /\btotalSupply\b.*\blockedReserves\b/.test(allBodyText) || + /collateralization/i.test(c.name) || + /health/i.test(c.name) || + /solvency/i.test(c.name) + ); + }); + + if (!hasHealthCheck) { + violations.push({ + invariant: 'Cross-Contract Solvency', + description: + 'No contract was detected that enforces the system-level solvency invariant (total locked reserves >= total minted wrapped supply). Consider adding an on-chain health checker like VaultHealthEvaluator.', + path: 'system-wide', + sourceLocation: contracts[0]?.filePath ?? 'unknown', + severity: 'warning', + category: 'solvency', + }); + } + + // Check if locked state variables exist but no minted counterpart (or vice versa) + for (const contract of contracts) { + const hasLockedVars = contract.stateVariables.some( + (v) => v.category === 'locked', + ); + const hasMintedVars = contract.stateVariables.some( + (v) => v.category === 'minted', + ); + + if (hasLockedVars && !hasMintedVars) { + violations.push({ + invariant: 'Cross-Contract Solvency', + description: `Contract '${contract.name}' tracks locked reserves but has no corresponding minted/wrapped token supply variable. Ensure the invariant is checked elsewhere.`, + path: `${contract.name}`, + sourceLocation: `${contract.filePath}:1`, + severity: 'info', + category: 'solvency', + }); + } + + if (!hasLockedVars && hasMintedVars) { + violations.push({ + invariant: 'Cross-Contract Solvency', + description: `Contract '${contract.name}' manages minted tokens but has no corresponding locked reserves variable. The solvency invariant (locked >= minted) cannot be verified within this contract.`, + path: `${contract.name}`, + sourceLocation: `${contract.filePath}:1`, + severity: 'warning', + category: 'solvency', + }); + } + } + + return violations; + } + + // ----------------------------------------------------------------------- + // Helpers + // ----------------------------------------------------------------------- + + /** + * Find functions across all contracts that call the given function and + * contain the specified type of operation. + * Uses word-boundary matching to avoid false substring matches. + */ + private findCallersWithOperation( + func: ContractFunction, + allContracts: ParsedContract[], + category: StateTransition['category'], + operation: StateTransition['operation'], + ): ContractFunction[] { + const callers: ContractFunction[] = []; + // Match function calls with word boundary: `funcName(` or `.funcName(` + const callPattern = new RegExp( + `(?:\\b|\\.)${this.escapeRegex(func.name)}\\s*\\(`, + ); + for (const contract of allContracts) { + for (const f of contract.functions) { + if (callPattern.test(f.body)) { + const hasOp = f.transitions.some( + (t) => t.category === category && t.operation === operation, + ); + if (hasOp) callers.push(f); + } + } + } + return callers; + } + + /** + * Escape regex special characters in a string. + */ + private escapeRegex(s: string): string { + return s.replace(/[.*+?^${}()|[\]\\]/g, '\\$&'); + } + + /** + * Determine if a mint operation is within a privileged context — i.e., + * the function has role-based access control that only the bridge vault + * can satisfy, which implies the lock already happened. + */ + private isPrivilegedContext( + func: ContractFunction, + _mint: StateTransition, + ): boolean { + // Check both modifiers (function signature) and body for access-control patterns + const combined = `${func.modifiersText} ${func.body}`; + return ( + /\bonlyRole\b/.test(combined) || + /\bMINTER_ROLE\b/.test(combined) || + /\bminter\b/i.test(combined) || + /\brequire\s*\(\s*hasRole/.test(combined) || + /\brequire\s*\(\s*msg\.sender\s*==\s*\w+[Vv]ault/.test(combined) + ); + } +} diff --git a/apps/cli/src/invariants/types.ts b/apps/cli/src/invariants/types.ts new file mode 100644 index 00000000..1462a422 --- /dev/null +++ b/apps/cli/src/invariants/types.ts @@ -0,0 +1,142 @@ +/** + * @module invariants/types + * @description Core type definitions for the static invariant checker. + */ + +/** Category of a state variable based on its role in bridge invariants. */ +export type StateVariableCategory = 'locked' | 'minted' | 'unknown'; + +/** A contract-level state variable relevant to bridge invariants. */ +export interface StateVariable { + /** Name of the variable (e.g. "lockedReserves", "_totalSupply"). */ + name: string; + /** Solidity type (e.g. "uint256", "mapping(address => uint256)"). */ + type: string; + /** Whether the variable tracks locked assets, minted supply, or is uncategorized. */ + category: StateVariableCategory; + /** The contract this variable belongs to. */ + contractName: string; + /** Source file path. */ + filePath: string; + /** Line number where declared. */ + line: number; +} + +/** Type of state-modifying operation. */ +export type OperationKind = 'add' | 'subtract'; + +/** Mapping of known operation signatures to their invariant category. */ +export interface OperationMapping { + /** Pattern to match (e.g. "_mint", "vault.lock"). */ + signature: string; + /** Category: does this increase locked or minted state? */ + category: StateVariableCategory; + /** Whether this adds or subtracts from the tracked amount. */ + kind: OperationKind; + /** Description for reporting. */ + description: string; +} + +/** A single state-modifying operation detected in a function body. */ +export interface StateTransition { + /** The operation kind. */ + operation: OperationKind; + /** Category of state affected. */ + category: StateVariableCategory; + /** Name of the operation (e.g. "_mint", "vault.lock"). */ + operationName: string; + /** The expression used for the amount (e.g. "amount", "tokenAmount"). */ + amountExpression: string; + /** The function where this transition occurs. */ + functionName: string; + /** The contract containing this function. */ + contractName: string; + /** Source file path. */ + filePath: string; + /** Line number. */ + line: number; + /** Context snippet of the source line. */ + context: string; +} + +/** A detected function definition within a contract. */ +export interface ContractFunction { + /** Function name. */ + name: string; + /** Visibility: public, external, internal, private. */ + visibility: string; + /** Whether the function is a view/pure (read-only). */ + isReadOnly: boolean; + /** Modifier text between params and body (e.g. 'external onlyRole(MINTER_ROLE) returns (bool)'). */ + modifiersText: string; + /** Full function body text. */ + body: string; + /** Contract this function belongs to. */ + contractName: string; + /** Source file path. */ + filePath: string; + /** Starting line number. */ + line: number; + /** Lines of code in the function body. */ + bodyLineCount: number; + /** State transitions detected in this function. */ + transitions: StateTransition[]; +} + +/** A parsed contract with its functions and state variables. */ +export interface ParsedContract { + /** Contract name. */ + name: string; + /** Source file path. */ + filePath: string; + /** State variables relevant to invariants. */ + stateVariables: StateVariable[]; + /** Functions defined in the contract. */ + functions: ContractFunction[]; + /** Inherited contracts detected from `is` clause. */ + inherits: string[]; + /** Total lines in the file. */ + lineCount: number; +} + +/** A single invariant violation detected during analysis. */ +export interface InvariantViolation { + /** The specific invariant being violated. */ + invariant: string; + /** Human-readable description of the violation. */ + description: string; + /** The execution path (contract → function chain) where the violation occurs. */ + path: string; + /** Source location: file:line. */ + sourceLocation: string; + /** Severity of the violation. */ + severity: 'critical' | 'warning' | 'info'; + /** The category of the invariant. */ + category: 'solvency' | 'conservative-minting' | 'access-control'; +} + +/** Result of running invariant checks on a set of contracts. */ +export interface InvariantCheckResult { + /** Whether all invariants are satisfied. */ + allInvariantsSatisfied: boolean; + /** Total number of contracts analyzed. */ + contractsAnalyzed: number; + /** Total number of functions analyzed. */ + functionsAnalyzed: number; + /** Total number of state transitions detected. */ + transitionsDetected: number; + /** List of invariant violations found. */ + violations: InvariantViolation[]; + /** Summary message. */ + summary: string; + /** Per-contract detailed analysis. */ + contractDetails: Array<{ + contractName: string; + filePath: string; + functionsScanned: number; + lockedVariables: string[]; + mintedVariables: string[]; + transitions: number; + violations: number; + }>; +} diff --git a/apps/cli/src/main.ts b/apps/cli/src/main.ts index 4e2be75e..71723adc 100644 --- a/apps/cli/src/main.ts +++ b/apps/cli/src/main.ts @@ -5,6 +5,7 @@ import { CongestionCommand } from './commands/congestion.command'; import { CompareCommand } from './commands/compare.command'; import { StatusCommand } from './commands/status.command'; import { HelpCommand } from './commands/help.command'; +import { CheckInvariantsCommand } from './commands/check-invariants.command'; import { CommandRunner } from './commands/command-runner'; declare const process: { argv: string[]; exit(code?: number): void }; @@ -18,6 +19,7 @@ async function bootstrap(): Promise { const compareCommand = new CompareCommand(); const statusCommand = new StatusCommand(); const helpCommand = new HelpCommand(); + const checkInvariantsCommand = new CheckInvariantsCommand(); const runner = new CommandRunner( historyCommand, @@ -26,11 +28,31 @@ async function bootstrap(): Promise { compareCommand, statusCommand, helpCommand, + checkInvariantsCommand, ); runner.onModuleInit(); const output = await runner.run(process.argv); console.log(output); + + // For CI/CD integration: exit with code 1 when the check-invariants command + // detects violations (fail-on-violations defaults to true). Parse the JSON + // output to determine exit code when the command ran with violations. + const { commandName } = runner.parseArgv(process.argv); + if (commandName === 'check-invariants' || commandName === 'invariants' || commandName === 'verify-invariants') { + try { + const result = JSON.parse(output); + if (result && result.success === false) { + process.exit(1); + } + } catch { + // Not JSON output; try text-based detection + if (output.startsWith('[ERROR]')) { + process.exit(1); + } + } + } + return output; }