A Formal Verification Model for Security Vulnerability in Non-Fungible Tokens (NFTS) Platform.

Abstract

Non-fungible tokens have been a unique transformation in the implementation of the concept of distributed ledger technology in digital assets. NFTs are said to be non-interchangeable, which distinguishes its value from fungible tokens like Bitcoin (Btc). Scammers are utilizing the open source nature of the blockchain to victimize users and steal their NFTs, leaving NFT collectors with infringed artwork. In a bid to eliminate security vulnerability and attack in NFT platform, we implemented a smart contract verification model. Our verification model is a 2-pronged approach that utilized F*, functional programming language. We presented two tools that translated solidity source code and EVM bytecode to solidity* and EVM* respectively. The EVM decompiler analyzes contracts in which the solidity source codes are unavailable as well as low level properties of contracts. The EVM* and Solidity* tools helped to check the equivalence between a solidity program and the bytecode output from the solidity compiler in order to avoid bugs and preserve verified properties at the source level. In this paper, Etherscan token tracker was used to verify and authenticate NFT token before buying or minting such NFT. Keywords: Non-Fungible Tokens (NFTs), The NFT- marketplace (NFTM), Ethereum