  Secure compilation studies compilers that generate target-level components
that are as secure as their source-level counterparts. Full abstraction is the
most widely-proven property when defining a secure compiler. A compiler is
modular if it allows different components to be compiled independently and then
to be linked together to form a whole program. Unfortunately, many existing
fully-abstract compilers to untyped machine code are not modular. So, while
fully-abstractly compiled components are secure from malicious attackers, if
they are linked against each other the resulting component may become
vulnerable to attacks. This paper studies how to devise modular, fully-abstract
compilers. It first analyses the attacks arising when compiled programs are
linked together, identifying security threats that are due to linking. Then, it
defines a compiler from an object-based language with method calls and dynamic
memory allocation to untyped assembly language extended with a memory isolation
mechanism. The paper provides a proof sketch that the defined compiler is
fully-abstract and modular, so its output can be linked together without
introducing security violations.
