Implementing a Secure Abstract Machine - Extended Version

Adriaan Larmuseau, Marco Patrignani, and Dave Clarke

November 2015

Abstract:

Abstract machines are both theoretical models used to study language properties and practical models of language implementations. As with all language implementations, abstract machines are subject to security violations by the context in which they reside. This paper presents the implementation of an abstract machine for ML that preserves the abstractions of the language it implements, in possibly malicious, low-level contexts. To guarantee this security result, we make use of a low-level memory isolation mechanism and derive the formalisation of the machine through a methodology, whose every step is accompanied by formal properties that ensure that the step has been carried out properly. We provide an implementation of the abstract machine and analyse its performance for relevant scenarios.

Note: This technical report serves as the companion report to a SEC@SAC 2016 paper of the same name.

Available as PDF (641 kB, no cover)

Download BibTeX entry.