Messaging applications have become essential for communication, especially with respect to sharing sensitive information, such as personal and financial data. Unfortunately, these applications are susceptible to cyber-attacks that tend to jeopardise the confidentiality and integrity of our data. Cryptographic systems are used to secure messages, and in particular the X3DH protocol is a system that enables users to exchange keys securely to ensure that their messages remain private and tamper-proof. However, attackers could still target theoretically secure cryptographic systems that have been implemented correctly.
To ensure that cryptographic systems such as X3DH would be executed properly and securely, researchers and developers have used formal verification methods or manual code reviews. Formal verification methods involve a rigorous process of mathematically proving that a software system would meet its requirements, whereas manual code reviews require human experts to examine a software’s code for security vulnerabilities or other issues. Both methods could be time-consuming and prone to errors.
In an attempt to address this issue, this project proposes a solution that uses technology known as RV-TEE (runtime verification with trusted execution environment) to ensure secure and proper execution of the X3DH protocol. The solution combines two powerful methodologies: runtime verification and hardware-based security. Runtime verification would check the program’s behaviour while it is running, and hardware-based security would create a trusted execution environment to isolate security-critical code from potential malware and untrusted code, providing an additional layer of security.
The approach for carrying out this solution was split into three stages or processes. Firstly, the protocol was implemented by acquiring a pre-existing, open-source implementation (‘A’ in Figure 1). Secondly, a set of rules and properties was established using the protocol’s documentation, which was used in Larva (a runtime verification tool) to check that the process was running as intended (‘B’ in Figure 1). Lastly, the protocol was split into two environments: the rich execution environment (REE) and the trusted execution environment (TEE). The TEE used the hardware security module (HSM) to perform the security-critical code. Larva was used, here, to confirm that the new implementation of the protocol was still functioning as expected (‘C’ in Figure 1).
By using RV-TEE to confirm the proper execution of the X3DH protocol, this solution offers a high degree of assurance that the protocol would be executed correctly, thus further reassuring users that their messages would remain private. Furthermore, utilising HSMs attached to stock hardware over standard interfaces would ensure secure execution, even if an attacker were to gain access to the software running on a device.
The proposed solution promises to be cost-effective, and efficient because it builds upon existing hardware security modules that are widely available. By ensuring that cryptographic systems, such as X3DH, execute correctly and securely, this solution offers a new approach towards improving security in messaging applications.
Figure 1. The methodology for the proposed solution
Student: Kirsty Borg
Supervisor : Dr Christian Colombo