ARM Architecture
ConceptARM Architecture is treated in the evidence primarily as a weakly consistent instruction-set platform studied in systems-security and binary-analysis research. The supplied evidence covers ARM in four principal contexts: (1) as a target ISA for differential testing of instruction decoders (Fleece), where ARMv8 has comparatively few but real decoding errors; (2) as a hardware-security-feature substrate for in-process compartmentalization using Pointer Authentication (PA) and Memory Tagging Extension (MTE) (Capacity); (3) as an evaluation architecture for post-quantum cryptography benchmarking (PQC-LEO); and (4) as a weakly consistent multiprocessor architecture whose programmer-visible concurrency behaviour requires more elaborate semantics than simple state-update or store-buffer models, motivating integrated ISA-plus-concurrency-model specifications (the Sail/POWER/ARM line of work).
First seen 7/3/2026
Last seen 8/11/2026
Evidence 22 chunks
Wiki v4
WIKI
Overview
Across the supplied evidence, ARM Architecture is positioned primarily as a weakly consistent instruction-set platform that is studied, evaluated, and exploited in systems-security and binary-analysis research. The evidence treats ARM in four principal contexts:
- As a weakly consistent multiprocessor ISA whose programmer-visible concurrency behaviour cannot be expressed as a simple per-instruction state-update model, motivating the development of integrated ISA-plus-concurrency-model specification frameworks such as Sail.
- As an ISA used as a differential-testing target for instruction decoders (Fleece), where ARMv8 instruction encoding is examined alongside x86-64 and PowerPC.
- As a modern hardware platform whose newer security features (Pointer Authentication, Memory Tagging Extension) substitute for x86's Protection Keys for Userspace (PKU) and can be retrofitted into a capability-based in-process access control scheme (Capacity).
- As a principal evaluation architecture in a post-quantum cryptography benchmarking framework (PQC-LEO), where performance scaling differs from x86.
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
12 connectionsSeveral hypervisor verification efforts target the ARM architecture.
TrustZone is a security technology in ARM architecture.
Fleece is used to test decoders for ARM architectures.
Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture (reid:fmcad:2016) ← evaluates 97% 1e
The paper presents trustworthy specifications of ARM v8-A and v8-M architectures.
Who Guards the Guards? Formal Validation of the ARM v8-M Architecture Specification (reid:oopsla:2017) ← evaluates 97% 1e
The paper formally validates the ARM v8-M architecture specification.
Modelling the ARMv8 Architecture Operationally: Concurrency and ISA (flur:popl:2016) ← evaluates 97% 1e
The paper models the ARMv8 architecture operationally, covering concurrency and ISA.
Examiner tests ARM devices against CPU emulators.
ASL is the language used to specify the ARM architecture.
ISA-Formal is used to verify ARM processors.
Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 (pulte:popl:2017) ← evaluates 97% 1e
The paper provides axiomatic and operational models for ARMv8 concurrency.
The paper covers ARMv8-A architecture semantics.
The paper verifies ARM processors using the ISA-Formal approach.
CITATIONS
10 sources10 citations — click to expand
[1] ARM is grouped with IBM POWER as a weakly consistent multiprocessor that cannot be modelled with a simple per-instruction state-update semantics; TSO architectures (x86, Sparc) require only per-thread store buffers, while ARM and POWER expose additional out-of-order and speculative behaviour to the programmer. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors
[2] The Sail paper names ARM alongside POWER as a key motivation for executable, mathematically rigorous architectural envelope specifications, arguing that traditional ARM/POWER documentation is inadequate to define allowed concurrent behaviour, serve as a test oracle, or act as an emulator. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors
[3] Fleece Table II reports ARMv8 testing with 6,051 inputs, 4,337 differences, and a runtime of 3:09, compared with 482,711 inputs in 508 minutes for x86 and 3,629 inputs in 1:02 for PowerPC, with the paper noting that x86 testing generated about 100x as many inputs as ARM and PowerPC testing. Structured Random Differential Testing of Instruction Decoders
[4] Fleece Table IV reports that on ARM, Fleece-generated inputs yield 4,337 unique differences from 6,051 inputs in 3:09, whereas random inputs process 1,706,422 ARM inputs in 10 minutes yielding only 600 unique differences, attributed to the rarity (1 in 32768) of opcodes with 15-bit opcode or reserved fields in random input. Structured Random Differential Testing of Instruction Decoders
[5] Fleece Table III records per-decoder error counts on ARMv8: XED n/a, libopcodes 2, LLVM 1, Dyninst 7, Capstone 3, with ARMv8 decoders having the fewest errors among tested architectures. Structured Random Differential Testing of Instruction Decoders
[6] ARM-specific Table I example errors in Fleece: libopcodes producing `mov w8, w26` instead of `orr w8, wzr, w26, lsr #4`; LLVM reporting valid `ldaxrb w24, [sp]` as invalid; Dyninst producing `eor q9, q5, q0` rather than vector-form `eor v9.16b, v5.16b, v0.16b`; Capstone reporting invalid for bytes decoding to `mov v10.h[7], v11.h[2]`. Structured Random Differential Testing of Instruction Decoders
[7] Fig. 6 of the Fleece paper shows a single ARM instruction (bytes `0x630844e0`) decoded differently across libopcodes, Capstone, Dyninst, and LLVM: libopcodes and LLVM produce valid decodings that reassemble to the input bytes, Capstone reports invalid, and Dyninst produces an erroneous decoding that fails reassembly. Structured Random Differential Testing of Instruction Decoders
[8] The Fleece paper notes that both ARM and PowerPC have undergone significant revisions, each requiring decoder updates, and that extensions can produce new opcode-operand interactions affecting existing instructions. Structured Random Differential Testing of Instruction Decoders
[9] The Capacity paper states that modern ARM lacks a PKU-equivalent feature, and instead newer ARM architectures introduced Pointer Authentication (PA) and Memory Tagging Extension (MTE), which Capacity uses together with PA-key-authenticated intra-process domains to implement capability-based in-process compartmentalization. Capacity
[10] The PQC-LEO framework automates evaluation of PQC computational and networking performance across x86 and ARM, with the proof-of-concept showing greater performance reduction for higher-security PQC methods on ARM than on x86. PQC-LEO