A high-level model for an assembly language attacker by means of reflection
2015 (English)In: Dependable Software Engineering: Theories, Tools, and Applications, Springer, 2015, 168-182 p.Conference paper (Refereed)
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 paper we formally prove that a light-weight ML equipped with a reflection operator can serve as an accurate model for malicious assembly language programs, when reasoning about the security threats such an attacker model poses to the abstractions of ML programs that reside within a protected memory space. The proof proceeds by relating bisimulations over the assembly language attacker and the high-level attacker.
Place, publisher, year, edition, pages
Springer, 2015. 168-182 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9409
IdentifiersURN: urn:nbn:se:uu:diva-267094DOI: 10.1007/978-3-319-25942-0_11ISI: 000374099200011ISBN: 9783319259413OAI: oai:DiVA.org:uu-267094DiVA: diva2:872013
SETTA 2015, November 4–6, Nanjing, China