A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor

Title:	A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
Authors:	Zhe Hou (zhe /dot/ hou /at/ ntu /dot/ edu /dot/ sg), David Sanan (sanan /at/ ntu /dot/ edu /dot/ sg), Alwen Tiu (ATiu /at/ ntu /dot/ edu /dot/ sg) and Yang Liu (yangliu /at/ ntu /dot/ edu /dot/ sg)
Submission date:	2016-10-19
Abstract:	We formalise the SPARCv8 instruction set architecture (ISA) which is used in processors such as LEON3. Our formalisation can be specialised to any SPARCv8 CPU, here we use LEON3 as a running example. Our model covers the operational semantics for all the instructions in the integer unit of the SPARCv8 architecture and it supports Isabelle code export, which effectively turns the Isabelle model into a SPARCv8 CPU simulator. We prove the language-based non-interference property for the LEON3 processor. Our model is based on deterministic monad, which is a modified version of the non-deterministic monad from NICTA/l4v.
BibTeX:	@article{SPARCv8-AFP, author = {Zhe Hou and David Sanan and Alwen Tiu and Yang Liu}, title = {A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor}, journal = {Archive of Formal Proofs}, month = oct, year = 2016, note = {\url{http://isa-afp.org/entries/SPARCv8.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.