@TechReport{	  it:2015-017,
  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-017},
  month		= jun,
  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.}
}