Machine assisted proof of ARMv7 instruction level isolation properties. (English) Zbl 1426.68286
Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8307, 276-291 (2013).
Summary: In this paper, we formally verify security properties of the ARMv7 instruction set architecture (ISA) for user mode executions. To obtain guarantees that arbitrary (and unknown) user processes are able to run isolated from privileged software and other user processes, instruction level noninterference and integrity properties are provided, along with proofs that transitions to privileged modes can only occur in a controlled manner. This work establishes a main requirement for operating system and hypervisor verification, as demonstrated for the PROSPER separation kernel. The proof is performed in the HOL4 theorem prover, taking the Cambridge model of ARM as basis. To this end, a proof tool has been developed, which assists the verification of relational state predicates semi-automatically.
For the entire collection see [Zbl 1298.68028].
For the entire collection see [Zbl 1298.68028].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 68M07 | Mathematical problems of computer architecture |
| 68M25 | Computer security |
