RV-TEE-Based Trustworthy Secure Shell Deployment: An Empirical Evaluation

By: Axel Curmi, Christian Colombo, Mark Vella


Incorrect cryptographic protocol implementation and malware attacks targeting its runtime may lead to insecure execution even if the protocol design has been proven safe. This research focuses on adapting a runtime-verification-centric trusted execution environment (RV-TEE) solution to a cryptographic protocol deployment — particularly that of the Secure Shell Protocol (SSH). We aim to show that through a concrete realization of RV-TEE, which is neither tied to specific CPU mode nor requires the consequential operating system support, SSH execution can be rendered trustworthy. We provide: (i) An RV-TEE setup for a popular SSH implementation based on a widely-adopted RV tool, and a USB-connected hardware security module (ii) An overview of the property extraction process through a methodical analysis of the SSH protocol specifications (iii) Security vulnerabilities identified as a result of RV-TEE adoption (iv) An overhead analysis delineating what SSH applications can benefit from our proposed setup in a practical manner.


runtime verification, trusted execution environment, cryptographic protocols.

Cite as:

Axel Curmi, Christian Colombo, Mark Vella, “RV-TEE-Based Trustworthy Secure Shell Deployment: An Empirical Evaluation”, Journal of Object Technology, Volume 21, no. 2 ( 2022), pp. 2:1-15, doi:10.5381/jot.2022.21.2.a4.

PDF | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn

The JOT Journal   |   ISSN 1660-1769   |   DOI 10.5381/jot   |   AITO   |   Open Access   |    Contact