Title: Secure compilation to modern processors: extended version
Authors: Agten, Pieter
Strackx, Raoul
Jacobs, Bart
Piessens, Frank
Issue Date: Apr-2012
Publisher: Department of Computer Science, KU Leuven
Series Title: CW Reports vol:CW619
Abstract: We present a secure (fully abstract) compilation scheme to compile a high-level language to low-level machine code. Full abstraction is achieved by relying on the virtualization support provided by modern processors: a small hypervisor efficiently implements fine-grained memory access control, and this gives the low-level language sufficient protection features to serve as a target for the fully abstract compilation of a simple Java-like language.

We formalize high-level and low-level languages and prove full abstraction for our compilation algorithm. We also show by means of an implementation that our low-level language with fine-grained memory access-control can be realized efficiently on modern commodity platforms.

This report is an extended version of the paper published at Computer Security Foundations Symposium 2012. It extends the conference version with technical details about the formalization and the proofs.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW619.pdfDocument Published 703KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.