Jonathan Certes

Home / Research / Methods and models for formal verification of remote attestation on microprocessors

Context and stakes

During my Ph.D, we considered the security of the execution for an algorithm in a complex environment. Let's imagine that we possess an algorithm on which all vulnerabilities have been removed. We want to execute it on dedicated hardware.

During the execution, the application loads its environment into the memory of such device and we can interact with it: either from a physical access or through a network.

Although, it is possible that other applications share the same hardware. Let's admit that one other application is malicious, or simply vulnerable because all vulnerabilities have not been removed. Then it can be instrumented to tamper with the properties of our application which we had previously verified.

As a consequence, before we interact with our application, it is recommended to dynamically verify its integrity and the one of its execution environment. This paradigm, where we establish a dynamic root of trust, is called remote attestation. This involves a challenge-response protocol and requires a static root of trust:

• an attesting function to compute an integrity check ;
• and an authentication mechanism so that the response provided by this attesting function can be trusted.

On a microprocessor with peripherals, the attack surface is large. The attesting function will probably need to check the integrity of the memory that is dedicated to peripherals. But more important: how do we establish a static root of trust if the state of the microprocessor and its peripherals cannot be trusted?

• can we rely on the value of the program counter if the Memory Management Unit (MMU) maps to the virtual address space?
• how do we detect a read access if data is available in cache memory and one can access it through a side channel?

Threat model

In my thesis, we considered the following threat model:

• An attacker has a remote access to the device running our application (no physical access).
• This attacker has elevated privileges: he/she can read or write any memory that is accessible from the microprocessor, re-configure all the peripherals, poison the cache memories, etc.
• The attacker corrupted the application that we aim at verifying: a remote attestation will detect its intrusion.
• A secure boot sequence is implemented on the device and this cannot be altered by the attacker. Triggering a reset of the microprocessor allows to recover a safe state.

The objective, for our adversary, is to mask the corruption of the application. Which means that the attacker has to forge a response expected by the challenge-response protocol.

• Either by altering the execution of the attesting function. For instance, by attesting a non-corrupted copy of the application.
• Or by accessing a secret involved in the authentication mechanism and computing the integrity check by himself/herself.

Contributions

We targeted off-the-shelf microprocessors and we chose to re-use a strategy available at state of the art for formal verification. In that regards, we faced several issues:

1. to conduct a formal verification of our solution, we formally express our specifications from informations available in the documentation. Which means that we could not be restricted to simple devices, where verification through model-checking can be achieved in a reasonable amount of time.
2. the target microprocessor is closed-source: we cannot modify its core and we cannot observe internal signals. For our strategy, this was a requirement to establish a static root of trust and secure the remote attestation.
3. finally, the attack surface allows to reconfigure the peripherals and to corrupt the execution environment for the attesting function. This falsifies the authentication mechanism: the response provided by the attesting function cannot be trusted.

We provided contributions accordingly:

1. we proposed a method, along with a framework, to automatically formally verify complex hardware designs.
2. we proposed an architecture to unlock verification of security properties from external signals and establish a static root of trust on microprocessor.
3. we proposed a solution to attest the configuration of the microprocessor and its peripherals, so that the execution environment does not falsify the authentication mechanism.

Recorded presentations

• Ph.D defense 2023 (English)
• Soutenance de Thèse 2023 (French)

Associated publications

• Jonathan Certes, Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur (French), 2023

---