On modular and fully-abstract compilation

M Patrignani, D Devriese… - 2016 IEEE 29th Computer …, 2016 - ieeexplore.ieee.org
2016 IEEE 29th Computer Security Foundations Symposium (CSF), 2016ieeexplore.ieee.org
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 …
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.
ieeexplore.ieee.org
Showing the best result for this search. See all results