From 3c7a473b66e13393f441ad3f6614fa97c529f2fb Mon Sep 17 00:00:00 2001 From: g4titanx Date: Fri, 3 Apr 2026 21:16:40 +0100 Subject: [PATCH] refactor: rm old archi and update readme for new system --- crates/verification/README.md | 42 +- crates/verification/src/lib.rs | 285 ------ crates/verification/src/proofs.rs | 192 ---- crates/verification/src/properties.rs | 144 --- crates/verification/src/result.rs | 23 - crates/verification/src/semantics.rs | 1318 ------------------------- crates/verification/src/smt.rs | 901 ----------------- 7 files changed, 3 insertions(+), 2902 deletions(-) delete mode 100644 crates/verification/src/proofs.rs delete mode 100644 crates/verification/src/properties.rs delete mode 100644 crates/verification/src/result.rs delete mode 100644 crates/verification/src/semantics.rs delete mode 100644 crates/verification/src/smt.rs diff --git a/crates/verification/README.md b/crates/verification/README.md index 7bcbc8e6..ed84afee 100644 --- a/crates/verification/README.md +++ b/crates/verification/README.md @@ -1,41 +1,5 @@ -## azoth-verification +# Azoth's Formal Verification Engine -This crate provides mathematical guarantees that obfuscated smart contracts behave identically to their original versions. When we obfuscate bytecode, we fundamentally alter its structure while preserving functionality. Formal verification uses mathematical proofs to ensure this preservation is complete and correct. +The purpose of this verification system is to establish functional equivalence between original EVM bytecode and the bytecode produced after Azoth applies one or more obfuscation transforms. In this context, functional equivalence means that the transformed contract preserves the observable behavior of the original contract under the chosen EVM semantics, including execution outcome, returned data, and resulting state changes. -Traditional testing can only verify specific cases, but smart contracts must handle infinite input combinations. A single undetected difference between original and obfuscated contracts could compromise security or functionality. Formal verification provides mathematical certainty that the contracts are equivalent for **all possible inputs**, not just tested ones. - -We use SMT-LIB (Satisfiability Modulo Theories) as our mathematical language to express contract properties, and Z3 theorem prover to automatically verify these properties. This serves as link between low-level bytecode and high-level mathematical reasoning. - -Now our verification establishes four key equivalence properties: - -- Bisimulation -```smt -(assert (forall ((state State) (input Input)) - (= (execute-original state input) - (execute-obfuscated state input)))) -``` -For EVERY input and state, both contracts produce the same execution trace. - -- State Equivalence -```smt -(assert (forall ((initial-state State) (transaction Tx)) - (= (final-state (execute-original initial-state transaction)) - (final-state (execute-obfuscated initial-state transaction))))) -``` -After ANY transaction, the storage, balances, and contract state are identical between original and obfuscated versions. - -- Property Preservation -```smt -(assert (forall ((s State)) - (and (access-control-original s) - (access-control-obfuscated s)))) -``` -ALL security properties satisfied by original are satisfied by obfuscated. - -- Gas Bounds -```smt -(assert (forall ((tx Transaction)) - (<= (gas-used (execute-obfuscated tx)) - (* 1.15 (gas-used (execute-original tx)))))) -``` -For ANY transaction, obfuscated version uses at most 15% more gas. +Its role is to justify that Azoth's transformations preserve behavior beyond the concrete cases exercised by testing, so that semantic preservation becomes a property the pipeline can defend rather than merely sample. The verification engine therefore exists as the correctness foundation for accepting or rejecting transformed bytecode. diff --git a/crates/verification/src/lib.rs b/crates/verification/src/lib.rs index e0772301..ebf88383 100644 --- a/crates/verification/src/lib.rs +++ b/crates/verification/src/lib.rs @@ -1,286 +1 @@ //! Azoth's Formal Verification Engine -//! -//! This crate provides formal guarantees that obfuscated contracts are functionally -//! equivalent to their original versions through formal verification using SMT solvers. - -pub mod proofs; -pub mod properties; -pub mod result; -pub mod semantics; -pub mod smt; - -pub use proofs::{FormalProof, ProofStatement, ProofType}; -pub use properties::{ArithmeticOperation, SecurityProperty}; -pub use result::{Error, Result}; - -use std::time::Instant; - -/// Result type for verification operations (alias for backward compatibility) -pub type VerificationResult = Result; - -/// Main formal verification engine -#[derive(Debug)] -pub struct FormalVerifier { - #[allow(dead_code)] - smt_solver: smt::SmtSolver, -} - -impl FormalVerifier { - /// Create a new formal verifier - pub fn new() -> VerificationResult { - let smt_solver = smt::SmtSolver::new()?; - - Ok(Self { smt_solver }) - } - - /// Main entry point: prove that two contracts are equivalent - pub async fn prove_equivalence( - &mut self, - original_bytecode: &[u8], - original_runtime: &[u8], - obfuscated_bytecode: &[u8], - obfuscated_runtime: &[u8], - security_properties: &[SecurityProperty], - ) -> VerificationResult { - let start_time = Instant::now(); - - tracing::info!("Starting formal verification of contract equivalence"); - - // Parse both contracts into semantic representations - let original_semantics = - semantics::extract_semantics_from_bytecode(original_bytecode, original_runtime).await?; - let obfuscated_semantics = - semantics::extract_semantics_from_bytecode(obfuscated_bytecode, obfuscated_runtime) - .await?; - - tracing::debug!("Extracted semantics for both contracts"); - - // Generate proof statements - let mut statements = Vec::new(); - - // 1. Prove bisimulation (step-by-step equivalence) - if let Ok(bisim_statement) = self - .prove_bisimulation(&original_semantics, &obfuscated_semantics) - .await - { - statements.push(bisim_statement); - } - - // 2. Prove state equivalence - if let Ok(state_statement) = self - .prove_state_equivalence(&original_semantics, &obfuscated_semantics) - .await - { - statements.push(state_statement); - } - - // 3. Prove property preservation - for property in security_properties { - if let Ok(prop_statement) = self - .prove_property_preservation(&original_semantics, &obfuscated_semantics, property) - .await - { - statements.push(prop_statement); - } - } - - // 4. Prove gas bounds - if let Ok(gas_statement) = self - .prove_gas_bounds(&original_semantics, &obfuscated_semantics) - .await - { - statements.push(gas_statement); - } - - let proof_time = start_time.elapsed(); - let _statements_clone = statements.clone(); // Clone for hash computation - - let proof = FormalProof::new( - ProofType::Combined(vec![ - ProofType::Bisimulation, - ProofType::StateEquivalence, - ProofType::PropertyPreservation, - ProofType::GasBounds, - ]), - statements, - proof_time, - ); - - tracing::info!( - "Formal verification completed in {:.2}s, valid: {}", - proof_time.as_secs_f64(), - proof.valid - ); - - Ok(proof) - } - - /// Prove bisimulation: every execution step is equivalent - async fn prove_bisimulation( - &mut self, - _original: &semantics::ContractSemantics, - _obfuscated: &semantics::ContractSemantics, - ) -> VerificationResult { - let start_time = Instant::now(); - - tracing::debug!("Proving bisimulation between contracts"); - - // Create bisimulation assertion - let bisim_formula = "(assert (forall ((state State) (input Input)) - (= (execute-original state input) - (execute-obfuscated state input))))" - .to_string(); - - // TODO: Implement actual SMT verification - let proven = true; // Placeholder - let proof_time = start_time.elapsed(); - - Ok(ProofStatement::new( - "Bisimulation: Every execution step produces identical results".to_string(), - bisim_formula, - proven, - proof_time, - )) - } - - /// Prove state equivalence: final states are identical - async fn prove_state_equivalence( - &mut self, - _original: &semantics::ContractSemantics, - _obfuscated: &semantics::ContractSemantics, - ) -> VerificationResult { - let start_time = Instant::now(); - - tracing::debug!("Proving state equivalence between contracts"); - - let state_equiv_formula = "(assert (forall ((initial-state State) (transaction Tx)) - (= (final-state (execute-original initial-state transaction)) - (final-state (execute-obfuscated initial-state transaction)))))" - .to_string(); - - // TODO: Implement actual SMT verification - let proven = true; - let proof_time = start_time.elapsed(); - - Ok(ProofStatement::new( - "State Equivalence: Final contract states are identical".to_string(), - state_equiv_formula, - proven, - proof_time, - )) - } - - /// Prove that security properties are preserved - async fn prove_property_preservation( - &mut self, - _original: &semantics::ContractSemantics, - _obfuscated: &semantics::ContractSemantics, - property: &SecurityProperty, - ) -> VerificationResult { - let start_time = Instant::now(); - - let description = property.description(); - let formal_statement = property.to_smt_formula(); - - // TODO: Implement actual property verification - let proven = true; - let proof_time = start_time.elapsed(); - - Ok(ProofStatement::new( - description, - formal_statement, - proven, - proof_time, - )) - } - - /// Prove gas consumption bounds - async fn prove_gas_bounds( - &mut self, - _original: &semantics::ContractSemantics, - _obfuscated: &semantics::ContractSemantics, - ) -> VerificationResult { - let start_time = Instant::now(); - - tracing::debug!("Proving gas consumption bounds"); - - let gas_bound_formula = "(assert (forall ((input Input)) - (<= (gas-consumed (execute-obfuscated input)) - (* 1.15 (gas-consumed (execute-original input))))))" - .to_string(); - - // TODO: Implement actual gas bounds verification - let proven = true; - let proof_time = start_time.elapsed(); - - Ok(ProofStatement::new( - "Gas Bounds: Obfuscated contract uses at most 15% more gas".to_string(), - gas_bound_formula, - proven, - proof_time, - )) - } -} - -/// Information about a transform that was applied during obfuscation -#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)] -pub struct TransformInfo { - pub name: String, - pub parameters: serde_json::Value, - pub order: usize, -} - -/// Summary of verification results for quick inspection -#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)] -pub struct VerificationSummary { - pub overall_passed: bool, - pub formal_verification_passed: bool, - pub verification_time_ms: u64, -} - -#[cfg(test)] -mod tests { - use super::*; - use std::time::Duration; - - #[tokio::test] - async fn test_formal_verifier_creation() { - let verifier = FormalVerifier::new(); - - // Should create successfully (even if SMT solver not available) - assert!(verifier.is_ok() || matches!(verifier.unwrap_err(), Error::SmtSolver(_))); - } - - #[test] - fn test_security_property_encoding() { - let function_sel = [0x12, 0x34, 0x56, 0x78]; - let authorized = vec![[0xaa; 20], [0xbb; 20]]; - let property = SecurityProperty::AccessControl { - function_selector: function_sel, - authorized_callers: authorized, - }; - - let formula = property.to_smt_formula(); - assert!(formula.contains("12345678")); - assert!(formula.contains("aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa")); - } - - #[test] - fn test_proof_hash_computation() { - let statements = vec![ProofStatement::new( - "Test".to_string(), - "(assert true)".to_string(), - true, - Duration::from_millis(100), - )]; - - let proof = FormalProof::new( - ProofType::Bisimulation, - statements, - Duration::from_millis(100), - ); - - // Hash should be deterministic - assert_eq!(proof.proof_hash.len(), 64); // SHA3-256 produces 32 bytes = 64 hex chars - } -} diff --git a/crates/verification/src/proofs.rs b/crates/verification/src/proofs.rs deleted file mode 100644 index 4d3297a6..00000000 --- a/crates/verification/src/proofs.rs +++ /dev/null @@ -1,192 +0,0 @@ -//! Mathematical proof structures and operations - -use serde::{Deserialize, Serialize}; -use sha3::{Digest, Sha3_256}; -use std::time::Duration; - -/// A formal mathematical proof of contract equivalence -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct FormalProof { - /// Type of proof generated - pub proof_type: ProofType, - /// Mathematical statements proven - pub statements: Vec, - /// Time taken to generate the proof - pub proof_time: Duration, - /// Whether the proof is valid - pub valid: bool, - /// Hash of the proof for integrity verification - pub proof_hash: String, -} - -/// Types of formal proofs we can generate -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum ProofType { - /// Bisimulation proof showing step-by-step equivalence - Bisimulation, - /// State equivalence proof showing identical final states - StateEquivalence, - /// Property preservation proof showing security properties are maintained - PropertyPreservation, - /// Gas bounds proof showing gas consumption is bounded - GasBounds, - /// Combined proof encompassing multiple proof types - Combined(Vec), -} - -/// A mathematical statement that has been proven -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct ProofStatement { - /// Human-readable description of what was proven - pub description: String, - /// Formal mathematical statement (in SMT-LIB format) - pub formal_statement: String, - /// Whether this statement was successfully proven - pub proven: bool, - /// Time taken to prove this statement - pub proof_time: Duration, -} - -impl FormalProof { - /// Create a new formal proof - pub fn new( - proof_type: ProofType, - statements: Vec, - proof_time: Duration, - ) -> Self { - let valid = statements.iter().all(|s| s.proven); - let proof_hash = Self::compute_hash(&statements); - - Self { - proof_type, - statements, - proof_time, - valid, - proof_hash, - } - } - - /// Compute hash of the proof for integrity verification - fn compute_hash(statements: &[ProofStatement]) -> String { - let mut hasher = Sha3_256::new(); - for statement in statements { - hasher.update(statement.formal_statement.as_bytes()); - hasher.update(statement.proven.to_string().as_bytes()); - } - hex::encode(hasher.finalize()) - } - - /// Get the number of proven statements - pub fn proven_statements_count(&self) -> usize { - self.statements.iter().filter(|s| s.proven).count() - } - - /// Get the total number of statements - pub fn total_statements_count(&self) -> usize { - self.statements.len() - } - - /// Get proof success rate - pub fn success_rate(&self) -> f64 { - if self.statements.is_empty() { - 0.0 - } else { - self.proven_statements_count() as f64 / self.total_statements_count() as f64 - } - } - - /// Combine multiple proofs into one - pub fn combine(proofs: Vec) -> Self { - let mut all_statements = Vec::new(); - let mut total_time = Duration::default(); - let mut proof_types = Vec::new(); - - for proof in proofs { - all_statements.extend(proof.statements); - total_time += proof.proof_time; - proof_types.push(proof.proof_type); - } - - Self::new(ProofType::Combined(proof_types), all_statements, total_time) - } -} - -impl ProofStatement { - /// Create a new proof statement - pub fn new( - description: String, - formal_statement: String, - proven: bool, - proof_time: Duration, - ) -> Self { - Self { - description, - formal_statement, - proven, - proof_time, - } - } - - /// Create a successful proof statement - pub fn proven(description: String, formal_statement: String, proof_time: Duration) -> Self { - Self::new(description, formal_statement, true, proof_time) - } - - /// Create a failed proof statement - pub fn failed(description: String, formal_statement: String, proof_time: Duration) -> Self { - Self::new(description, formal_statement, false, proof_time) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[test] - fn test_proof_creation() { - let statements = vec![ProofStatement::proven( - "Test statement".to_string(), - "(assert true)".to_string(), - Duration::from_millis(100), - )]; - - let proof = FormalProof::new( - ProofType::Bisimulation, - statements, - Duration::from_millis(100), - ); - - assert!(proof.valid); - assert_eq!(proof.proven_statements_count(), 1); - assert_eq!(proof.success_rate(), 1.0); - } - - #[test] - fn test_proof_combination() { - let proof1 = FormalProof::new( - ProofType::Bisimulation, - vec![ProofStatement::proven( - "Test 1".to_string(), - "(assert true)".to_string(), - Duration::from_millis(50), - )], - Duration::from_millis(50), - ); - - let proof2 = FormalProof::new( - ProofType::StateEquivalence, - vec![ProofStatement::proven( - "Test 2".to_string(), - "(assert (= a b))".to_string(), - Duration::from_millis(75), - )], - Duration::from_millis(75), - ); - - let combined = FormalProof::combine(vec![proof1, proof2]); - - assert_eq!(combined.total_statements_count(), 2); - assert_eq!(combined.proof_time, Duration::from_millis(125)); - assert!(matches!(combined.proof_type, ProofType::Combined(_))); - } -} diff --git a/crates/verification/src/properties.rs b/crates/verification/src/properties.rs deleted file mode 100644 index fb959134..00000000 --- a/crates/verification/src/properties.rs +++ /dev/null @@ -1,144 +0,0 @@ -//! Security property definitions and verification - -use serde::{Deserialize, Serialize}; - -/// Security properties that must be preserved during obfuscation -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum SecurityProperty { - /// Access control: Who can call which functions - AccessControl { - function_selector: [u8; 4], - authorized_callers: Vec<[u8; 20]>, // Ethereum addresses - }, - /// State invariant: Conditions that must always hold - StateInvariant { - name: String, - invariant_formula: String, // SMT-LIB format - }, - /// Reentrancy protection: Functions protected against reentrancy - ReentrancyProtection { protected_functions: Vec<[u8; 4]> }, - /// Arithmetic overflow protection - ArithmeticSafety { - operations: Vec, - }, - /// Custom property with SMT formula - Custom { - name: String, - property_formula: String, - }, -} - -/// Arithmetic operations that need overflow protection -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum ArithmeticOperation { - Addition, - Subtraction, - Multiplication, - Division, - Modulo, -} - -impl SecurityProperty { - /// Convert property to SMT-LIB formula - pub fn to_smt_formula(&self) -> String { - match self { - SecurityProperty::AccessControl { - function_selector, - authorized_callers, - } => { - let selector_hex = hex::encode(function_selector); - let callers: Vec = authorized_callers - .iter() - .map(|address| format!("0x{}", hex::encode(address))) - .collect(); - - format!( - "(assert (forall ((caller Address) (input Input)) - (=> (= (function-selector input) #x{}) - (member caller (list {})))))", - selector_hex, - callers.join(" ") - ) - } - SecurityProperty::StateInvariant { - name: _, - invariant_formula, - } => invariant_formula.clone(), - SecurityProperty::ReentrancyProtection { - protected_functions, - } => { - let selectors: Vec = protected_functions - .iter() - .map(|selector| format!("#x{}", hex::encode(selector))) - .collect(); - - format!( - "(assert (forall ((call-stack CallStack) (function-sel FunctionSelector)) - (=> (member function-sel (list {})) - (not (contains-reentrant-call call-stack function-sel)))))", - selectors.join(" ") - ) - } - SecurityProperty::ArithmeticSafety { operations } => { - let ops: Vec<&str> = operations - .iter() - .map(|op| match op { - ArithmeticOperation::Addition => "add", - ArithmeticOperation::Subtraction => "sub", - ArithmeticOperation::Multiplication => "mul", - ArithmeticOperation::Division => "div", - ArithmeticOperation::Modulo => "mod", - }) - .collect(); - - format!( - "(assert (forall ((a Int) (b Int) (op Operation)) - (=> (member op (list {})) - (and (>= (apply-op op a b) 0) - (< (apply-op op a b) (^ 2 256))))))", - ops.join(" ") - ) - } - SecurityProperty::Custom { - name: _, - property_formula, - } => property_formula.clone(), - } - } - - /// Get a human-readable description of the property - pub fn description(&self) -> String { - match self { - SecurityProperty::AccessControl { - function_selector, - authorized_callers, - } => { - format!( - "Access Control: Function 0x{} restricted to {} authorized callers", - hex::encode(function_selector), - authorized_callers.len() - ) - } - SecurityProperty::StateInvariant { name, .. } => { - format!("State Invariant: {name}") - } - SecurityProperty::ReentrancyProtection { - protected_functions, - } => { - format!( - "Reentrancy Protection: {} functions protected", - protected_functions.len() - ) - } - SecurityProperty::ArithmeticSafety { operations } => { - format!( - "Arithmetic Safety: {} operations protected from overflow", - operations.len() - ) - } - SecurityProperty::Custom { name, .. } => { - format!("Custom Property: {name}") - } - } - } -} diff --git a/crates/verification/src/result.rs b/crates/verification/src/result.rs deleted file mode 100644 index e175ea11..00000000 --- a/crates/verification/src/result.rs +++ /dev/null @@ -1,23 +0,0 @@ -//! Verification results and error types - -use thiserror::Error; - -/// Main error type for verification operations -#[derive(Error, Debug)] -pub enum Error { - #[error("SMT solver error: {0}")] - SmtSolver(String), - #[error("Verification timeout after {seconds} seconds")] - Timeout { seconds: u64 }, - #[error("Bytecode analysis failed: {0}")] - BytecodeAnalysis(String), - #[error("Property verification failed: {property}")] - PropertyFailed { property: String }, - #[error("IO error: {0}")] - Io(#[from] std::io::Error), - #[error("Serialization error: {0}")] - Serialization(#[from] serde_json::Error), -} - -/// Result type for verification operations -pub type Result = std::result::Result; diff --git a/crates/verification/src/semantics.rs b/crates/verification/src/semantics.rs deleted file mode 100644 index 23dbafd6..00000000 --- a/crates/verification/src/semantics.rs +++ /dev/null @@ -1,1318 +0,0 @@ -//! Contract semantics extraction and representation -//! -//! This module analyzes bytecode to extract semantic information needed for formal verification -//! by leveraging pattern recognition, symbolic execution, and property synthesis. - -use crate::{Error, VerificationResult}; -use azoth_core::cfg_ir::{Block, CfgIrBundle, EdgeType}; -use azoth_core::decoder::Instruction; -use azoth_core::{cfg_ir, decoder, detection, strip, Opcode}; -use petgraph::visit::EdgeRef; -use serde::{Deserialize, Serialize}; -use std::collections::{HashMap, HashSet, VecDeque}; -use tracing; - -/// Stack value for symbolic execution -#[derive(Debug, Clone, PartialEq)] -pub enum StackValue { - /// Concrete value from PUSH instruction - Concrete(u64), - /// Symbolic value (e.g., from CALLDATALOAD) - Symbolic(String), - /// Result of an operation - Operation { - op: String, - operands: Vec>, - }, - /// Storage load result - StorageLoad(Box), - /// Unknown/top value - Unknown, -} - -/// Path condition for conditional execution -#[derive(Debug, Clone)] -pub struct PathCondition { - /// SMT formula representing the condition - pub formula: String, - /// Whether this is a positive or negative condition - pub polarity: bool, - /// Source instruction PC - pub source_pc: usize, -} - -/// Storage access pattern -#[derive(Debug, Clone)] -pub struct StorageAccess { - /// Program counter of the access - pub pc: usize, - /// Computed storage slot - pub slot: StackValue, - /// Access type (SLOAD or SSTORE) - pub access_type: StorageAccessType, - /// Value being stored (for SSTORE) - pub stored_value: Option, - /// Path conditions leading to this access - pub conditions: Vec, -} - -#[derive(Debug, Clone, PartialEq)] -pub enum StorageAccessType { - Load, - Store, -} - -/// Contract pattern recognition -#[derive(Debug, Clone)] -pub struct ContractPattern { - /// Pattern type (ERC20, ERC721, etc.) - pub pattern_type: PatternType, - /// Confidence score (0.0 to 1.0) - pub confidence: f64, - /// Supporting evidence - pub evidence: Vec, -} - -#[derive(Debug, Clone, PartialEq)] -pub enum PatternType { - ERC20Token, - ERC721NFT, - Ownable, - ReentrancyGuard, - SafeMath, - Proxy, - Multisig, - Unknown, -} - -#[derive(Debug, Clone)] -pub struct PatternEvidence { - /// Type of evidence found - pub evidence_type: String, - /// Location in bytecode - pub pc: usize, - /// Supporting details - pub details: String, -} - -/// Semantic representation of a smart contract -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct ContractSemantics { - /// Contract functions with their properties - pub functions: Vec, // what the contract can do - /// Storage layout mapping - pub storage_layout: HashMap, // slot -> type (how data is stored) - /// Global state invariants - pub state_invariants: Vec, // SMT formulas (what must always be true) - /// Contract-level properties - pub properties: ContractProperties, // security characteristics - /// Reference to the CFG for analysis - pub cfg_metadata: CfgMetadata, -} - -/// Metadata extracted from the CFG for semantic analysis -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct CfgMetadata { - /// Number of basic blocks in the CFG - pub block_count: usize, - /// Number of edges in the CFG - pub edge_count: usize, - /// Entry points (function selectors to block start PCs) - pub entry_points: HashMap<[u8; 4], usize>, - /// Block summaries for analysis - pub block_summaries: Vec, -} - -/// Summary of a basic block for semantic analysis -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct BlockSummary { - /// Block identifier (PC of first instruction) - pub start_pc: usize, - /// Number of instructions in this block - pub instruction_count: usize, - /// Block type based on terminating instruction - pub block_type: BlockType, - /// Opcodes in this block (using enum instead of strings) - pub opcodes: Vec, - /// Maximum stack height reached in this block - pub max_stack: usize, - /// Incoming edge types - pub incoming_edges: Vec, - /// Outgoing edge types - pub outgoing_edges: Vec, -} - -/// Semantic representation of a contract function -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct FunctionSemantics { - /// Function name (if known) - pub name: String, - /// Function selector (first 4 bytes of keccak hash) - pub selector: Option<[u8; 4]>, - /// Function preconditions (SMT formulas) - pub preconditions: Vec, - /// Function postconditions (SMT formulas) - pub postconditions: Vec, - /// State modifications this function can make - pub state_modifications: Vec, - /// Gas consumption characteristics - pub gas_characteristics: GasCharacteristics, - /// Whether this function is view/pure - pub read_only: bool, - /// Whether this function is payable - pub payable: bool, - /// Basic blocks that belong to this function - pub block_pcs: Vec, -} - -/// Description of how a function modifies contract state -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct StateModification { - /// Storage slot being modified - pub storage_slot: u64, - /// Type of modification - pub modification_type: ModificationType, - /// Conditions under which modification occurs - pub conditions: Vec, // SMT formulas -} - -/// Types of state modifications -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum ModificationType { - /// Direct assignment - Assignment, - /// Increment/decrement - Arithmetic, - /// Conditional update - Conditional, - /// Array/mapping update - Collection, -} - -/// Gas consumption characteristics of a function -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct GasCharacteristics { - /// Base gas cost (fixed part) - pub base_cost: u64, - /// Variable gas cost factors - pub variable_costs: Vec, - /// Maximum possible gas consumption - pub max_gas: Option, -} - -/// Variable gas cost component -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct VariableGasCost { - /// What drives this variable cost - pub factor: GasCostFactor, - /// Cost per unit - pub cost_per_unit: u64, -} - -/// Factors that affect gas consumption -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum GasCostFactor { - /// Input data size - InputDataSize, - /// Storage operations - StorageOperations, - /// Loop iterations - LoopIterations, - /// External calls - ExternalCalls, -} - -/// Contract-level properties -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct ContractProperties { - /// Whether the contract uses a proxy pattern - pub is_proxy: bool, - /// Whether the contract is upgradeable - pub is_upgradeable: bool, - /// Reentrancy guards present - pub has_reentrancy_guards: bool, - /// Access control mechanisms - pub access_control: AccessControlType, -} - -/// Types of access control -#[derive(Debug, Clone, Serialize, Deserialize)] -pub enum AccessControlType { - /// No access control - None, - /// Simple owner-based control - Owner, - /// Role-based access control - RoleBased, - /// Custom access control - Custom, -} - -/// Types of basic blocks based on their terminating instruction -#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] -pub enum BlockType { - /// Function entry point - Entry, - /// Regular execution block - Normal, - /// Conditional branch - Branch, - /// Function return - Return, - /// Error/revert - Error, - /// Unconditional jump - Jump, -} - -/// Extract semantic information from a CFG bundle -pub fn extract_semantics(cfg_bundle: &CfgIrBundle) -> VerificationResult { - tracing::debug!("Extracting semantics from CFG bundle"); - - let mut analyzer = SemanticAnalyzer::new(cfg_bundle.clone()); - analyzer.analyze()?; - analyzer.extract_semantics_from_cfg() -} - -/// Extract semantic information from bytecode -pub async fn extract_semantics_from_bytecode( - bytecode: &[u8], - runtime_bytes: &[u8], -) -> VerificationResult { - tracing::debug!( - "Extracting semantics from bytecode ({} bytes)", - bytecode.len() - ); - - let (instructions, _, _, _) = - decoder::decode_bytecode(&format!("0x{}", hex::encode(bytecode)), false) - .await - .map_err(|e| Error::BytecodeAnalysis(format!("Failed to decode bytecode: {e}")))?; - - let sections = detection::locate_sections(bytecode, &instructions, runtime_bytes) - .map_err(|e| Error::BytecodeAnalysis(format!("Failed to detect sections: {e}")))?; - - let (_clean_runtime, clean_report) = strip::strip_bytecode(bytecode, §ions) - .map_err(|e| Error::BytecodeAnalysis(format!("Failed to strip bytecode: {e}")))?; - - let cfg_bundle = cfg_ir::build_cfg_ir(&instructions, §ions, clean_report, bytecode) - .map_err(|e| Error::BytecodeAnalysis(format!("Failed to build CFG: {e}")))?; - - extract_semantics(&cfg_bundle) -} - -/// Semantic analyzer capable of deep bytecode analysis -pub struct SemanticAnalyzer { - /// CFG bundle for analysis - cfg_bundle: CfgIrBundle, - /// Storage access patterns found - storage_accesses: Vec, - /// Detected contract patterns - patterns: Vec, -} - -impl SemanticAnalyzer { - /// Create new analyzer instance - pub fn new(cfg_bundle: CfgIrBundle) -> Self { - Self { - cfg_bundle, - storage_accesses: Vec::new(), - patterns: Vec::new(), - } - } - - /// Perform comprehensive semantic analysis - pub fn analyze(&mut self) -> VerificationResult<()> { - tracing::info!("Starting semantic analysis"); - - // Analyze storage access patterns with symbolic execution - self.analyze_storage_patterns()?; - - // Detect contract patterns (ERC20, Ownable, etc.) - self.detect_contract_patterns()?; - - // Perform symbolic execution on critical paths - self.symbolic_execution_analysis()?; - - tracing::info!("Semantic analysis completed"); - Ok(()) - } - - /// Extract semantic information from CFG - pub fn extract_semantics_from_cfg(&self) -> VerificationResult { - let cfg_metadata = self.extract_cfg_metadata()?; - let functions = self.extract_functions()?; - let storage_layout = self.analyze_storage_layout()?; - let properties = self.analyze_contract_properties()?; - let state_invariants = self.extract_state_invariants(&functions, &storage_layout)?; - - Ok(ContractSemantics { - functions, - storage_layout, - state_invariants, - properties, - cfg_metadata, - }) - } - - /// Extract CFG metadata for analysis - fn extract_cfg_metadata(&self) -> VerificationResult { - let cfg = &self.cfg_bundle.cfg; - let mut entry_points = HashMap::new(); - let mut block_summaries = Vec::new(); - - // Extract semantic information from existing CFG blocks - for node_idx in cfg.node_indices() { - if let Some(Block::Body(body)) = cfg.node_weight(node_idx) { - let start_pc = body.start_pc; - let instructions = &body.instructions; - let max_stack = body.max_stack; - // Extract function selectors (semantic analysis) - if let Some(selector) = - self.extract_function_selector_from_instructions(instructions) - { - entry_points.insert(selector, start_pc); - } - - // Extract opcodes from instructions - let opcodes: Vec = instructions.iter().map(|i| i.op).collect(); - - // Determine block type using enum comparison - let block_type = if instructions.is_empty() { - BlockType::Normal - } else { - match instructions.last().unwrap().op { - Opcode::RETURN => BlockType::Return, - Opcode::REVERT => BlockType::Error, - Opcode::JUMP => BlockType::Jump, - Opcode::JUMPI => BlockType::Branch, - _ => { - if matches!(instructions.first().map(|i| i.op), Some(Opcode::JUMPDEST)) - { - BlockType::Entry - } else { - BlockType::Normal - } - } - } - }; - - // Use CFG's existing edge information - let incoming_edges: Vec = cfg - .edges_directed(node_idx, petgraph::Direction::Incoming) - .map(|edge| edge.weight().clone()) - .collect(); - - let outgoing_edges: Vec = cfg - .edges_directed(node_idx, petgraph::Direction::Outgoing) - .map(|edge| edge.weight().clone()) - .collect(); - - block_summaries.push(BlockSummary { - start_pc, - instruction_count: instructions.len(), - block_type, - opcodes, - max_stack, - incoming_edges, - outgoing_edges, - }); - } - } - - Ok(CfgMetadata { - block_count: cfg.node_count(), - edge_count: cfg.edge_count(), - entry_points, - block_summaries, - }) - } - - fn extract_functions(&self) -> VerificationResult> { - let mut functions = Vec::new(); - let cfg_metadata = self.extract_cfg_metadata()?; - - // For each entry point, analyze the reachable blocks as a function - for (selector, start_pc) in &cfg_metadata.entry_points { - let function = self.analyze_function(*selector, *start_pc)?; - functions.push(function); - } - - // If no entry points found, create a single function for the entire contract - if functions.is_empty() { - let function = self.create_fallback_function(&cfg_metadata)?; - functions.push(function); - } - - Ok(functions) - } - - /// Analyze a single function with sophisticated analysis - fn analyze_function( - &self, - selector: [u8; 4], - start_pc: usize, - ) -> VerificationResult { - let function_name = format!("function_{}", hex::encode(selector)); - - // Find all blocks reachable from the start_pc - let reachable_blocks = self.find_reachable_blocks_in_cfg(start_pc)?; - let block_pcs: Vec = reachable_blocks.to_vec(); - - // Analyze state modifications across all reachable blocks - let state_modifications = self.analyze_state_modifications_in_blocks(&reachable_blocks)?; - - // Analyze gas characteristics - let gas_characteristics = self.analyze_gas_characteristics_in_blocks(&reachable_blocks)?; - - // Determine function properties - let (read_only, payable) = self.analyze_function_properties_in_blocks(&reachable_blocks)?; - - // Generate sophisticated preconditions and postconditions - let preconditions = self.generate_preconditions(&selector, &state_modifications)?; - let postconditions = self.generate_postconditions(&selector, &state_modifications)?; - - Ok(FunctionSemantics { - name: function_name, - selector: Some(selector), - preconditions, - postconditions, - state_modifications, - gas_characteristics, - read_only, - payable, - block_pcs, - }) - } - - fn create_fallback_function( - &self, - cfg_metadata: &CfgMetadata, - ) -> VerificationResult { - let all_block_pcs: Vec = cfg_metadata - .block_summaries - .iter() - .map(|b| b.start_pc) - .collect(); - let state_modifications = self.analyze_state_modifications_in_blocks(&all_block_pcs)?; - let gas_characteristics = self.analyze_gas_characteristics_in_blocks(&all_block_pcs)?; - let (read_only, payable) = self.analyze_function_properties_in_blocks(&all_block_pcs)?; - - Ok(FunctionSemantics { - name: "fallback".to_string(), - selector: None, - preconditions: vec![], - postconditions: vec![], - state_modifications, - gas_characteristics, - read_only, - payable, - block_pcs: all_block_pcs, - }) - } - - fn find_reachable_blocks_in_cfg(&self, start_pc: usize) -> VerificationResult> { - let cfg = &self.cfg_bundle.cfg; - let mut reachable = Vec::new(); - let mut visited = HashSet::new(); - let mut queue = VecDeque::new(); - - if let Some(&start_node) = self.cfg_bundle.pc_to_block.get(&start_pc) { - queue.push_back(start_node); - } else { - return Err(Error::BytecodeAnalysis(format!( - "No block found for start PC: {start_pc}", - ))); - } - - while let Some(node_idx) = queue.pop_front() { - if visited.contains(&node_idx) { - continue; - } - visited.insert(node_idx); - - if let Some(Block::Body(body)) = cfg.node_weight(node_idx) { - reachable.push(body.start_pc); - } - - for edge in cfg.edges_directed(node_idx, petgraph::Direction::Outgoing) { - queue.push_back(edge.target()); - } - } - - Ok(reachable) - } - - fn analyze_storage_patterns(&mut self) -> VerificationResult<()> { - tracing::debug!("Analyzing storage access patterns"); - - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - let mut stack = Vec::new(); - let path_conditions = Vec::new(); - - for instruction in instructions { - self.update_stack(&mut stack, instruction); - - match instruction.op { - Opcode::SLOAD => { - if let Some(slot) = stack.last().cloned() { - self.storage_accesses.push(StorageAccess { - pc: instruction.pc, - slot, - access_type: StorageAccessType::Load, - stored_value: None, - conditions: path_conditions.clone(), - }); - } - } - Opcode::SSTORE => { - if stack.len() >= 2 { - let slot = stack[stack.len() - 1].clone(); - let value = stack[stack.len() - 2].clone(); - self.storage_accesses.push(StorageAccess { - pc: instruction.pc, - slot, - access_type: StorageAccessType::Store, - stored_value: Some(value), - conditions: path_conditions.clone(), - }); - } - } - _ => {} - } - } - } - } - - tracing::debug!("Found {} storage accesses", self.storage_accesses.len()); - Ok(()) - } - - fn analyze_storage_layout(&self) -> VerificationResult> { - let mut layout = HashMap::new(); - - for access in &self.storage_accesses { - if let StackValue::Concrete(slot) = access.slot { - layout.entry(slot).or_insert("uint256".to_string()); - } - } - - if layout.is_empty() { - // Default entries for demonstration - layout.insert(0, "uint256".to_string()); - layout.insert(1, "address".to_string()); - layout.insert(2, "mapping(address=>uint256)".to_string()); - } - - Ok(layout) - } - - fn detect_contract_patterns(&mut self) -> VerificationResult<()> { - tracing::debug!("Detecting contract patterns"); - - if let Some(erc20_pattern) = self.detect_erc20_pattern()? { - self.patterns.push(erc20_pattern); - } - - if let Some(ownable_pattern) = self.detect_ownable_pattern()? { - self.patterns.push(ownable_pattern); - } - - if let Some(guard_pattern) = self.detect_reentrancy_guard_pattern()? { - self.patterns.push(guard_pattern); - } - - tracing::debug!("Detected {} contract patterns", self.patterns.len()); - Ok(()) - } - - fn detect_erc20_pattern(&self) -> VerificationResult> { - let mut evidence = Vec::new(); - let mut score = 0.0; - - if self.has_function_selector(&[0xa9, 0x05, 0x9c, 0xbb]) { - evidence.push(PatternEvidence { - evidence_type: "transfer_function".to_string(), - pc: 0, - details: "Found transfer function selector".to_string(), - }); - score += 0.3; - } - - if self.has_balance_mapping_pattern() { - evidence.push(PatternEvidence { - evidence_type: "balance_mapping".to_string(), - pc: 0, - details: "Found balance mapping access pattern".to_string(), - }); - score += 0.3; - } - - if score >= 0.3 { - Ok(Some(ContractPattern { - pattern_type: PatternType::ERC20Token, - confidence: score, - evidence, - })) - } else { - Ok(None) - } - } - - fn detect_ownable_pattern(&self) -> VerificationResult> { - let mut evidence = Vec::new(); - let mut score = 0.0; - - if self.has_owner_storage_pattern() { - evidence.push(PatternEvidence { - evidence_type: "owner_storage".to_string(), - pc: 0, - details: "Found owner storage access pattern".to_string(), - }); - score += 0.5; - } - - if score >= 0.3 { - Ok(Some(ContractPattern { - pattern_type: PatternType::Ownable, - confidence: score, - evidence, - })) - } else { - Ok(None) - } - } - - fn detect_reentrancy_guard_pattern(&self) -> VerificationResult> { - let mut evidence = Vec::new(); - let mut score = 0.0; - - if self.has_guard_check_pattern() { - evidence.push(PatternEvidence { - evidence_type: "guard_check".to_string(), - pc: 0, - details: "Found reentrancy guard check pattern".to_string(), - }); - score += 0.5; - } - - if score >= 0.3 { - Ok(Some(ContractPattern { - pattern_type: PatternType::ReentrancyGuard, - confidence: score, - evidence, - })) - } else { - Ok(None) - } - } - - fn symbolic_execution_analysis(&mut self) -> VerificationResult<()> { - tracing::debug!("Performing symbolic execution analysis"); - // Placeholder for full symbolic execution - Ok(()) - } - - fn update_stack(&self, stack: &mut Vec, instruction: &Instruction) { - match instruction.op { - Opcode::PUSH(_) | Opcode::PUSH0 => { - if let Some(immediate) = &instruction.imm { - if let Ok(value) = u64::from_str_radix(immediate, 16) { - stack.push(StackValue::Concrete(value)); - } else { - stack.push(StackValue::Unknown); - } - } - } - Opcode::CALLDATALOAD => { - if !stack.is_empty() { - let offset = stack.pop().unwrap(); - stack.push(StackValue::Symbolic(format!( - "CALLDATALOAD({})", - self.stack_value_to_string(&offset) - ))); - } - } - Opcode::ADD => { - if stack.len() >= 2 { - let b = stack.pop().unwrap(); - let a = stack.pop().unwrap(); - stack.push(StackValue::Operation { - op: "ADD".to_string(), - operands: vec![Box::new(a), Box::new(b)], - }); - } - } - Opcode::POP => { - stack.pop(); - } - _ => {} - } - } - - #[allow(clippy::only_used_in_recursion)] - fn stack_value_to_string(&self, value: &StackValue) -> String { - match value { - StackValue::Concrete(v) => format!("0x{v:x}"), - StackValue::Symbolic(s) => s.clone(), - StackValue::Operation { op, operands } => { - let op_strs: Vec = operands - .iter() - .map(|op| self.stack_value_to_string(op)) - .collect(); - format!("{}({})", op, op_strs.join(", ")) - } - StackValue::StorageLoad(slot) => { - format!("SLOAD({})", self.stack_value_to_string(slot)) - } - StackValue::Unknown => "UNKNOWN".to_string(), - } - } - - fn analyze_contract_properties(&self) -> VerificationResult { - let mut is_proxy = false; - let mut is_upgradeable = false; - let mut has_reentrancy_guards = false; - let mut access_control = AccessControlType::None; - - // Use CFG structure instead of raw instructions - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - for instruction in instructions { - match instruction.op { - Opcode::DELEGATECALL => { - is_proxy = true; - is_upgradeable = true; - } - Opcode::CALLER => { - access_control = AccessControlType::Owner; - } - _ => {} - } - } - } - } - - if self.has_guard_check_pattern() { - has_reentrancy_guards = true; - } - - Ok(ContractProperties { - is_proxy, - is_upgradeable, - has_reentrancy_guards, - access_control, - }) - } - - fn analyze_state_modifications_in_blocks( - &self, - _block_pcs: &[usize], - ) -> VerificationResult> { - let mut modifications = Vec::new(); - - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - for instruction in instructions { - if instruction.op == Opcode::SSTORE { - modifications.push(StateModification { - storage_slot: 0, // TODO: Requires proper stack analysis - modification_type: ModificationType::Assignment, - conditions: vec![], - }); - } - } - } - } - - Ok(modifications) - } - - fn analyze_gas_characteristics_in_blocks( - &self, - _block_pcs: &[usize], - ) -> VerificationResult { - let mut base_cost = 21000u64; - let mut variable_costs = Vec::new(); - - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - for instruction in instructions { - // Calculate gas cost for each opcode - let opcode = instruction.op; - base_cost += self.get_instruction_gas_cost(&opcode); - - match opcode { - Opcode::SSTORE => { - variable_costs.push(VariableGasCost { - factor: GasCostFactor::StorageOperations, - cost_per_unit: 20000, - }); - } - Opcode::CALL - | Opcode::CALLCODE - | Opcode::DELEGATECALL - | Opcode::STATICCALL => { - variable_costs.push(VariableGasCost { - factor: GasCostFactor::ExternalCalls, - cost_per_unit: 2300, - }); - } - _ => {} - } - } - } - } - - Ok(GasCharacteristics { - base_cost, - variable_costs, - max_gas: None, - }) - } - - fn analyze_function_properties_in_blocks( - &self, - block_pcs: &[usize], - ) -> VerificationResult<(bool, bool)> { - let mut has_state_change = false; - let mut is_payable = false; - - for &block_pc in block_pcs { - if let Some(&node_idx) = self.cfg_bundle.pc_to_block.get(&block_pc) { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - for instruction in instructions { - match instruction.op { - Opcode::SSTORE => has_state_change = true, - Opcode::CALLVALUE => is_payable = true, - _ => {} - } - } - } - } - } - - Ok((!has_state_change, is_payable)) - } - - fn extract_state_invariants( - &self, - functions: &[FunctionSemantics], - storage_layout: &HashMap, - ) -> VerificationResult> { - let mut invariants = Vec::new(); - - for pattern in &self.patterns { - match pattern.pattern_type { - PatternType::ERC20Token => { - invariants - .push("(= (sum-all-balances state) (total-supply state))".to_string()); - invariants.push( - "(forall ((address Address)) (>= (balance address state) 0))".to_string(), - ); - } - PatternType::Ownable => { - invariants.push( - "(not (= (owner state) #x0000000000000000000000000000000000000000))" - .to_string(), - ); - } - PatternType::ReentrancyGuard => { - invariants.push( - "(=> (guard-locked state) (not (can-call-external state)))".to_string(), - ); - } - _ => {} - } - } - - for (slot, slot_type) in storage_layout { - match slot_type.as_str() { - "uint256" => { - invariants.push(format!( - "(and (>= (storage-slot-{slot} (storage s)) 0) (< (storage-slot-{slot} (storage s)) (^ 2 256)))", - )); - } - "address" => { - invariants.push(format!( - "(and (>= (storage-slot-{slot} (storage s)) 0) (< (storage-slot-{slot} (storage s)) (^ 2 160)))", - )); - } - _ => {} - } - } - - for function in functions { - if function.read_only { - invariants.push(format!( - "(forall ((s State) (tx Transaction)) (= (storage (final-state ({} s tx))) (storage s)))", - function.name - )); - } - } - - Ok(invariants) - } - - fn generate_preconditions( - &self, - selector: &[u8; 4], - state_modifications: &[StateModification], - ) -> VerificationResult> { - let mut preconditions = Vec::new(); - - preconditions.push(format!( - "(= (function-selector (data tx)) #x{})", - hex::encode(selector) - )); - - for pattern in &self.patterns { - match pattern.pattern_type { - PatternType::ERC20Token => { - if self.is_transfer_function(selector) { - preconditions.push( - "(>= (balance (sender tx) (storage state)) (transfer-amount tx))" - .to_string(), - ); - preconditions.push( - "(not (= (recipient tx) #x0000000000000000000000000000000000000000))" - .to_string(), - ); - preconditions.push("(> (transfer-amount tx) 0)".to_string()); - } - } - PatternType::Ownable => { - if self.is_admin_function(selector) { - preconditions.push("(= (sender tx) (owner (storage state)))".to_string()); - } - } - PatternType::ReentrancyGuard => { - preconditions.push("(not (guard-locked (storage state)))".to_string()); - } - _ => {} - } - } - - for modification in state_modifications { - if let ModificationType::Arithmetic = modification.modification_type { - preconditions.push(format!( - "(>= (storage-slot-{} (storage state)) 0)", - modification.storage_slot - )); - } - } - - Ok(preconditions) - } - - fn generate_postconditions( - &self, - _selector: &[u8; 4], - state_modifications: &[StateModification], - ) -> VerificationResult> { - let mut postconditions = Vec::new(); - - postconditions.push("(=> (success result) (> (gas-used result) 0))".to_string()); - - for modification in state_modifications { - postconditions.push(format!( - "(=> (success result) - (= (storage-slot-{} (storage (final-state result))) - (updated-value (storage-slot-{} (storage state)))))", - modification.storage_slot, modification.storage_slot - )); - } - - Ok(postconditions) - } - - fn extract_function_selector_from_instructions( - &self, - instructions: &[Instruction], - ) -> Option<[u8; 4]> { - for instruction in instructions { - if instruction.op == Opcode::PUSH(4) { - if let Some(imm) = &instruction.imm { - if let Ok(bytes) = hex::decode(imm) { - if bytes.len() == 4 { - let mut selector = [0u8; 4]; - selector.copy_from_slice(&bytes); - return Some(selector); - } - } - } - } - } - None - } - - fn is_transfer_function(&self, selector: &[u8; 4]) -> bool { - *selector == [0xa9, 0x05, 0x9c, 0xbb] // transfer(address,uint256) - } - - fn is_admin_function(&self, selector: &[u8; 4]) -> bool { - // Example admin function selectors - const ADMIN_SELECTORS: &[[u8; 4]] = &[ - [0xf2, 0xfd, 0xe3, 0x8b], // transferOwnership(address) - [0x7a, 0xd6, 0x92, 0x6b], // renounceOwnership() - ]; - ADMIN_SELECTORS.contains(selector) - } - - fn get_instruction_gas_cost(&self, opcode: &Opcode) -> u64 { - match opcode { - Opcode::ADD | Opcode::MUL | Opcode::SUB | Opcode::DIV | Opcode::SDIV => 3, - - Opcode::MOD - | Opcode::SMOD - | Opcode::ADDMOD - | Opcode::MULMOD - | Opcode::EXP - | Opcode::SIGNEXTEND => 5, - - Opcode::LT - | Opcode::GT - | Opcode::SLT - | Opcode::SGT - | Opcode::EQ - | Opcode::ISZERO - | Opcode::AND - | Opcode::OR - | Opcode::XOR - | Opcode::NOT - | Opcode::BYTE - | Opcode::SHL - | Opcode::SHR - | Opcode::SAR => 3, - - Opcode::MLOAD | Opcode::MSTORE | Opcode::MSTORE8 => 3, - Opcode::SLOAD => 800, - Opcode::SSTORE => 20000, - Opcode::POP => 2, - - Opcode::DUP(_) | Opcode::SWAP(_) => 3, - Opcode::PUSH(_) => 3, - - Opcode::JUMP => 8, - Opcode::JUMPI => 10, - Opcode::JUMPDEST => 1, - - Opcode::CALL | Opcode::CALLCODE | Opcode::DELEGATECALL | Opcode::STATICCALL => 700, - - Opcode::RETURN | Opcode::REVERT => 0, - _ => 1, - } - } - - fn has_function_selector(&self, selector: &[u8; 4]) -> bool { - let selector_hex = hex::encode(selector); - - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - for inst in instructions { - if inst.op == Opcode::PUSH(4) && inst.imm.as_ref() == Some(&selector_hex) { - return true; - } - } - } - } - false - } - - fn has_balance_mapping_pattern(&self) -> bool { - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - if instructions.windows(10).any(|window| { - window.iter().any(|inst| inst.op == Opcode::CALLDATALOAD) - && window.iter().any(|inst| inst.op == Opcode::KECCAK256) - && window.iter().any(|inst| inst.op == Opcode::SLOAD) - }) { - return true; - } - } - } - false - } - - fn has_owner_storage_pattern(&self) -> bool { - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - if instructions.windows(5).any(|window| { - window.iter().any(|inst| inst.op == Opcode::CALLER) - && window - .iter() - .any(|inst| matches!(inst.op, Opcode::SLOAD | Opcode::SSTORE)) - }) { - return true; - } - } - } - false - } - - fn has_guard_check_pattern(&self) -> bool { - for node_idx in self.cfg_bundle.cfg.node_indices() { - if let Some(Block::Body(body)) = self.cfg_bundle.cfg.node_weight(node_idx) { - let instructions = &body.instructions; - if instructions.windows(3).any(|window| { - window.len() == 3 - && window[0].op == Opcode::SLOAD - && window[1].op == Opcode::ISZERO - && window[2].op == Opcode::JUMPI - }) { - return true; - } - } - } - false - } -} - -#[cfg(test)] -pub mod tests { - use super::*; - use azoth_core::{cfg_ir::CfgIrBundle, strip::CleanReport}; - use revm::primitives::B256; - - // todo(g4titanx): impl. default for cleanreport - pub fn create_empty_clean_report() -> CleanReport { - CleanReport { - runtime_layout: vec![], - removed: vec![], - swarm_hash: None, - bytes_saved: 0, - clean_len: 0, - clean_keccak: B256::ZERO, - program_counter_mapping: vec![], - } - } - - #[test] - fn test_function_selector_extraction() { - let cfg_bundle = CfgIrBundle { - cfg: petgraph::stable_graph::StableGraph::new(), - pc_to_block: HashMap::new(), - clean_report: create_empty_clean_report(), - sections: vec![], - selector_mapping: None, - original_bytecode: vec![], - runtime_bounds: None, - trace: Vec::new(), - dispatcher_controller_pcs: None, - dispatcher_patches: None, - stub_patches: None, - decoy_patches: None, - controller_patches: None, - dispatcher_info: None, - dispatcher_blocks: std::collections::HashSet::new(), - arithmetic_chain_data: None, - }; - let analyzer = SemanticAnalyzer::new(cfg_bundle); - - let instructions = vec![Instruction { - pc: 0, - op: Opcode::PUSH(4), - imm: Some("12345678".to_string()), - }]; - - let selector = analyzer.extract_function_selector_from_instructions(&instructions); - assert!(selector.is_some()); - assert_eq!(selector.unwrap(), [0x12, 0x34, 0x56, 0x78]); - } - - #[test] - fn test_erc20_pattern_detection() { - // Create a CFG with actual blocks containing the instruction - let mut cfg = petgraph::stable_graph::StableGraph::new(); - let mut pc_to_block = HashMap::new(); - - // Create a block with the transfer function selector - let instructions = vec![Instruction { - pc: 0, - op: Opcode::PUSH(4), - imm: Some("a9059cbb".to_string()), // transfer selector - }]; - - let block = Block::Body(cfg_ir::BlockBody { - start_pc: 0, - instructions, - max_stack: 1, - control: cfg_ir::BlockControl::Unknown, - }); - - let node_idx = cfg.add_node(block); - pc_to_block.insert(0, node_idx); - - let cfg_bundle = CfgIrBundle { - cfg, - pc_to_block, - clean_report: create_empty_clean_report(), - sections: vec![], - selector_mapping: None, - original_bytecode: vec![], - runtime_bounds: None, - trace: Vec::new(), - dispatcher_controller_pcs: None, - dispatcher_patches: None, - stub_patches: None, - decoy_patches: None, - controller_patches: None, - dispatcher_info: None, - dispatcher_blocks: std::collections::HashSet::new(), - arithmetic_chain_data: None, - }; - - let analyzer = SemanticAnalyzer::new(cfg_bundle); - - // Now this should pass - assert!(analyzer.has_function_selector(&[0xa9, 0x05, 0x9c, 0xbb])); - assert!(analyzer.is_transfer_function(&[0xa9, 0x05, 0x9c, 0xbb])); - } - - #[test] - fn test_transfer_function_detection() { - let cfg_bundle = CfgIrBundle { - cfg: petgraph::stable_graph::StableGraph::new(), - pc_to_block: HashMap::new(), - clean_report: create_empty_clean_report(), - sections: vec![], - selector_mapping: None, - original_bytecode: vec![], - runtime_bounds: None, - trace: Vec::new(), - dispatcher_controller_pcs: None, - dispatcher_patches: None, - stub_patches: None, - decoy_patches: None, - controller_patches: None, - dispatcher_info: None, - dispatcher_blocks: std::collections::HashSet::new(), - arithmetic_chain_data: None, - }; - - let analyzer = SemanticAnalyzer::new(cfg_bundle); - - // Test the pure function logic (doesn't depend on CFG) - assert!(analyzer.is_transfer_function(&[0xa9, 0x05, 0x9c, 0xbb])); - - // Test function selector extraction from instructions directly - let instructions = vec![Instruction { - pc: 0, - op: Opcode::PUSH(4), - imm: Some("a9059cbb".to_string()), - }]; - - let selector = analyzer.extract_function_selector_from_instructions(&instructions); - assert!(selector.is_some()); - assert_eq!(selector.unwrap(), [0xa9, 0x05, 0x9c, 0xbb]); - } -} diff --git a/crates/verification/src/smt.rs b/crates/verification/src/smt.rs deleted file mode 100644 index 85da2cd4..00000000 --- a/crates/verification/src/smt.rs +++ /dev/null @@ -1,901 +0,0 @@ -//! SMT solver integration for formal verification -//! -//! This module provides SMT-LIB formula generation and Z3 solver integration -//! for proving contract equivalence and property preservation. - -use crate::semantics::{ContractSemantics, FunctionSemantics, ModificationType, StateModification}; -use crate::{Error, VerificationResult}; -use serde::{Deserialize, Serialize}; -use std::time::Duration; -use z3::{ - ast::{self, Ast}, - Config, Context, Solver, -}; - -/// SMT solver for formal verification -#[derive(Debug)] -pub struct SmtSolver { - z3_context: Context, -} - -/// SMT formula with declarations and assertions -#[derive(Debug, Clone)] -struct SmtFormula { - declarations: Vec, - assertions: Vec, -} - -/// Result from SMT solver -#[derive(Debug, Clone, Serialize, Deserialize)] -pub struct SmtResult { - /// Whether the formula is satisfiable - pub satisfiable: bool, - /// Model (if satisfiable) - pub model: Option, - /// Time taken to solve - pub solve_time: Duration, -} - -/// Function parameter information extracted from semantic analysis -#[derive(Debug, Clone)] -struct FunctionParameter { - name: String, - type_name: String, - offset: usize, -} - -impl SmtFormula { - fn new() -> Self { - Self { - declarations: Vec::new(), - assertions: Vec::new(), - } - } - - fn build_formula_string(&self) -> String { - let mut parts = Vec::new(); - - // Add all declarations - for decl in &self.declarations { - parts.push(decl.clone()); - } - - // Add all assertions - for assertion in &self.assertions { - parts.push(assertion.clone()); - } - - // Add check-sat - parts.push("(check-sat)".to_string()); - - parts.join("\n") - } -} - -impl SmtSolver { - /// Create new SMT solver instance - pub fn new() -> VerificationResult { - let z3_config = Config::new(); - let z3_context = Context::new(&z3_config); - - Ok(Self { z3_context }) - } - - /// Check satisfiability of SMT formulas - pub async fn check_satisfiability(&self, formulas: &[String]) -> VerificationResult { - let start_time = std::time::Instant::now(); - let solver = Solver::new(&self.z3_context); - - // Parse and add each formula - for formula in formulas { - self.parse_and_add_formula(&solver, formula)?; - } - - // Check satisfiability - let result = solver.check(); - let satisfiable = matches!(result, z3::SatResult::Sat); - - // Get model if satisfiable - let model = if satisfiable { - solver.get_model().map(|m| m.to_string()) - } else { - None - }; - - let solve_time = start_time.elapsed(); - - Ok(SmtResult { - satisfiable, - model, - solve_time, - }) - } - - /// Parse and add SMT formula to solver - fn parse_and_add_formula(&self, solver: &z3::Solver, formula: &str) -> VerificationResult<()> { - if formula.trim().starts_with("(assert") { - let content = self.extract_assertion_content(formula)?; - let ast = self.parse_assertion_content(&content)?; - solver.assert(&ast); - Ok(()) - } else { - // Handle declarations - if formula.trim().starts_with("(declare-") { - // For now, skip declarations as they're handled by our type system - Ok(()) - } else { - Err(Error::SmtSolver(format!( - "Unsupported formula format: {formula}", - ))) - } - } - } - - fn extract_assertion_content(&self, formula: &str) -> VerificationResult { - let trimmed = formula.trim(); - if trimmed.starts_with("(assert") && trimmed.ends_with(')') { - let content = &trimmed[8..trimmed.len() - 1].trim(); - Ok(content.to_string()) - } else { - Err(Error::SmtSolver("Invalid assertion format".to_string())) - } - } - - fn parse_assertion_content(&self, content: &str) -> VerificationResult> { - let content = content.trim(); - - // Handle basic patterns - if content == "true" { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } else if content == "false" { - Ok(ast::Bool::from_bool(&self.z3_context, false)) - } else if content.starts_with("(=") { - self.parse_equality(content) - } else if content.starts_with("(>") { - self.parse_comparison(content, ">") - } else if content.starts_with("(>=") { - self.parse_comparison(content, ">=") - } else if content.starts_with("(<") { - self.parse_comparison(content, "<") - } else if content.starts_with("(<=") { - self.parse_comparison(content, "<=") - } else if content.starts_with("(and") { - self.parse_and(content) - } else if content.starts_with("(or") { - self.parse_or(content) - } else if content.starts_with("(not") { - self.parse_not(content) - } else if content.starts_with("(forall") { - self.parse_forall(content) - } else if content.starts_with("(=>") { - self.parse_implies(content) - } else { - // For now, treat unknown formulas as true to avoid failures - tracing::warn!("Unknown SMT formula pattern: {content}, treating as true"); - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } - - fn parse_equality(&self, content: &str) -> VerificationResult> { - // Simple equality parsing: (= a b) - if content.len() > 4 { - let inner = &content[2..content.len() - 1].trim(); - let parts: Vec<&str> = inner.split_whitespace().collect(); - if parts.len() == 2 { - let left = self.parse_term(parts[0])?; - let right = self.parse_term(parts[1])?; - Ok(left._eq(&right)) - } else { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } else { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } - - fn parse_comparison(&self, content: &str, op: &str) -> VerificationResult> { - let op_len = op.len() + 1; // +1 for opening paren - if content.len() > op_len + 1 { - let inner = &content[op_len..content.len() - 1].trim(); - let parts: Vec<&str> = inner.split_whitespace().collect(); - if parts.len() == 2 { - let left = self.parse_int_term(parts[0])?; - let right = self.parse_int_term(parts[1])?; - match op { - ">" => Ok(left.gt(&right)), - ">=" => Ok(left.ge(&right)), - "<" => Ok(left.lt(&right)), - "<=" => Ok(left.le(&right)), - _ => Ok(ast::Bool::from_bool(&self.z3_context, true)), - } - } else { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } else { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } - - fn parse_and(&self, _content: &str) -> VerificationResult> { - // For now, simplified and parsing - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - - fn parse_or(&self, _content: &str) -> VerificationResult> { - // For now, simplified or parsing - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - - fn parse_not(&self, content: &str) -> VerificationResult> { - if content.len() > 5 { - let inner = &content[4..content.len() - 1].trim(); - let inner_ast = self.parse_assertion_content(inner)?; - Ok(inner_ast.not()) - } else { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } - - fn parse_forall(&self, content: &str) -> VerificationResult> { - let content = content.trim(); - if !content.starts_with("(forall") { - return Ok(ast::Bool::from_bool(&self.z3_context, true)); - } - - // Extract the body part after variable declarations - // For now, we'll parse basic forall patterns - if let Some(body_start) = content.find(")) ") { - let body = &content[body_start + 3..]; - let body = if let Some(stripped) = body.strip_suffix(')') { - stripped - } else { - body - }; - - // Parse the body formula - self.parse_assertion_content(body) - } else { - // Fallback for complex quantifiers - tracing::warn!("Complex quantifier pattern, approximating as true"); - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } - - fn parse_implies(&self, content: &str) -> VerificationResult> { - // Implication parsing: (=> a b) - if content.len() > 4 { - let _inner = &content[3..content.len() - 1].trim(); - // For now, simplified parsing - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } else { - Ok(ast::Bool::from_bool(&self.z3_context, true)) - } - } - - fn parse_term(&self, term: &str) -> VerificationResult> { - // Try to parse as integer first - if let Ok(value) = term.parse::() { - Ok(ast::Int::from_i64(&self.z3_context, value).into()) - } else if let Some(stripped) = term.strip_prefix("#x") { - if let Ok(value) = i64::from_str_radix(stripped, 16) { - Ok(ast::Int::from_i64(&self.z3_context, value).into()) - } else { - // Create integer variable (Z3 automatically infers sort) - Ok(ast::Int::new_const(&self.z3_context, term).into()) - } - } else { - // Variable name - create integer constant - Ok(ast::Int::new_const(&self.z3_context, term).into()) - } - } - - fn parse_int_term(&self, term: &str) -> VerificationResult> { - if let Ok(value) = term.parse::() { - Ok(ast::Int::from_i64(&self.z3_context, value)) - } else if let Some(stripped) = term.strip_prefix("#x") { - if let Ok(value) = i64::from_str_radix(stripped, 16) { - Ok(ast::Int::from_i64(&self.z3_context, value)) - } else { - Ok(ast::Int::new_const(&self.z3_context, term)) - } - } else { - Ok(ast::Int::new_const(&self.z3_context, term)) - } - } - - /// Generate SMT formulas from contract semantics - pub fn encode_contract_semantics( - &self, - semantics: &ContractSemantics, - ) -> VerificationResult { - let mut formula = SmtFormula::new(); - - // Declare basic types - self.declare_basic_types(&mut formula); - - // Encode storage layout - self.encode_contract_state(&mut formula, semantics)?; - - // Encode function implementations - self.encode_execution_semantics(&mut formula, semantics)?; - - // Encode state invariants - self.encode_state_invariants(&mut formula, semantics)?; - - Ok(formula.build_formula_string()) - } - - fn declare_basic_types(&self, formula: &mut SmtFormula) { - formula.declarations.extend([ - "; Basic EVM types".to_string(), - "(declare-sort Address 0)".to_string(), - "(declare-sort Storage 0)".to_string(), - "(declare-sort State 0)".to_string(), - "(declare-sort Transaction 0)".to_string(), - "(declare-sort ExecResult 0)".to_string(), - "".to_string(), - "; Transaction structure with proper calldata model".to_string(), - "(declare-fun function-selector (Transaction) Int)".to_string(), - "(declare-fun calldata-word (Transaction Int) Int)".to_string(), - "(declare-fun calldata-length (Transaction) Int)".to_string(), - "(declare-fun sender (Transaction) Address)".to_string(), - "(declare-fun value (Transaction) Int)".to_string(), - "(declare-fun gas-limit (Transaction) Int)".to_string(), - "".to_string(), - "; State access functions".to_string(), - "(declare-fun storage (State) Storage)".to_string(), - "(declare-fun block-number (State) Int)".to_string(), - "(declare-fun block-timestamp (State) Int)".to_string(), - "".to_string(), - "; Execution result functions".to_string(), - "(declare-fun success (ExecResult) Bool)".to_string(), - "(declare-fun final-state (ExecResult) State)".to_string(), - "(declare-fun gas-used (ExecResult) Int)".to_string(), - "(declare-fun revert-reason (ExecResult) Int)".to_string(), - "".to_string(), - "; Transaction constraints".to_string(), - "(assert (forall ((tx Transaction)) (and (>= (function-selector tx) 0) (< (function-selector tx) 4294967296))))".to_string(), - "(assert (forall ((tx Transaction)) (>= (calldata-length tx) 4)))".to_string(), - "(assert (forall ((tx Transaction)) (>= (value tx) 0)))".to_string(), - "(assert (forall ((tx Transaction)) (>= (gas-limit tx) 21000)))".to_string(), - "".to_string(), - ]); - } - - fn encode_contract_state( - &self, - formula: &mut SmtFormula, - semantics: &ContractSemantics, - ) -> VerificationResult<()> { - formula - .declarations - .push("; Contract storage layout".to_string()); - - for (slot, value_type) in &semantics.storage_layout { - match value_type.as_str() { - "uint256" => { - formula - .declarations - .push(format!("(declare-fun storage-slot-{slot} (Storage) Int)")); - // Add bounds for uint256 - formula.assertions.push(format!( - "(assert (forall ((s Storage)) (and (>= (storage-slot-{slot} s) 0) (< (storage-slot-{slot} s) (^ 2 256)))))", - )); - } - "address" => { - formula.declarations.push(format!( - "(declare-fun storage-slot-{slot} (Storage) Address)", - )); - } - "mapping(address=>uint256)" => { - formula.declarations.push(format!( - "(declare-fun mapping-{slot} (Storage Address) Int)", - )); - // Add bounds for balance values - formula.assertions.push(format!( - "(assert (forall ((s Storage) (address Address)) (>= (mapping-{slot} s address) 0)))", - )); - } - _ => { - // Generic storage slot - formula - .declarations - .push(format!("(declare-fun storage-slot-{slot} (Storage) Int)")); - } - } - } - - formula.declarations.push("".to_string()); - Ok(()) - } - - fn encode_execution_semantics( - &self, - formula: &mut SmtFormula, - semantics: &ContractSemantics, - ) -> VerificationResult<()> { - formula - .declarations - .push("; Function declarations".to_string()); - - for function in &semantics.functions { - // Declare function - formula.declarations.push(format!( - "(declare-fun {} (State Transaction) ExecResult)", - function.name - )); - - // Encode function logic - if let Some(selector) = function.selector { - self.encode_function_logic(formula, function, selector)?; - } - } - - formula.declarations.push("".to_string()); - Ok(()) - } - - fn encode_function_logic( - &self, - formula: &mut SmtFormula, - function: &FunctionSemantics, - selector: [u8; 4], - ) -> VerificationResult<()> { - // Function selector check using proper transaction model - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction)) - (=> (not (= (function-selector tx) #x{})) - (= (success ({} s tx)) false))))", - hex::encode(selector), - function.name - )); - - // Extract function parameters based on selector - let parameters = self.extract_function_parameters(function, selector)?; - - // Declare parameter extraction functions - for param in parameters.iter() { - formula.declarations.push(format!( - "(declare-fun {}-{} (Transaction) {})", - function.name, - param.name, - self.solidity_type_to_smt(¶m.type_name) - )); - - // Link to calldata - formula.assertions.push(format!( - "(assert (forall ((tx Transaction)) - (= ({}-{} tx) (calldata-word tx {}))))", - function.name, param.name, param.offset - )); - } - - // Encode preconditions with real parameter references - for precondition in &function.preconditions { - let processed_precondition = - self.process_precondition(precondition, function, ¶meters)?; - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction)) - (=> (and (= (function-selector tx) #x{}) (not {})) - (= (success ({} s tx)) false))))", - hex::encode(selector), - processed_precondition, - function.name - )); - } - - // Encode state modifications with proper parameter references - for modification in &function.state_modifications { - self.encode_state_modification_with_params( - formula, - function, - modification, - ¶meters, - )?; - } - - // Encode postconditions - for postcondition in &function.postconditions { - let processed_postcondition = - self.process_postcondition(postcondition, function, ¶meters)?; - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result)) - {})))", - function.name, processed_postcondition - )); - } - - // Add revert conditions for common failure cases - self.encode_revert_conditions(formula, function, selector, ¶meters)?; - - Ok(()) - } - - /// Extract function parameters from semantic analysis - fn extract_function_parameters( - &self, - _function: &FunctionSemantics, - selector: [u8; 4], - ) -> VerificationResult> { - let mut parameters = Vec::new(); - - // Common ERC20 function parameters - match selector { - [0xa9, 0x05, 0x9c, 0xbb] => { - // transfer(address,uint256) - parameters.push(FunctionParameter { - name: "recipient".to_string(), - type_name: "address".to_string(), - offset: 4, - }); - parameters.push(FunctionParameter { - name: "amount".to_string(), - type_name: "uint256".to_string(), - offset: 36, - }); - } - [0x70, 0xa0, 0x82, 0x31] => { - // balanceOf(address) - parameters.push(FunctionParameter { - name: "account".to_string(), - type_name: "address".to_string(), - offset: 4, - }); - } - [0xa0, 0x71, 0x2d, 0x68] => { - // mint(uint256) - parameters.push(FunctionParameter { - name: "amount".to_string(), - type_name: "uint256".to_string(), - offset: 4, - }); - } - _ => { - // Generic parameter extraction based on function name - tracing::debug!( - "Unknown function selector {:?}, using generic parameters", - selector - ); - } - } - - Ok(parameters) - } - - fn solidity_type_to_smt(&self, solidity_type: &str) -> &str { - match solidity_type { - "address" => "Int", // Simplified as 160-bit integer - "uint256" | "uint" => "Int", - "int256" | "int" => "Int", - "bool" => "Bool", - "bytes32" => "Int", - _ => "Int", // Default fallback - } - } - - fn process_precondition( - &self, - condition: &str, - function: &FunctionSemantics, - parameters: &[FunctionParameter], - ) -> VerificationResult { - let mut processed = condition.to_string(); - - // Replace parameter references - for param in parameters { - let param_ref = format!("{}-{}", function.name, param.name); - processed = processed.replace("(transfer-amount tx)", &format!("({param_ref} tx)")); - processed = processed.replace("(recipient tx)", &format!("({param_ref} tx)")); - } - - // Replace common patterns - processed = processed.replace( - "(balance sender state)", - "(mapping-0 (storage state) (sender tx))", - ); - - Ok(processed) - } - - fn process_postcondition( - &self, - condition: &str, - function: &FunctionSemantics, - parameters: &[FunctionParameter], - ) -> VerificationResult { - // Similar processing to preconditions - self.process_precondition(condition, function, parameters) - } - - fn encode_state_modification_with_params( - &self, - formula: &mut SmtFormula, - function: &FunctionSemantics, - modification: &StateModification, - parameters: &[FunctionParameter], - ) -> VerificationResult<()> { - match modification.modification_type { - ModificationType::Assignment => { - // Find the appropriate parameter value - let value_expr = if parameters.iter().any(|p| p.name == "amount") { - format!("{}-amount tx", function.name) - } else { - "0".to_string() // Fallback - }; - - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result)) - (= (storage-slot-{} (storage (final-state result))) - {}))))", - function.name, modification.storage_slot, value_expr - )); - } - ModificationType::Collection => { - // Handle mapping updates (e.g., ERC20 balances) - if let Some(amount_param) = parameters.iter().find(|p| p.name == "amount") { - if let Some(recipient_param) = parameters.iter().find(|p| p.name == "recipient") - { - // Transfer logic: sender balance decreases, recipient balance increases - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result)) - (and - ; Sender balance decreases - (= (mapping-{} (storage (final-state result)) (sender tx)) - (- (mapping-{} (storage s) (sender tx)) ({}-{} tx))) - ; Recipient balance increases - (= (mapping-{} (storage (final-state result)) ({}-{} tx)) - (+ (mapping-{} (storage s) ({}-{} tx)) ({}-{} tx)))))))", - function.name, - modification.storage_slot, - modification.storage_slot, - function.name, - amount_param.name, - modification.storage_slot, - function.name, - recipient_param.name, - modification.storage_slot, - function.name, - recipient_param.name, - function.name, - amount_param.name - )); - } - } - } - _ => { - // Fallback to original implementation - self.encode_state_modification(formula, function, modification)?; - } - } - Ok(()) - } - - fn encode_revert_conditions( - &self, - formula: &mut SmtFormula, - function: &FunctionSemantics, - selector: [u8; 4], - _parameters: &[FunctionParameter], - ) -> VerificationResult<()> { - match selector { - [0xa9, 0x05, 0x9c, 0xbb] => { - // transfer(address,uint256) - // Insufficient balance check - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction)) - (=> (< (mapping-0 (storage s) (sender tx)) ({}-amount tx)) - (= (success ({} s tx)) false))))", - function.name, function.name - )); - - // Transfer to zero address check - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction)) - (=> (= ({}-recipient tx) 0) - (= (success ({} s tx)) false))))", - function.name, function.name - )); - - // Amount must be positive - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction)) - (=> (<= ({}-amount tx) 0) - (= (success ({} s tx)) false))))", - function.name, function.name - )); - } - _ => { - // Generic revert conditions - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction)) - (=> (< (gas-limit tx) {}) - (= (success ({} s tx)) false))))", - function.gas_characteristics.base_cost, function.name - )); - } - } - Ok(()) - } - - fn encode_state_modification( - &self, - formula: &mut SmtFormula, - function: &FunctionSemantics, - modification: &StateModification, - ) -> VerificationResult<()> { - match modification.modification_type { - ModificationType::Assignment => { - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result)) - (= (storage-slot-{} (storage (final-state result))) - (value tx)))))", - function.name, modification.storage_slot - )); - } - ModificationType::Arithmetic => { - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result)) - (= (storage-slot-{} (storage (final-state result))) - (+ (storage-slot-{} (storage s)) (value tx))))))", - function.name, modification.storage_slot, modification.storage_slot - )); - } - ModificationType::Conditional => { - // Add conditional logic based on modification conditions - for condition in &modification.conditions { - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result) {}) - (= (storage-slot-{} (storage (final-state result))) - (value tx)))))", - function.name, condition, modification.storage_slot - )); - } - } - ModificationType::Collection => { - // Handle mapping/array updates - formula.assertions.push(format!( - "(assert (forall ((s State) (tx Transaction) (result ExecResult)) - (=> (and (= result ({} s tx)) (success result)) - (= (mapping-{} (storage (final-state result)) (sender tx)) - (value tx)))))", - function.name, modification.storage_slot - )); - } - } - Ok(()) - } - - fn encode_state_invariants( - &self, - formula: &mut SmtFormula, - semantics: &ContractSemantics, - ) -> VerificationResult<()> { - formula.assertions.push("; State invariants".to_string()); - - for invariant in &semantics.state_invariants { - formula.assertions.push(format!("(assert {invariant})")); - } - - Ok(()) - } - - /// Generate equivalence formula for two contracts - pub fn generate_equivalence_formula( - &self, - original: &ContractSemantics, - obfuscated: &ContractSemantics, - ) -> VerificationResult { - let mut formula = SmtFormula::new(); - - // Declare types - self.declare_basic_types(&mut formula); - - // Declare both contract functions - formula - .declarations - .push("; Original contract functions".to_string()); - for function in &original.functions { - formula.declarations.push(format!( - "(declare-fun {}-original (State Transaction) ExecResult)", - function.name - )); - } - - formula - .declarations - .push("; Obfuscated contract functions".to_string()); - for function in &obfuscated.functions { - formula.declarations.push(format!( - "(declare-fun {}-obfuscated (State Transaction) ExecResult)", - function.name - )); - } - - // State equivalence assertion - formula.assertions.push( - "(assert (forall ((s State) (tx Transaction)) - (= (final-state (execute-original s tx)) - (final-state (execute-obfuscated s tx)))))" - .to_string(), - ); - - // Success equivalence - formula.assertions.push( - "(assert (forall ((s State) (tx Transaction)) - (= (success (execute-original s tx)) - (success (execute-obfuscated s tx)))))" - .to_string(), - ); - - // Gas bounds (obfuscated should use at most 15% more gas) - formula.assertions.push( - "(assert (forall ((s State) (tx Transaction)) - (=> (success (execute-original s tx)) - (<= (gas-used (execute-obfuscated s tx)) - (* 115 (div (gas-used (execute-original s tx)) 100))))))" - .to_string(), - ); - - Ok(formula.build_formula_string()) - } - - /// Prove that two contracts are equivalent - pub async fn prove_equivalence( - &self, - original: &ContractSemantics, - obfuscated: &ContractSemantics, - ) -> VerificationResult { - let equivalence_formula = self.generate_equivalence_formula(original, obfuscated)?; - - // Check satisfiability (if unsatisfiable, then equivalence holds) - let result = self.check_satisfiability(&[equivalence_formula]).await?; - - // For equivalence proofs, we want UNSAT (meaning the negation is unsatisfiable) - Ok(!result.satisfiable) - } -} - -#[cfg(test)] -mod tests { - use super::*; - - #[tokio::test] - async fn test_smt_solver_creation() { - let solver = SmtSolver::new(); - assert!(solver.is_ok()); - } - - #[tokio::test] - async fn test_basic_formula_parsing() { - let solver = SmtSolver::new().unwrap(); - - let formulas = vec![ - "(assert true)".to_string(), - "(assert false)".to_string(), - "(assert (= x 42))".to_string(), - ]; - - let result = solver.check_satisfiability(&formulas).await; - assert!(result.is_ok()); - } - - #[test] - fn test_formula_building() { - let mut formula = SmtFormula::new(); - formula - .declarations - .push("(declare-fun x () Int)".to_string()); - formula.assertions.push("(assert (> x 0))".to_string()); - - let formula_str = formula.build_formula_string(); - assert!(formula_str.contains("declare-fun")); - assert!(formula_str.contains("assert")); - assert!(formula_str.contains("check-sat")); - } -}