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.
Note: This technical report is an extended version of a paper titled: A High-Level Model for an Assembly Language Attacker by means of Reflection that is to appear at SETTA 2015.
Available as PDF (555 kB, no cover)
Download BibTeX entry.