Blockchain Meets Formal Logic: Semantics Level Cybersecurity Challenges

Blockchain is a disruptive combination of dis-tributed data structures and cryptography functions in an attempt to implement the concept of trust among multiple distributed agents. It fostered the arising of diverse applications from cryptocurrencies to Distributed Autonomous Organisations (DAO), passing by smart contacts. Despite the strong crypto-graphic means employed, still, Blockchain-based technologies are not free from vulnerabilities from a cybersecurity point of view. Many countermeasures have been introduced to cope with known vulnerabilities at the network, platform, and application levels, but it is still several issues to overcome at the semantics/logical level, where the attacks target particularly smart contracts, made of logical conditions that can be seen as predicates and inference rules. Such attacks are all the more difficult to detect since they are played at the logical level. Therefore, we explore in this paper the relevance, constraints, and properties of logical frameworks to formally verify the correctness of smart contracts before their implementation and be able to solve some vulnerabilities and then prevent their related cyber-attacks.