Author:

Keywords:

Secure compilation, full abstraction, protected module architectures, formal methods, Science & Technology, Technology, Computer Science, Software Engineering, Computer Science, Secure Compilation, Object-Oriented Programming, Untyped Machine Code, Security, Fully abstract compilation, protected module architecture, FULLY ABSTRACT, SEMANTICS, 0803 Computer Software, 0806 Information Systems, Software Engineering, 4606 Distributed computing and systems software, 4612 Software engineering

Abstract:

A fully abstract compiler prevents security features of the source language from being bypassed by an at- tacker operating at the target language level. Unfortunately, developing fully abstract compilers is very complex, and it is even more so when the target language is an untyped assembly language. To provide a fully abstract compiler that targets untyped assembly, it has been suggested to extend the target language with a protected module architecture — an assembly-level isolation mechanism which can be found in next- generation processors. This paper provides a fully abstract compilation scheme whose source language is an object-oriented, high-level language and whose target language is such an extended assembly language. The source language enjoys features such as dynamic memory allocation and exceptions. Secure compilation of first-order method references, cross-package inheritance and inner classes is also presented. Moreover, this paper contains the formal proof of full abstraction of the compilation scheme. Measurements of the overhead introduced by the compilation scheme indicate that it is negligible.