A sealed capability in CHERI is both immutable and un-dereferenceable. While sealed capabilities are generally used for compartment switching, in this talk we consider the consequences of permitting application code to perform more general capability sealing. This might be useful for secure exchange of data between untrusted code components; we will present illustrative scenarios.

This presentation considers the interaction between sealed capabilities and memory allocators. We examine both explicit malloc style allocators and automated garbage collection regimes. We show that memory allocators must be aware of sealed capabilities and should be able to trace reference graphs through sealed capabilities, otherwise runtime memory errors occur (e.g. space leaks or dangling pointers). We propose an augmented allocator API to track capability seal operations, and sketch a prototypical implementation.

Reader in Programming Language Implementation at the School Computing Science, University of Glasgow. In Scotland since 2010.