@TechReport{	  it:2015-026,
  author	= {Adriaan Larmuseau and Dave Clarke},
  title		= {Modelling an Assembly Attacker by Reflection},
  institution	= {Department of Information Technology, Uppsala University},
  department	= {Computing Science Division},
  year		= {2015},
  number	= {2015-026},
  month		= aug,
  note		= {This technical report is an extended version of a paper
		  titled: \emph{A High-Level Model for an Assembly Language
		  Attacker by means of Reflection} that is to appear at SETTA
		  2015.},
  abstract	= {Many high-level functional programming languages are
		  compiled to or interoperate with, low-level languages such
		  as C and assembly. Research into the security of these
		  compilation and interoperation mechanisms often makes use
		  of high-level attacker models to simplify formalisations.
		  In practice, however, the validity of such high-level
		  attacker models is frequently called into question. In this
		  technical report we formally prove that a light-weight
		  ML-like including references, equipped with a reflection
		  operator can serve as an accurate model for malicious
		  assembly language programs, when reasoning about the
		  security threats posed to the abstractions of high-level
		  functional programs that reside within a protected memory
		  space. The proof proceeds by relating a bisimulation over
		  the inputs and observations of the assembly language
		  attacker to a bisimulation over the inputs and observations
		  of the high-level attacker.}
}