Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties

DOI10.1007/978-3-319-03545-1_18zbMath1426.68286OpenAlexW2105482908MaRDI QIDQ2938055

Narges Khakpour, Mads Dam, Oliver Schwarz

Publication date: 13 January 2015

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-136354

zbMATH Keywords

theorem provingnoninterferenceARM instruction setkernel securityuser mode execution

Mathematics Subject Classification ID

Mathematical problems of computer architecture (68M07) Formalization of mathematics in connection with theorem provers (68V20) Computer security (68M25)

Related Items (2)

System-level non-interference of constant-time cryptography. I: Model ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model

Uses Software

• HOL
• seL4
• ARMor

This page was built for publication: Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties