Prove that user execution cannot alter any of: - banked registers for FIQ and IRQ modes - banked SP registers for modes other than monitor and user mode Then, use that lemma where needed in the enclave entry/return path, rather than needlessly saving and restoring the register values.
Prove that user execution cannot alter any of:
Then, use that lemma where needed in the enclave entry/return path, rather than needlessly saving and restoring the register values.