Blockchain-enhanced smart contracts for formal verification of IoT access control mechanisms

Technologies like Bluetooth and WiFi enable more and more devices to become interconnected, forming the IoT ecosystem. However, this growing connectivity brings significant security risks, especially in terms of access management. Blockchain technology, alongside smart contracts, has introduced novel ways to address trust concerns in decentralized networks. Traditional internet of Things (IoT) access control models rely on centralized authorities, making them vulnerable to single points of failure. Additionally, many smart contracts deployed today have exploitable weaknesses that can be leveraged to steal digital assets. To address this issue, we propose a decentralized approach, leveraging blockchain technology and smart contracts to ensure security and trust. Our methodology formalizes smart contract behavior using Transition Systems (TS) and Computation Tree Logic (CTL), allowing for the verification of key properties. Solidity code is translated into the Verds model-checking tool, which validates the correctness and security of the contracts. Our experiments demonstrate that the method is both scalable and effective, ensuring secure execution of smart contracts in dynamic IoT environments. This approach not only mitigates security risks but also highlights the potential of formal verification in improving the robustness of smart contracts, making them suitable for deployment in real-world applications.