Jonathan Certes

Research and teaching in information system security

Home Research Resources Teaching

Home / Research / Static root of trust on microprocessor ARM Cortex-A9

Motivation

Back in 2021, we decided to extend a solution of formally verified remote attestation for microcontroller to microprocessor ARM Cortex-A9.

Remote attestation is a protocol to verify that a remote algorithm, running on a Prover, satisfies security properties for a Verifier, allowing to establish dynamic root of trust. Modern architectures combine signature or MAC primitives with hardware monitors to enforce secret confidentiality.

Remote attestation

Our works were based on a verified hardware/software co-design for remote attestation: VRASED. Its proof is established using formal methods and its implementation is conducted on a simple embedded device based on a single core microcontroller. A heavy modification of the core, along with a hardware monitor, enforces security properties to establish a static root of trust.

Our objective was to extend this method to microprocessors where cores cannot be modified. We wondered if it was possible to tackle this problem with support from the microprocessor’s debug interface and demonstrate that the same security properties also hold.

Of course, this only works in the case where the microprocessor is an incorruptible, expected state right before the request for remote attestation. We proposed to attest the configuration of a microprocessor ARM Cortex-A9 in a different study. Here, an hypothesis is that we can set the microprocessor to this expected state before remote attestation.

Solution

We proposed a solution based on hardware/software co-design to deduce the value of useful signals at critical steps of the protocol execution. Axioms describe the behaviour of ARM CoreSight debugger in accordance with its documentation and the content of the software. New properties are verified through model-checking of the hardware. Then, we conducted a proof to show that the soundness and security properties from VRASED also hold on our system, even with no modification of the core.

We relied on a modern Systems on Chip (SoC), a Xilinx Zynq-7000, where the microprocessor ARM Cortex-A9 is integrated with a FPGA. Both the secret and the code of attesting function are stored in dedicated ROM located in the FPGA. A RAM is also located in the FPGA and is used as an exclusive stack by the attesting function. CoreSight debug interface outputs program flow traces trough a trace port interface unit to the FPGA. Signals are monitored by the hardware extension to obtain read/write addresses and information about the execution of attesting function.

Implementation on Xilinx Zynq-7000

The code of the attesting function is wrapped around with specific instructions to configure CoreSight and the MMU. As a consequence, during its execution:

In case of a future corruption, the hardware extension resets the microprocessor if the program counter is located within the attesting function. A reset also occurs if a read/write access to the secret or exclusive stack is attempted outside the attesting function.

Proof strategy

The hardware extension is described in Verilog and formally verified using our solution for automated formal verification of hardware designs. It contains the hardware monitor from VRASED.

Since the processor is left unmodified, verified properties from VRASED are expressed using deduced values for the monitored signals (not their real values) and cannot be used to prove the remote attestation security anymore. We add axioms and prove that their conjunction implies the initial VRASED security properties. These axioms form a proof obligation to be discharged by the other modules of the system.

The other modules of the system aim at obtaining CoreSight traces and access signals to memories in the FPGA, then process them to deduce values that are accepted by VRASED original automaton. The cornerstone of the deduction process is a transducer that translates the content of CoreSight traces into deduced values for the interruption signals, program counter and read/write addresses.

Proof obligations

As a consequence, the design of the hardware extension is an iterative process which can be described as follows:

  1. Security properties are defined in VRASED. We re-use the same automaton to verify a property Pn expressed from deduced predicates.
  2. Axioms An are necessary to imply the security property. These axioms form a proof obligation.
  3. Axioms An are implied by the conjunction of properties Pn+1 and axioms An+1. Rewritings with a theorem prover demonstrate that this implication is a tautology.
  4. The hardware monitor is extended to verify properties Pn+1. This hypothesis is ensured with model-checking.
  5. Steps 3 and 4 are repeated while incrementing n until the proof is based only on axioms resulting from a translation of CoreSight documentation.

The role of the trace decompresser is to identify the type of packet that is transmitted by CoreSight and inform the transducer that an event occurred. The trace decoder transmits decoded addresses and exception information to the transducer when an event occurs.

Associated resources

Implementation requires a SoC Xilinx Zynq-7000. We chose to implement our solution on a Digilent Cora Z7-07S development board.

Synthesis, place and route and implementation can be conducted with EDA suite Xilinx Vivado.

Programming the board requires a connection through UART and on chip debugger openOCD.

Model-checking is performed by NuSMV.

Proof of security is demonstrated with the Coq proof assistant.

Recorded presentation

Associated publications


no cookie, no javascript, no external resource, KISS!