In this article, we discuss the use of Finite State Machines (FSMs) as a complementary methodology that has proven effective in enhancing the auditing process. During a recent bridge audit, this approach led to the identification of a critical vulnerability. FSMs serve as valuable tools for discovering bugs in the implementation of a project design. To better comprehend the relevance and functionality of FSMs in the Web3 domain and smart contract auditing, we will begin with definitions of smart contracts, protocols, and FSMs.

A smart contract is a set of rules programmed to execute automatically and deterministically on a blockchain.

In the realm of software engineering, a protocol defines a set of rules that must be adhered to for achieving a particular goal. It stipulates agreements among various systems on data formatting, data processing, and data communication.

Adapting the traditional definition of FSMs to suit the Web3 context, we find that a finite state machine accepts or rejects an input based on a unique sequence of states determined by the tuple (initial_state, input, final_state). Certain security constraints, referred to as S1, are integral to the initial state (S1 ∈ initial_state). Additional security constraints, denoted as S2, pertain to the inputs (often implied by a transaction to be executed). Hence, we can express these as S2 ∈ inputs, and the total "security constraints" can be denoted as S1 ∪ S2.

Therefore, a DLT system can be modeled as a function of the current state (the ledger, or blocks) and inputs (such as pending transactions from the mempool set for the next block). This relationship can be succinctly described as dlt(state, inputs) => new state or produce_block(blocks_so_far, current_transactions) => new block. This formulation underscores why the aforementioned tuple is sufficient for verifying the legitimacy of transitions. Furthermore, in systems where the execution of smart contracts can be linearized, one may consider the execution of each transaction as a discrete step. In this case, the function is closely related and can be presented as process_transaction(state_of_execution_environment, transaction) => new_state.

Given that a protocol is an agreed set of rules and a smart contract is a deterministic set of rules, we can define smart contracts as deterministic protocols. Consequently, a deterministic protocol can be modeled as a finite-state machine.

To ensure security by design and to guarantee that the contract implementation aligns with the intended design, it is advisable to encode the deterministic rules of a smart contract as a protocol and abstract them as an FSM. This approach ensures the correct logical functioning of the smart contract for any given input.

Simple Transfer in Solidity

In this section, we first outline a basic example to explain the methodology. Subsequently, we demonstrate how Finite State Machines (FSMs) can be applied to more complex systems.

To illustrate, let's design a simple state machine for the transfer function of a Solidity smart contract. Consider the code snippet provided below.

function transfer(address from, address to, uint256 amount) {
require(from != address(0), "ERC20: transfer from the zero address");

uint256 fromBalance = _balances[from];
require(fromBalance >= amount, "ERC20: transfer amount exceeds balance");
_balances[from] = fromBalance - amount;
_balances[to] += amount;

emit Transfer(from, to, amount);
}

Code Block 1: Simple Transfer in Solidity

Imagine a scenario where User A wishes to transfer a specific amount of tokens to User B. Importantly, the burning of tokens—i.e., transferring them to a zero or burn address—should not be permitted in this case. Given this context, a successful transfer in Solidity necessitates three key checks:

The from account must not be a zero address. The to account must not be a zero address. The from account must have a balance greater than or equal to the amount being sent.

These conditions can be formalized, as shown in Table 1:

Table 1: Condition Table

Given the straightforward nature of this transfer, it initiates at a single starting state—where the function is invoked (state 1: transfer function is called). It can then transition to various end states, each contingent on meeting specific conditions. The potential final states are detailed in Table 2:

Table 2: Final State Table

Thus, the state transitions can be enumerated as:

• 1 → 2.a
• 1 → 2.b
• 1 → 2.c
• 1 → 2.d

After the initial analysis and definition of the transfer protocol, an FSM diagram can be created, as will be illustrated in Table 3.

Table 3: State Transition Table

Finally, we can draw the state diagram as in Figure 1:

Figure 1: Flow State Machine Diagram

The FSM we built can help us to verify that the conditions are held in a particular code implementation. By creating assertions based on this FSM, we can easily identify code anomalies, such as the violation of the flow 1→2.c in the given code. In this specific case, the function fails to return an error, revealing a missing check and thereby indicating a security vulnerability.

While our simplified example allows for full representation of all flows, including errors, in one diagram, this approach becomes impractical for more complex cases due to an explosion in the number of states. To mitigate this, we must abstract further, separating errors from other flows to create a more manageable and readable FSM.

Simplification of Simple Transfer in Solidity

The next step involves streamlining our FSM by removing the error states. Table 4 shows that the conditions remain consistent, even after this simplification.

Table 4: Condition Table

By focusing solely on the successful transfer outcome, we can substantially reduce the complexity of the FSM. Table 5 illustrates the simplified flow, depicting only the final state where the transfer is successful.

Table 5: Final States Table

As a result, we can define a set of state transitions.

List of State Transitions

• 1 → 2

With this preliminary analysis, we can construct the FSM state transition table, shown in Table 6. Based on this, a state diagram can be created, as demonstrated in Figure 2.

Table 6: State Transition Table

Figure 2: Flow State Machine Diagram

In this final representation, the diagram deliberately omits error states, concentrating instead on transitions that result in on-chain state modifications. It specifies the security conditions that must be met for each state transition to be valid.

Application to a Bridge Audit

The utility of this FSM methodology isn't confined to simple examples; it also extends to complex systems. For instance, in the audit of a bridge codebase designed for the Stellar and a Substrate-based parachain, our FSM model played a pivotal role. It helped uncover a replay attack, subsequently classified as a critical vulnerability. Here we spotlight how FSMs model one of the main flows of the issue protocol in the bridge, derived from the Interlay Protocol Specification.

Issue Protocol

The issue protocol takes center stage as we dissect its different flows through the lens of FSMs. For illustrative purposes, we include the pseudo-code (Code Block 2) highlighting the vulnerable sections. The actors, definitions, and prerequisites for a successful operation are laid out as follows:

//This function allows users to open an issueRequest of a certain amount targeting a specific vault. 

fn _request_issue(
requester: T::AccountId,
	amount_requested: BalanceOf<T>,
		vault_id: DefaultVaultId<T>,
	) -> Result<H256, DispatchError>{
...
}

//This function allows users or vaults to cancel a previously opened issueRequest.
fn _cancel_issue(
requester: T::AccountId, 
issue_id: H256
) -> Result<(), DispatchError> {
...
}

//This functions allows users or vaults to execute the previously openend issueRequest, de facto finalizing the brinding procedure. 
fn _execute_issue(
	executor: T::AccountId,
	issue_id: H256,
	transaction_envelope_xdr_encoded: Vec<u8>,
	externalized_envelopes_encoded: Vec<u8>,
	transaction_set_encoded: Vec<u8>,
	) -> Result<(), DispatchError> {

...

	// Verify that the transaction is valid
	ext::stellar_relay::validate_stellar_transaction::<T>(
		&transaction_envelope,
		&envelopes,
		&transaction_set,
	)?;
	let amount_transferred: Amount<T> = ext::currency::get_amount_from_transaction_envelope::<T>(
		&transaction_envelope,
		issue.stellar_address,
		issue.asset,
	)?;

...
}

Code Block 2: Issue Protocol Pseudo-Code

The actors involved in this protocol and the definitions used, as well as the set of preconditions needed for this flow to be successful, are presented here.

Actors:

• User
• Vault

Definitions:

• C: Collateral Locked by the Vault.
• CT: 1.5 (150%) Collateral Threshold.
• GCT: GriefingCollateralThreshold
• X: Amount Of Tokens.
• GFC=X*GCT=Griefing Collateral.
• TxP: Proof Of Stellar Transaction.
• IRR: ReferenceIssueRequest
• HG: IssuePeriod "Hourglass"

Precondition:

• Vault V is not banned
• X exceeds the minimum threshold (min)

The protocol is initiated when a user sends a request_issue(X) transaction. The user, after initiating the request on the Substrate parachain, is then mandated to send an equivalent transaction on the Stellar network. In mathematical terms, this can be modeled as:

• User calls request_issue(X) on the Substrate parachain.
• User sends on Stellar (X+y) with y ∈ R.

Thus we can distinguish three different scenarios:

• y=0
• y<0
• y>0

Issue Protocol, Scenario y=0

Let's zero in on the ( y = 0 ) scenario. Here, the FSM comes into play with the following four components:

• Q: A finite set of states
• ConL: A finite set of Conditions
• TF: A finite set of transition functions
• STp: A set of accepted state transitions

Tables 7 and 8 will map out the various states and conditions, but for the sake of this discussion, let's break down the potential final states.

Sets:

• Q={1; 2; 3; 4; 5.a; 5.b; 5.c}
• ConL= {C>=(1.5)X; User.Balance>=GFC == User.Balance>=X*GFT; User has called request_issue; HG!Over; IssueID ! used before; TxProof! used before; User must be the same of State 2; HGisOver; Flow 1 → 2 → 4 → 5.c;TxProof is related to IssueID}
• TF={UserCall request_issue;HG Expires; UserCall executeIssue; VaultCall cancel_issue; User sends Tx on Stellar with Memo=issueID}
• STp={1→2; 2→3; 2→4; 3→5.a(1); 3→5.a(2); 3→4; 4→5.b; 4→5.c}

As we can see from the set of states, there are three possible final states and ten conditions to be held that can be described as follows in Table 7 and Table 8.

Table 7: Final States Table

Table 8: Condition Table

Moreover, we defined a set of accepted state transitions as STp={1→2; 2→3; 2→4; 3→5.a(1); 3→5.a(2); 3→4; 4→5.b; 4→5.c}. Wrapping up the states, conditions, and the accepted transition, we can build a state transition table, as shown in Table 9, and finally draw the flow state machine diagram as in Figure 3.

Table 9: State Transition Table

Figure 3: Flow State Machine Diagram

The above diagram depicts the four possible flows for this particular scenario:

1. 1 → 2 → 3 → 5.a(1)
2. 1 → 2 → 3 → 5.a(2)
3. 1 → 2 → 3 → 4 → 5.b
4. 1 → 2 → 4 → 5.c

The bridge audit illuminated critical vulnerabilities, one of which was a breach in the flow 1 → 2 → 3 → 5.a(1) by leveraging proof-of-concept attacks. Notably, this violation exploited a design flaw in the execute_issue() function, rendering it susceptible to Replay Attacks. This case study serves as an exemplification of the merits and limitations of using Finite State Machines (FSMs) as an auditing methodology.

fn _execute_issue(

...

	// Verify that the transaction is valid
	ext::stellar_relay::validate_stellar_transaction::<T>(
		&transaction_envelope,
		&envelopes,
		&transaction_set,
	)?;

	let amount_transferred: Amount<T> = ext::currency::get_amount_from_transaction_envelope::<T>(
		&transaction_envelope,
		issue.stellar_address,
		issue.asset,
	)?;

...
}

Code Block 3: Issue Protocol Vulnerable Code

The infringement in question pertained to the flow 1 → 2 → 3 → 5.a(1). It emerged that the execute_issue() function did not satisfactorily vet whether a transaction proof (TxProof) had been reused. This oversight violated the condition C7, thereby exposing the system to Replay Attacks. In practical terms, this could facilitate multiple issue requests targeting the same vault, all anchored by a singular Stellar transaction.

Remediation

Upon recognizing this critical vulnerability, the development team initiated an immediate response. The codebase was amended to include a function—ensure_transaction_memo_matches_hash—within the stellar_relay module. Invoking this function within execute_issue() now ensures that condition C7 is not contravened, thereby neutralizing the vulnerability.

pub fn ensure_transaction_memo_matches_hash<T: crate::Config>(
		transaction_envelope: &TransactionEnvelope,
		expected_hash: &H256,
	) -> Result<(), Error<T>> {
		<stellar_relay::Pallet<T>>::ensure_transaction_memo_matches_hash(
transaction_envelope,
expected_hash,
)
}

fn _execute_issue(
...
ext::stellar_relay::ensure_transaction_memo_matches_hash::<T>(
	&transaction_envelope,
	&issue_id,
)?;

// Verify that the transaction is valid
	ext::stellar_relay::validate_stellar_transaction::<T>(
&transaction_envelope,
	&envelopes,
	&transaction_set,
)?;

let amount_transferred: Amount<T> = ext::currency::get_amount_from_transaction_envelope::<T>(
		&transaction_envelope,
		issue.stellar_address,
		issue.asset,
	)?;
...
}

Code Block 4: Issue Protocol Code Fix

Methodological Analysis

Benefits of Using FSMs

• Enhanced Codebase Comprehension: FSMs deliver the auditor an intuitive blueprint of the underlying codebase. This schema expedites the identification of key functions and their expected behaviors, rendering the audit process more efficient.

• Quantifiable Security: With a limited set of states and transitions, FSMs enable the quantification of security risks. Assertion mechanisms can be embedded directly into the codebase to validate state transitions, reducing the potential for undetected vulnerabilities.

• Aids Formal Verification: The FSM methodology can complement formal verification processes, assisting in the identification of properties that warrant meticulous scrutiny.

• Fuzz Testing Compatibility: FSMs can also be employed in fuzz testing to randomly input state transitions and validate security constraints, adding another layer of robustness to the audit.

Limitations of the FSM Approach

• Necessity for Protocol Specification: The methodology's success hinges on the availability of an extensive protocol specification. Absence of this foundational document considerably impedes the usage of FSM in the auditing process.

• Scalability Concerns: In larger codebases, the complexity of managing multiple flows can become computationally prohibitive, demanding the deconstruction of main flows into sub-flows.

• Model Abstraction Risks: Incorrectly abstracting the protocol into an FSM can result in a skewed or incomplete representation, potentially leading to overlooked vulnerabilities.

The application of FSMs in this bridge audit showcased the methodology's potential for precise, data-driven security assessments while also highlighting areas that require caution. Therefore, while FSMs offer a transformative approach for blockchain security audits, their deployment should be considered alongside these intrinsic limitations.

Applicability of the FSM Methodology in Auditing

The Finite State Machines (FSMs) methodology is not confined to a particular use-case; its utility extends to deterministic protocols and smart contracts within any deterministic Distributed Ledger Technology (DLT) framework. This adaptability makes FSMs a potent tool in Design Audits, which focus on validating the congruity between the project's design and its actual implementation. FSMs are especially impactful when scrutinizing critical sections of a project, lending themselves to a multidisciplinary approach that could include manual auditing, fuzz testing, and formal verification.

FSMs champion the principle of 'Security by Design,' allowing projects to embed security measures at the blueprint stage. The methodology works in tandem with other auditing techniques, giving auditors a comprehensive toolbox for unearthing vulnerabilities that could otherwise go unnoticed.

Conclusions and Takeaways

In this article, we have shown a possible application of FSMs in the auditing process, an approach that has led to the discovery of a critical vulnerability. We've further enriched the discussion by highlighting the benefits, limitations, and potential applicabilities of this complementary methodology.

The primary takeaways can be summarized as:

• FSMs offer a well-defined framework for examining a system's diverse states and transitions, making it easier to comprehend intricate blockchain designs.

• FSMs render security attributes measurable. By defining and assessing state transitions and associated security conditions, auditors can quantify risks, something rarely feasible with other auditing methodologies.

• FSMs serve as invaluable adjuncts to formal verification procedures. They identify which properties are crucial to the protocol and should undergo rigorous testing.

• For FSMs to be effective, detailed documentation covering protocol specifications, business logic, and design choices is non-negotiable.

• Despite the merits of this approach, FSMs are not a panacea. Larger codebases could lead to computational bottlenecks, necessitating a segmented approach to manage flows and transitions.

In light of the above, it's incumbent upon development teams to adhere to best practices in software engineering. This means producing thorough documentation that not only encapsulates business logic and protocol definitions but also design choices. Such documentation serves as the bedrock for auditors to translate these specifications into FSMs. This meticulous approach magnifies the chances of detecting design inconsistencies at an early stage, thereby reinforcing the project's overall security architecture.

The case for FSMs in security audits is robust, but it should not be considered a substitute for other methodologies; rather, it should be part of a multi-faceted approach to create a more secure and resilient system.

Related Work

The state of the art on the application of FSM or Deterministic Finite Automata (DFA) to blockchain technologies shows how it is possible and beneficial to describe a smart contract as an FSM.

Craig S. Wright in Systems and Methods for Implementing Deterministic Finite Automata (DFA) via a Blockchain demonstrates how the approach is practical for the Bitcoin Blockchain.

Adrian Colyer in Designing Secure Ethereum Smart Contracts: a Finite State Machine Approach proposes FSolidM, a novel framework for creating secure smart contracts. FSolidM allows users to develop smart contracts using both a graphical and a code view and enables the definition of a smart contract as a finite state machine.

Apurba Pokharel in Modeling Blockchains as a Deterministic Finite Automata gives insight into how to approach the modeling process.

All these efforts are limited to the description of the modeling process. To the best of our knowledge, there are no prior examples of applying the FSMs to the security auditing process.