In recent years, multiple solutions have been proposed for blockchain interoperability. However, designing these solutions is complex, and design failures have caused great economic damage to their owners. Safety and liveness are essential properties for these solutions, and formalisation eases their verification. However, only a few efforts were performed to formalise interoperability solutions with known formal methods. TLA+ and PAT were previously used; however, the Event-B method has not been explored, although it might be a suitable approach.

Researchers at Pyxis (Guzmán Llambías) and Universidad de la República (Laura González, Raúl Ruggia and Guzmán Llambías) from Uruguay explored the formalisation of a gateway-based interoperability solution with the Event-B method. The results showed that the method was suitable and that a straightforward specification could be developed considering Ethereum and Hyperledger Fabric as the involved blockchains. The specification was assessed with three strategies that enabled its verification and validation: formal verification (e.g. safety properties), functional validation, and functional utility. These promising results constitute a step forward in the development of formal specifications for blockchain interoperability solutions.

In this post we present a resume of the research, the full research paper can be found here.

Key takeaways: Event-B can be considered as a promising method to formalise blockchain interoperability solutions as the gateway-based approach.

Key takeaways: The main use for using Event-B is to obtain a formal proof for the main safety properties the system must comply with.

Key takeaways: Event-B animations provide a communication tool with domain experts without Event-B knowledge to validate the functional behaviour of the gateway.

Event-B

Event-B is a method based on first-order logic and type-based theory that enables the formalisation of systems that can be modelled as discrete transition systems. Event-B

models enable the verification of the functional correctness of the system and the safety properties they must comply with. The main use for using Event-B is to obtain a formal proof for the main safety properties of the system. Several use cases running in production now are the Ariane 5 rocket, part of the NYC subway line, and part of the Paris Métro line.

A nice introduction to Event-B can be found here.

The Rodin Platform is an open-source software to aid in the construction and verification of Event-B models [21]. It can be used with a ProB model checker and animator to validate and animate the model. Rodin comes with a set of provers that can automatically discharge POs. Verifying POs enables to design Event-B models (and refinements) correct by construction.

Why formalise a blockchain interoperability solution with Event-B?

Developing Blockchain interoperability solutions is complex and costly (errors have cost millions of dollars to existing solutions123). Software architects and developers must ensure that their design decisions guarantee safety and liveness properties. Safety properties prevent an undesirable state or event from occurring, whereas liveness properties imply that a state or event will eventually occur in the system. An example of a safety property in a blockchain interoperability solution is that a transaction is relayed from a source blockchain to a target blockchain, only when it is final. Non-finalised transactions cannot be relayed. On the other hand, a liveness property is that every finalised transaction will be eventually relayed from the source to the target blockchain.

Ensuring safety and liveness properties by design is complex and Event-B may help to generate formal proofs that these properties are met by design.

The gateway-based approach

The gateway-based approach for blockchain interoperability comprises pieces of software hosted aside each blockchain that know how to interact with it (i.e. submit transactions and listen to events). In addition, gateways define a protocol to exchange messages between them, enabling blockchain interoperability by exchanging cross-chain transactions. Figure X presents a high-level overview of a gateway. For each blockchain, there exists a connector that can interact with it. Whenever a smart contract on the source blockchain emits a cross-chain event, this event is listened by the blockchain connector. The connector transforms the received event into a canonical message data format and redirects the message to the router component. Each message has a destination (i.e. blockchain and a smart contract) that enables the Router component to route it to the connector related to the destination (i.e. target connector). The target connector receives the canonical message, transforms it into the target blockchain data format, and submits a transaction to the target smart contract.

Fig. 3 illustrates the behaviour of the gateway. First, the gateway subscribes to the events emitted by the smart contract on the source blockchain. Second, the user initiates a cross-chain transaction (cc-tx) by submitting a local transaction to the source smart contract. This local transaction contains the data required to invoke the target smart contract. Third, the source smart contract processes the transaction and emits an event. Fourth, the gateway listens to the event and invokes the target smart contract by submitting a local transaction using the event data.

Event-B modelling

We modelled the Gateway behaviour of one-way smart contract invocation from Fabric to Ethereum, and from Ethereum to Fabric. The full Event-B specification can be found here.

Modelling Ethereum to Fabric smart contract invocation

Fabric has authentication and authorization mechanisms and do not allow any user to submit a transaction. Only authenticated and authorised users (i.e. write grant) are allowed to submit a transaction. These safety properties are required to enable cross-chain transactions originated from Ethereum and targeted to Fabric. This means the gateway must have a Fabric user and have write permissions. Figure X presents how these safety properties were modelled with Event-B.

Requirements to be modelled:

• Every submitted transaction to Fabric must be authenticated.
• Every submitted transaction to Fabric must be authorised.

Modelling Fabric to Ethereum smart contract invocation

Ethereum does not require any authentication or authorisation requirements, but their users must pay a fee to submit a transaction. This requirement defines the behaviour of the Gateway, who must have a wallet in Ethereum and enough Ethers to submit a transaction. This behaviour was modelled in Event-B to formally describe the Gateway behaviour when submitting transaction to Ethereum. Figure X presents how these requirements were modelled with Event-B.

Requirements to be modelled:

• Submitting a transaction to Ethereum implies that the Gateway must pay a fee to the validators to process the transaction.
• The balance of each address must be equal or greater than zero. (Safety property)

Formal proofs

The Event-B model was formally verified using proof obligations (POs), which determined its correctness. The Rodin platform automatically generated 23 POs for all machines (see Table X): 17 were invariant preservation PO rules (INV), and six were well-definedness PO rules (WD). INV rules verified that the defined invariants were preserved at any state change in the machine. WD rules verified that formulas used in axioms, guards, actions, and invariants were well-defined (e.g. x divided by 0 is not a well-defined formula). All POs were automatically discharged by Rodin. Overall, it was proved that each machine’s invariants, guards, and actions were defined properly and correctly by its construction.

Key takeaways: The Rodin Platform enabled automatic formal proof generation of safety properties. In addition, it enabled a formal verification of the correctness of the Event-B model.

Functional validation

Animation of Event-B models enables users without Event-B knowledge to validate the functional behaviour of the specification. Animations of the interaction from Ethereum to Fabric can be found here and the interaction from Fabric to Ethereum can be found here.
These animations enable the user to select the execution of events with its corresponding parameters. The safety properties checked that undesirable states were not reached, as is shown in these animations. For example, if the gateway is not authorised, it cannot submit transactions to Fabric. These interactive animations enabled functional validation of the specification.

Conclusions

To sum up, this post presented a resume of our preliminary research results towards the formalisation of blockchain interoperability solutions with Event-B method, to guarantee safety and liveness properties. Future work will include to prove more properties like transaction finality and model blockchain interoperability patterns (link to the other post).

_____________________________________________________________________________________________

[1] https://cointelegraph.com/news/wormhole-token-bridge-loses-321m-in-largest-hack-so-far-in-2022

[2] https://cointelegraph.com/news/nomad-token-bridge-drained-of-190m-in-funds-in-security-exploit

[3] https://cointelegraph.com/news/breaking-harmony-one-s-horizon-bridge-hacked-for-100m