Home / Research / Attestation of configuration for ARM cortex-A9 processor
Motivation
Back in 2022, we needed to place a microprocessor ARM Cortex-A9 into an incorruptible, expected state before a request for remote attestation. We previously established a static root of trust on microprocessor ARM Cortex-A9 with the hypothesis that we can set the microprocessor to this expected state.
We needed to configure the peripherals, including the MMU and the debug interface, for a critical secure hardware system and we wanted a solution empowered with formal verification. The solution needed to be compatible with a modern System on Chip (SoC), the Xilinx Zynq-7000, where a microprocessor ARM Cortex-A9 is integrated with a FPGA.
Solution
We proposed a solution based on hardware/software co-design to forbid the execution of critical functions (accessing a secret) if prerequisites are not met. A trusted algorithm is located in a dedicated ROM, where fetches from the microprocessor can be monitored by external hardware. When executed, it sets the environment of the microprocessor as expected (configures the peripherals) and triggers the monitoring of the hardware.
Expected signals are stored into a dedicated memory which is not connected to the microprocessor. A hardware monitor reads access signals from the microprocessor to the ROM (containing the code of the trusted algorithm) and debug traces from CoreSight. It compares their values with the content of its dedicated memory ; in case of a mismatch, a reset of the microprocessor is triggered.
To make sure that the trusted algorithm is properly executed by the microprocessor, the hardware extension must distinguish a fetch from a read access to the ROM. To this purpose, the design of the trusted algorithm verifies a strict specification for its architecture.
Fastest possible read/fetch on the AXI bus is by packets of 8 words. The trusted algorithm is designed to force CoreSight to output a trace every 8 instructions. Two instructions are needed to force the execution of a trace, the 6 remaining instructions configures the peripherals as expected. Of course, more than 6 instructions are needed, so this sequence is repeated.
nop
nop
nop
nop
nop
nop
add r3, pc, #0 // an indirect branch forces CoreSight to output a trace
mov pc, r3 //
// <- destination
The ROM is accessible through the Advanced eXtensible Interface (AXI)
communication interface.
CoreSight outputs its trace through a 8-bit vector called TRACE_DATA.
The hardware monitor expects these signals to match the content of its dedicated
memory.
The important part is that an attacker can try to reproduce these signals
without fetching the trusted algorithm: only with read accesses to the ROM and
indirect branches from
an other program.
The idea is that such an algorithm would introduce delays to the signals on the
AXI bus or CoreSight TRACE_DATA.
Audit
We have audited this solution and tried to reproduce the exact same signals from an external program. We pre-charged the microprocessor registers with the appropriate destination addresses and managed to force CoreSight to output the correct data without introducing any delay for 6 accesses. After 6 accesses on the AXI bus, we must re-use a register to load the proper destination address and a delay appears (which gets detected by the hardware monitor).
Formal verification
We have proven that it is not possible to output different signals on the AXI bus or CoreSight signals without triggering a reset. This proof relies on temporal properties verified by model-checking, on the hardware monitor, using our solution for automated formal verification of hardware designs. Behaviour of the memory dedicated to store the expected signals is modelled and considered axiomatic. A proof is conducted with the Coq proof assistant.
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.
- Here
are all the resources to implement the design. It contains
Verilog description of the hardware extension, TCL code to generate a
schematic for Xilinx Vivado and C code of the software. It also contains a
gdb script to program the board with openOCD. - Here are resources to conduct model-checking on the hardware
monitor.
- Here , here , and here are programs
written in Coq that prove we obtain our security.
Recorded presentations
English
French
Associated publications
- Jonathan Certes, Benoît Morgan, Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement (French), SSTIC 2022
- Jonathan Certes, Méthodes et modèles pour la vérification formelle de l'attestation à distance sur microprocesseur (French), 2023