Machine assisted proof of ARMv7 instruction level isolation properties

DOI10.1007/978-3-319-03545-1_18MaRDI QIDQ2938055zbMATH OpenOpenAlexFDO

Authors Narges Khakpour, Oliver Schwarz, Mads Dam

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

ARM instruction setkernel securitynoninterferencetheorem provinguser mode execution

Mathematics Subject Classification ID

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

Recommendations

• A trustworthy monadic formalization of the ARMv7 instruction set architecture
• Hoare Logic for ARM Machine Code
• seL4 enforces integrity
• Formalizing SPARCv8 instruction set architecture in Coq
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code

Cited in

(7)

• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• System-level non-interference of constant-time cryptography. I: Model
• Formally verified implementation of an idealized model of virtualization
• AUSPICE-R: automatic safety-property proofs for realistic features in machine code
• Hoare Logic for ARM Machine Code
• Formalizing SPARCv8 instruction set architecture in Coq
• A trustworthy monadic formalization of the ARMv7 instruction set architecture

Describes a project that uses

Uses Software

• HOL
• seL4
• ARMor

This page was built for publication: Machine assisted proof of ARMv7 instruction level isolation properties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2938055)