diff --git a/CHANGES.md b/CHANGES.md
index 6cf58194e..277330355 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -53,6 +53,16 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
 
   This was found by Alison Felizzi and independently by Ryan Barry during the integrity proofs for AArch64 hyp mode.
 
+* Fixed: under some circumstances, `seL4_VCPUReg_CPACR` is saved twice to the current VCPU. The value of this
+  register may change between saves, causing the latter save to unintentionally grant EL0/1 access to the FPU.
+
+  1. A thread with an active current VCPU switches to a thread without a VCPU. The current VCPU is disabled.
+    1.1. `seL4_VCPUReg_CPACR` is saved to the current VCPU.
+    1.2. `enableFpuEL01` updates the register, enabling FPU access in EL0 and EL1.
+  2. The thread without a VCPU switches to a thread with a different VCPU to the first
+    2.1. All registers from `seL4_VCPUReg_TTBR0` to `seL4_VCPUReg_SPSR_EL1` are saved. This range includes
+         `seL4_VCPUReg_CPACR`, which overwrites the previously saved value and grants FPU access at EL0 and EL1.
+
 ### Upgrade Notes
 
 ---
diff --git a/include/arch/arm/armv/armv8-a/64/armv/vcpu.h b/include/arch/arm/armv/armv8-a/64/armv/vcpu.h
index 4bc8f0877..4a80e45da 100644
--- a/include/arch/arm/armv/armv8-a/64/armv/vcpu.h
+++ b/include/arch/arm/armv/armv8-a/64/armv/vcpu.h
@@ -630,8 +630,12 @@ static inline void armv_vcpu_boot_init(void)
 #endif
 }
 
-static inline void armv_vcpu_save(vcpu_t *vcpu, UNUSED bool_t active)
+static inline void armv_vcpu_save(vcpu_t *vcpu, bool_t active)
 {
+    /* If we aren't active then this state already got stored when we were disabled */
+    if (active) {
+        vcpu_save_reg(vcpu, seL4_VCPUReg_CPACR);
+    }
     vcpu_save_reg_range(vcpu, seL4_VCPUReg_TTBR0, seL4_VCPUReg_SPSR_EL1);
 
 #ifdef ARM_HYP_CP14_SAVE_AND_RESTORE_VCPU_THREADS
diff --git a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
index 607d43327..64a27294f 100644
--- a/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
+++ b/libsel4/sel4_arch_include/aarch64/sel4/sel4_arch/constants.h
@@ -72,18 +72,16 @@ typedef enum {
 } seL4_VCPUFault_Msg;
 
 typedef enum {
-    /* VM control registers EL1 */
+    /* System control registers EL1 */
     seL4_VCPUReg_SCTLR = 0,
+    seL4_VCPUReg_CPACR,
     seL4_VCPUReg_TTBR0,
     seL4_VCPUReg_TTBR1,
     seL4_VCPUReg_TCR,
     seL4_VCPUReg_MAIR,
     seL4_VCPUReg_AMAIR,
     seL4_VCPUReg_CIDR,
-
-    /* other system registers EL1 */
     seL4_VCPUReg_ACTLR,
-    seL4_VCPUReg_CPACR,
 
     /* exception handling registers EL1 */
     seL4_VCPUReg_AFSR0,