Verifying a Blockchain-Based Remote Debugging Protocol for Bug Bounty

We address the problem of a mutual agreement between a bug bounty issuer and a bounty hunter in blockchain smart contracts. Our framework is VeriOSS, where a Proof of Knowledge protocol is used. Through it, the hunter communicates in clear increasingly large portions of the detected bug and gets back increasingly ample portions of the reward, provided that the issuer considers the received information plausible. The process is iterated until the entire bug is revealed and the entire reward given. We formalize this protocol using the Applied Pi-calculus and we apply ProVerif to it so as to verify its correctness, i.e., that only the relevant information and the corresponding reward are exchanged and that the integrity and the authenticity of the communications is granted.