  We present a new least-privilege-based model of addressing on which to base
memory management functionality in an OS for modern computers like phones or
server-based accelerators. Existing software assumptions do not account for
heterogeneous cores with different views of the address space, leading to the
related problems of numerous security bugs in memory management code (for
example programming IOMMUs), and an inability of mainstream OSes to securely
manage the complete set of hardware resources on, say, a phone System-on-Chip.
  Our new work is based on a recent formal model of address translation
hardware which views the machine as a configurable network of address spaces.
We refine this to capture existing address translation hardware from modern
SoCs and accelerators at a sufficiently fine granularity to model minimal
rights both to access memory and configure translation hardware. We then build
an executable specification in Haskell, which expresses the model and metadata
structures in terms of partitioned capabilities. Finally, we show a fully
functional implementation of the model in C created by extending the capability
system of the Barrelfish research OS.
  Our evaluation shows that our unoptimized implementation has comparable (and
in some cases) better performance than the Linux virtual memory system, despite
both capturing all the functionality of modern hardware addressing and enabling
least-privilege, decentralized authority to access physical memory and devices.
