Auditing With Finite State Machines: A Complementary Methodology

This report introduces an FSM-based methodology for auditing deterministic protocols and smart contracts, demonstrates the approach with a simple Solidity transfer example, and applies it to a bridge between Stellar and a Substrate parachain. The bridge audit uncovered a critical replay vulnerability in the execute_issue() flow that allowed reuse of a Stellar transaction proof (TxProof) to finalize multiple issue requests; the developers mitigated the flaw by adding a memo-hash validation (ensure_transaction_memo_matches_hash) and integrating it into execute_issue(). The document concludes with benefits, limitations, and applicability of FSMs in security audits.