Modeling Trust Relationships in Blockchain Applications: The Case of Reconfigurable Systems-on-Chip

Nowadays, System-on-Chip (SoC) components are found everywhere in all kinds of smart devices. Each System-on-Chip contains many different blocks that provide specific functionalities, such as WiFi or Bluetooth connectivity. Whereas integrating each such block in a SoC typically requires paying some royalties, not all blocks are necessary for all applications, or throughout a device's lifecycle. Moreover, it is not possible to manufacture a specific SoC for each application. Significant advantages are therefore expected to be gained by enabling trustworthy remote SoC reconfiguration throughout their life cycles. A few approaches attempting to address this challenge have been proposed in the literature. They are typically based on Blockchain technology in order to support decentralization without relinquishing trust. Reviewing these approaches lead us to identify a potential flaw in the proposed protocols. Indeed, a SoC should be able to trust Blockchain information that it is given, without requiring any centralization. In order to validate our suspicions, we propose in this paper to use Verifpal: a cryptographic protocol verification tool that works from textual protocol models. We use it in a slightly unorthodox way in order to model the trust relationships in one of the approaches from the literature, and to verify it. The results show that, under some assumptions, a flaw is indeed present. We propose and model several possible fixes, and present their respective limitations.