Noninterference Analysis for Smart Contracts: Would you Bet on it?

In the context of Blockchains and Decentralized Finance the notion of Maximal Extractable Value (MEV) is attracting more and more attention. MEV is the maximum gain that users-including miners and validators-can obtain by interacting with a smart contract and with its dependencies. Such profits witness attacks that also exploit strategic transaction manipulations (e.g., reordering transactions in blocks) and distort the meaning of smart contracts. The use of the notion of noninterference for modeling and analysing MEV attacks has recently been proposed in the literature. Noninterference aims to capture unwanted information flows in multi-level systems. Various definitions of noninterference have been presented, and among these those based on unwinding conditions allow the possible flows to be specifically located in a system. In this paper we investigate the use of such unwinding conditions to analyze MEV. We exploit a simple case study-the Bet contract-to highlight the advantages and disadvantages of our proposal.