SCIENCE@home

On Modular and Fully-Abstract Compilation - Technical Appendix

Marco Patrignani,Dominique Devriese,F. Piessens

Published 2016 in arXiv.org

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.

PUBLICATION RECORD

  • Publication year

    2016

  • Venue

    arXiv.org

  • Publication date

    2016-04-01

  • Fields of study

    Computer Science

  • Identifiers
    arXiv 1604.05044
  • External record

    Open on Semantic Scholar

  • Source metadata

    Semantic Scholar

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-42 of 42 references · Page 1 of 1

CITED BY