Paper 2017/1246

Verification of FPGA-augmented trusted computing mechanisms based on Applied Pi Calculus

Alessandro Cilardo and Andrea Primativo


Trusted computing technologies may play a key role for cloud security as they enable users to relax the trustworthiness assumptions about the provider that operates the physical cloud infrastructure. This work focuses on the possibility of embodying Field-Programmable Gate Array (FPGA) devices in cloud-based infrastructures, where they can benefit compute-intensive workloads like data compression, machine learning, data encoding, etc. The focus is on the implications for cloud applications with security requirements. We introduce a general architecture model of a CPU+FPGA platform pinpointing key roles and specific assumptions that are relevant for the trusted computing mechanisms and the associated security properties. In addition, we formally verified the proposed solution based on Applied Pi Calculus, a descendant of Pi Calculus, that introduces constructs allowing the symbolic description of cryptographic primitives. The verification phase was automated by means of ProVerif, a tool taking as input a model expressed in Applied Pi Calculus along with some queries and annotations that define security properties to be proved or denied. The results of the analysis confirmed that the properties defined in our work hold under the Dolev Yao attacker model.

Available format(s)
Publication info
Preprint. MAJOR revision.
Trusted Computing
Contact author(s)
acilardo @ unina it
2017-12-30: received
Short URL
Creative Commons Attribution


      author = {Alessandro Cilardo and Andrea Primativo},
      title = {Verification of FPGA-augmented trusted computing mechanisms based on Applied Pi Calculus},
      howpublished = {Cryptology ePrint Archive, Paper 2017/1246},
      year = {2017},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.