On Modular and Fully-Abstract Compilation -- Technical Appendix

TL;DR

This paper explores how to design modular, fully-abstract secure compilers that maintain security when independently compiled components are linked together, addressing security threats arising from linking.

Contribution

It introduces a new compiler from an object-based language to untyped assembly with memory isolation, proving it is both fully-abstract and modular.

Findings

The compiler preserves security properties upon linking.

Identification of security threats due to linking.

Proof sketch demonstrating full abstraction and modularity.

Abstract

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.