@TechReport{ it:2015-028, author = {Adriaan Larmuseau and Marco Patrignani and Dave Clarke}, title = {A Secure Compiler for {ML} Modules - Extended Version}, institution = {Department of Information Technology, Uppsala University}, department = {Computing Science Division}, year = {2015}, number = {2015-028}, month = sep, note = {This technical report is an updated version of TR 2015-017 that serves as the companion report to an APLAS 2015 paper of the same title.}, abstract = {Many functional programming languages compile to low-level languages such as C or assembly. Most security properties of those compilers, however, apply only when the compiler compiles whole programs. This paper presents a compilation scheme that securely compiles a standalone module of ModuleML, a light-weight version of an ML with modules, into untyped assembly. The compilation scheme is secure in that it reflects the abstractions of a ModuleML module, for every possible piece of assembly code that it interacts with. This is achieved by isolating the compiled module through a low-level memory isolation mechanism and by dynamically type checking the low-level interactions. We evaluate an implementation of the compiler on relevant test scenarios.} }