A secure compiler for ML modules
2015 (English)In: Programming Languages and Systems: APLAS 2015, Springer, 2015, 29-48 p.Conference paper (Refereed)
Many functional programming languages compile to low-level languages such as C or assembly. Numerous 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 its interactions. We evaluate an implementation of the compiler on relevant test scenarios.
Place, publisher, year, edition, pages
Springer, 2015. 29-48 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 9458
IdentifiersURN: urn:nbn:se:uu:diva-268750DOI: 10.1007/978-3-319-26529-2_3ISI: 000376504900006ISBN: 9783319265285ISBN: 9783319265292OAI: oai:DiVA.org:uu-268750DiVA: diva2:881075
APLAS 2015, November 30 – December 2, Pohang, South Korea