Over the past decade, great progress has been made in the static modular verification of C code by means of separation logic-based program logics. However, the runtime guarantees offered by such verification are relatively limited when the verified modules are part of a whole program that also contains unverified modules. In particular, a memory safety error in an unverified module can corrupt the runtime state, leading to assertion failures or invalid memory accesses in the verified modules. This paper develops runtime checks to be inserted at the boundary between the verified and the unverified part of a program, to guarantee that no assertion failures or invalid memory accesses can occur at runtime in any verified module. One of the key challenges is enforcing the separation logic frame rule, which we achieve by checking the integrity of the footprint of the verified part of the program on each control flow transition from the unverified to the verified part. This in turn requires the presence of some support for module-private memory at runtime. We formalize our approach and prove soundness. We implement the necessary runtime checks by means of a program transformation that translates C code with separation logic annotations into plain C, and that relies on a protected module architecture for providing module-private memory and restricted module entry points. Benchmarks show the performance impact of this transformation depends on the choice of boundary between the verified and unverified parts of the program, but is below 4% for real-world applications.

A fully abstract compiler prevents security features of the source language from being bypassed by an attacker 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 article 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 article 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.

The inclusion of third-party scripts in web pages is a common practice. A recent study has shown that more than half of the Alexa top 10000 sites include scripts from more than 5 different origins. However, such script inclusions carry risks, as the included scripts operate with the privileges of the including website.

We present a secure (fully abstract) compilation scheme to compile an object-based high-level language to low-level machine code. Full abstraction is achieved by relying on a fine-grained program counter-based memory access protection scheme, which is part of our low-level target language. We discuss why standard compilers fail to provide full abstraction and introduce enhancements needed to achieve this goal. We prove that our enhanced compilation scheme provides full abstraction from our high-level source language to our low-level target language. Lastly, we show by means of a prototype implementation that our low-level language with fine-grained memory access control can be realized efficiently on modern commodity platforms.