Runtime Verification Audits World Mobile EarthNode NFT Claiming Contract
Runtime Verification is pleased to announce the World Mobile EarthNode NFT claiming contract audit completion. World Mobile, built on Cardano, is creating a mobile network built on the blockchain to connect people and communities globally.
Audit Scope
World Mobile aims to provide mobile network connectivity to under-connected parts of the globe using a decentralised, sharing economy based model supported by the blockchain. With the World Mobile protocol, users can create and operate a node to contribute to the sharing economy and provide value added services and, in return, can earn rewards in the form of WMT, the protocol's native currency.
The audit scope was limited to the World Mobile Group’s EarthNode NFT claiming smart contract, responsible for managing ownership of NFTs, which World Mobile EarthNode operators use to operate the node. The Admin (an account managed by World Mobile Group) locks the NFTs in the Ownership contract and indicates which operator can retrieve the NFT.
The EarthNode operator can retrieve the NFT by locking a fixed amount of World Mobile Tokens (WMTs) into the Ownership contract. The retrieved NFTs can be transferred freely in an open market. The owner of the NFT can release the NFT back to the Ownership contract to get back deposited WMTs. The Admin can lock, change the ownership, and retrieve the NFT only before the NFT is claimed, or after it is returned. However, the Admin cannot recover the locked WMTs while the operator holds the NFTs.
The audit scope is limited to the Haskell source code of the EarthNode NFT Claiming smart contract portion of the protocol. Issuance and burning of NFTs and other on-chain code or contracts are outside the audit scope. Any deployment and upgrade scripts, off-chain codebase, and client-side portions of the codebase were also outside the scope of the audit. A detailed list of all the contracts, libraries, and interfaces audited can be found in the report.
Methodology
Runtime Verification conducted a manual code review for a period of 3 weeks and delivered a detailed report on December 29th, 2022.
The first step of the audit process consisted of thoroughly reading through the documentation to understand the desired behavior of the code better.
Then, the code underwent a manual check to ensure all the use cases were covered and implemented correctly. During this process, a state machine was used to model the lifecycle of the WMTs and NFTs managed by the Ownership contract.
Next, potential undesired use cases that the code may encounter were tested. The discovered issues were reported to the World Mobile Group, and a best-effort review of the code fixes took place to ensure that the modified code was not introducing any new issues.
Results
The audit identified and highlighted some issues along with some informative findings. Runtime Verification conducted a best-effort review of code fixes and worked with the World Mobile Group team to incorporate code fixes into the smart contract.
Readers interested in a more detailed and technical explanation of the findings can review the full report in our GitHub repository.
About World Mobile Group
World Mobile is the first mobile network built on blockchain. With over 3 billion people left offline, digital exclusion is a significant problem. Unlike traditional mobile networks, World Mobile works with local businesses and entrepreneurs, giving them the power to connect their local communities via a sharing economy. World Mobile's hybrid network utilises air and ground assets that enable aerial connectivity, such as aerostats and AirNodes, to deliver network coverage in rural areas where previously it was impossible.
About Runtime Verification
Runtime Verification is a technology startup based in Champaign-Urbana, Illinois. The company uses formal methods to perform security audits on virtual machines and smart contracts on public blockchains. It also provides software testing, verification services, and products to improve the safety, reliability, and correctness of software systems in the blockchain field.**
