A Least-Privilege Memory Protection Model for Modern Hardware

Daniel Schwyn; David Cock; Lukas Humbel; Nora Hossle; Reto Achermann; Timothy Roscoe

REVIEW 3 major objections 5 minor 40 references

A Least-Privilege Memory Protection Model for Modern Hardware

T0 review · 3 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper claims that memory management can be faithfully based on a least-privilege model of address translation as a configurable network of address spaces, and that such a model can be implemented without sacrificing performance.

desk verdict A credible systems contribution that turns decoding nets into a least-privilege memory model with a real Barrelfish implementation; the completeness claim is overbroad but the core is solid. read the letter →

arxiv 1908.08707 v1 pith:4VV4IJ7W submitted 2019-08-23 cs.OS

Reto Achermann , Nora Hossle , Lukas Humbel , Daniel Schwyn , David Cock , Timothy Roscoe This is my paper · ORCID

classification cs.OS

keywords least-privilegememoryprotectionaddresstranslationhardwarecapabilitysystemsIOMMUsecurityheterogeneousspacesdecodingnetmodeloperating

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to replace the traditional operating-system assumption of a single, homogeneous physical address space with a least-privilege model in which a machine is a configurable network of address spaces. It refines a graph-theoretic account of address translation so that both access to memory and the right to reprogram translation hardware become fine-grained authorities, captured in an access-control matrix and an executable specification. A full implementation in a capability-based research OS shows that the model can drive real hardware, including IOMMUs and a PCIe co-processor, and that its memory-operation performance matches or beats a mainstream monolithic kernel like Linux. The payoff is a way to build OS memory management that is faithful to modern heterogeneous hardware while still being fast enough for production use.

What carries the argument

The central object is the decoding net: a directed graph in which each node is an address space or device with an accept set of local addresses and a translate function sending them to addresses in other spaces. The paper extends this with dynamic configuration spaces, so the graph is not just a static snapshot but a set of allowable programmable states, and overlays an access-control matrix over two rights—grant and map. That matrix is the abstract specification of who may touch memory and who may reprogram translation hardware. On the implementation side, a partitioned capability system uses canonical object names, a mapping database ordered by containment, and typed page-table capabilities to make the model executable while keeping translation structures unmappable and unforgeable.

What would settle it

A concrete falsifier is to take any existing or simulated translation unit whose behavior depends on the history of accesses or on context beyond the current configuration, and show that it cannot be represented as a decoding-net node with an accept set, a translate function, and a configuration space; that would refute the completeness claim on which the paper's security argument rests.

Watch

Extended reading notes

Core claim

The paper's central claim is that the semantics of real modern address-translation hardware can be captured completely by a graph of address spaces, and that an operating system can enforce least privilege on top of that graph. It identifies two distinct authorities that conventional kernels conflate: the grant right to insert a memory object into some address space, and the map right to insert some object into a particular address space. Separating these rights and recording them in an access-control matrix lets a system grant a device driver enough authority to set up a shared buffer without letting it reconfigure translations it does not own. The paper demonstrates the whole chain—abstract model, executable Haskell specification, and a C implementation in a capability-based OS—and reports that the implementation is competitive with Linux on standard memory-operation benchmarks.

Load-bearing premise

The load-bearing premise is that every real address-translation unit—including unusual or stateful ones—can be expressed as a decoding-net node that accepts a set of local addresses, translates them through a function, and has a configuration space of allowed states; if any existing hardware fails to fit this form, the model's completeness and the safety of an OS built on it collapse.

Editorial extensions

If this is right

An OS built on the model can give device drivers precisely the authority they need—for example, mapping a buffer into an IOMMU without granting the right to reconfigure the IOMMU broadly.
Least-privilege memory management can be decentralized: user-space drivers and co-processors can set up shared memory through capability invocation rather than through a single trusted kernel.
Verified operating systems could substitute this richer hardware model for the simplifying single-address-space assumptions in their correctness proofs, covering systems with multiple translation units.
The performance results suggest that fine-grained capability-based memory management does not inherently cost more than conventional virtual memory in common operations such as map, protect, and unmap.
The implementation manages memory on simulated platforms with swapped, private, and private-plus-swapped address-space topologies, which mainstream OS designs do not currently support.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural extension the paper does not build is a conformance harness that runs the C implementation against the Haskell executable specification as an oracle, checking every mapping operation against the model.
The grant/map distinction could apply to other configuration resources beyond memory, such as virtualized network address translation or programmable device mappings; the paper does not generalize in that direction.
The Linux sketch suggests a weaker, ACL-based variant of the model could be retrofitted to monolithic kernels, but the paper does not implement or benchmark that variant.
Because the evaluation focuses on microbenchmarks, end-to-end application workloads might reveal different trade-offs; the paper's measured overheads are for specific operations, not full systems.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

What you should know: this paper takes the decoding-net model of address translation and extends it with dynamic configuration and separate grant/map rights, then builds an executable Haskell spec and a working Barrelfish implementation. The performance numbers are believable and the Xeon Phi evaluation is a good reality check. If you care about OS memory management on heterogeneous hardware, this is worth your time.

The genuinely new bits are the grant/map separation and the implementation. The grant/map distinction is a useful refinement for reasoning about least privilege: a process can grant access to a buffer without having the right to reconfigure the address space that maps it. The Haskell executable spec is a sensible intermediate step, and the paper is honest that correspondence between abstract, Haskell, and C is by inspection rather than machine-checked. That is a soft spot, but the authors do not oversell it.

The implementation is not a toy. They adapted real drivers for the Xeon Phi and IOMMU, implemented a capability system with typed objects and a mapping database, and booted on several simulated ARM topologies. The evaluation is solid: Appel-Li and map/protect/unmap benchmarks are competitive with Linux, and the overhead analysis is reasonable. No error bars, but the trends are clear.

Where are the real problems? First, the completeness claim—'capture the full semantics of real addressing hardware without simplifying assumptions'—is asserted, not proven. The stress-test worry about requester-dependent translation (e.g., IOMMU contexts selected by device ID) is worth raising, but I think it is largely addressable: the decoding-net graph already has one node per device or address space, so the requester identity is encoded in the source node. The paper does not explicitly formalize this, though, so the overbroad claim remains. If you push on it, the authors should either narrow the claim or extend the definition of translate to take the requester into account.

Second, the performance comparison is confounded: Barrelfish/MAS lacks Spectre/Meltdown mitigations, and Linux has them enabled in the main comparison. The authors mention this, but it means the speedups are not apples-to-apples. They also do not release code or data, which makes independent reproduction difficult.

These are not fatal for a systems paper. The model is a useful foundation, and the implementation shows it can work. I would send this to peer review. A serious referee should ask for a code release, a more careful completeness argument, and a less confounded evaluation, but the core contribution is sound. I would bring it to a reading group and would cite it in future work on capability-based memory management.

Referee Report

3 major / 5 minor

Summary. The paper argues that the traditional OS abstraction of a single, shared physical address space is inadequate for modern heterogeneous platforms, and proposes a least-privilege model of addressing based on decoding nets. It extends the decoding-net formalism with dynamic configuration and an access-control matrix distinguishing map rights (to insert objects into an address space) and grant rights (to insert an object into some address space). The model is refined into an executable Haskell specification and then implemented as Barrelfish/MAS, an extension of the Barrelfish capability system. The paper reports that Barrelfish/MAS achieves performance comparable to or better than Linux on memory-management microbenchmarks, successfully configures Xeon Phi and IOMMU address spaces, scales well in synthetic topology benchmarks, and boots on simulated ARM platforms with unusual address-space topologies. The paper frames the model as a sound basis for future formal verification, but explicitly states that no formally verified OS software is presented.

Significance. This is a substantial systems contribution with a concrete, implemented alternative to the single-address-space abstraction. The paper gives a clear mapping from access-control concepts to a capability system, demonstrates the model on real hardware including the Xeon Phi and IOMMUs, and provides detailed benchmark measurements. The open implementation and the explicit non-goals are strengths: the authors do not overclaim the existence of a formal proof, and they provide reproducible artifacts. If the completeness claim can be substantiated or suitably qualified, the model would be a useful design basis for future OS memory-management and verification work. The performance results are plausible and the comparison with Linux is carefully documented, including mitigated and unmitigated configurations.

major comments (3)

[§3, §4.2, §5.2] The central completeness claim that the model captures 'the full semantics of real addressing hardware without simplifying assumptions' (Section 1) is not supported by the formalism as presented. In Section 3, node.translate has type address -> {name}, and in Section 4.1, configuration is defined as address space -> node. This makes translation a pure function of the local address only. Real IOMMUs and System MMUs select translation contexts based on the requester or device context (for example PCIe ATS/PRI requester IDs, SMMU stream IDs, or PASID-based translation), so the resulting global name can depend on who issues the access. Such behavior cannot be expressed without extending node.translate with a requester argument or adding explicit requester-state to nodes. This is directly relevant to the stated goal of covering secure co-processors and devices (Sections 1 and 6.4). I recommend either extending the model with requester-dependent translation or explicitly restricting the completeness claim and stating the class of hardware the model is designed to cover.
[§3, §4.2, §5.2] The correspondence between the abstract access-control matrix, the Haskell executable specification, and the C implementation is asserted 'by inspection and careful construction' rather than demonstrated. Since the paper motivates the model as a basis for formal verification of system software, the absence of any refinement proof, or even a precise statement of the invariants relating the three levels, leaves a gap between the model and the implementation. This is acceptable for a systems paper if framed as a design artifact, but the current wording overstates the formal status of the artifact and of the 'sound foundation' claim in the conclusion.
[§6.4] The section titled 'Correctness on simulated platforms' demonstrates only that Barrelfish/MAS boots and can allocate and manage memory on four simulator topologies; no correctness property (for example, absence of unauthorized mappings, no dangling capabilities, or translation resolving as predicted) is checked. The results support functionality and flexibility, but they do not by themselves support the correctness of the model or its safety guarantees. The title and the corresponding claim in the conclusion should be softened accordingly.

minor comments (5)

[§5.2] The text contains several typos: 'has has support' should be 'has support', 'capablities' and 'capablity' should be 'capabilities' and 'capability', and 'cannonical' should be 'canonical'.
[§5.2.1] In the descendant definition, 'We say a capability B is a descendant of capability A if A is smaller than A' contains a typo; the condition should presumably read 'B is smaller than A' or 'B is contained in A'.
[§6.1] The performance comparison would be clearer if the effect of the missing Spectre/Meltdown mitigations in Barrelfish/MAS were discussed beyond noting the slowdown; the NS (no-mitigation) Linux numbers help, but the headline 'up to 4x faster' is stated relative to mitigated Linux without repeating this caveat in the figure caption.
[§3] The notation 'name = Name nodeid address' and 'node = Node accept ::{address} translate :: address->{name}' is typeset in a way that is hard to parse; explicit type signatures or a small example would improve readability.
[§6.5] The claim 'There is typically less than one capability for each frame of memory' is confusingly phrased; presumably the authors mean that on average there is fewer than one capability per frame, which should be stated as an average ratio rather than a typical count.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the model builds on independently machine-checked prior work and the central claims are empirical or explicitly assumed, not derived from their own conclusions.

full rationale

The paper's derivation chain starts from the decoding-net model of Achermann et al. [1,2]. Although these are self-citations, [2] is an Isabelle/HOL formalization of physical addressing, which counts as independent machine-checked support under the review rules; the present paper does not rely on an unverified uniqueness theorem or on a fitted parameter. The refinement to dynamic configuration and to grant/map rights is presented explicitly as an access-control matrix in the sense of Lampson [24], and the static/dynamic security condition is a definition of correctness rather than a prediction derived from the model. The completeness claim in Section 1 ('capture the full semantics of real addressing hardware without simplifying assumptions') is asserted rather than proven, and the paper candidly states that the correspondence between abstract and executable models is 'by inspection and careful construction' (Section 3); these are correctness risks, not circularities. The performance and scaling results are direct measurements on Linux and Barrelfish/MAS, so no fitted input is relabeled as a prediction. I therefore find no circular step requiring remediation.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The model depends on the decoding net formalism from the authors' prior work, the choice of access control matrix for security, and an unproven correspondence between abstract, executable, and C levels. No numeric parameters are fitted to data.

assumptions (3)

domain assumption The decoding net model of Achermann et al. (nodes accept/translate addresses) correctly and completely captures modern address translation hardware.
Adopted in Section 3 from the authors' prior work [1,2]; the paper argues completeness as a goal but does not prove coverage for all hardware.
domain assumption Security is equivalent to consistency of the current configuration with an access control matrix of grant and map rights.
Section 4.1 defines a system as secure if its configuration is consistent with the matrix; this is a modeling choice, not a proven theorem.
ad hoc to paper The Haskell executable specification corresponds to the abstract model, and the C implementation corresponds to the executable specification, by inspection and careful construction.
Section 3 states the correspondence is 'by inspection and careful construction'; no formal refinement proof is provided.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Least-Privilege Memory Protection Model for Modern Hardware." pith.science (2026). https://pith.science/paper/4VV4IJ7W

@misc{pith2026190808707,
  author       = {Pith},
  title        = {Pith review of: A Least-Privilege Memory Protection Model for Modern Hardware},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4VV4IJ7W}},
  note         = {Machine review of arXiv:1908.08707}
}

read the original abstract

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.

Figures

Figures reproduced from arXiv: 1908.08707 by the authors.

**Figure 2.** Address spaces in a system with two PCI devices [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗

**Figure 3.** Object Type Hierarchy and possible rights (green). [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗

Figures from the paper (4 more)

**Figure 4.** Figure 4: Mapping a RAM object Invariant I1 (Never Accessible) Subjects can never access unmappable objects Note that (in contrast to the seL4 executable specification), the details of the translation structures are kept opaque at this point—we merely record that they exist at c…

**Figure 5.** Figure 5: Appel-Li benchmark on Barrelfish/MAS and Linux with and without Spectre/Meltdown mitigation (NS). both enabled and disabled, using two microbenchmarks. Barrelfish/MAS has no mitigation measures. 6.1.1. The Appel and Li benchmark [6] tests operations relevant to garbag…

**Figure 6.** Figure 6: Comparison of memory operations on Barrelfish/MAS and Linux with and without Spectre/Meltdown mitigation (NS). Execution time per page in µs. Buffer sizes in powers of two from 4kB to 64GB. Linux MMAP Local Map RPC Map 0 100 200 300 400 500 600 700 800 900 1000 Time [u…

**Figure 7.** Figure 7: Profiling Configuration Time for a Xeon Phi Co [PITH_FULL_IMAGE:figures/full_fig_p010_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

40 extracted references · 40 canonical work pages

[1]

Formalizing Memory Accesses and Interrupts

Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Formalizing Memory Accesses and Interrupts. In Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017, pages 66–116, 2017

work page 2017
[2]

Physical Addressing on Real Hardware in Isabelle/HOL

Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Physical Addressing on Real Hardware in Isabelle/HOL. In Interactive Theorem Proving, ITP’18, pages 1–19, Oxford, United Kingdom, 2018. Springer International Publishing

work page 2018
[3]

Do- It-Yourself Virtual Memory Translation

Hanna Alam, Tianhao Zhang, Mattan Erez, and Yoav Etsion. Do- It-Yourself Virtual Memory Translation. In Proceedings of the 44th Annual International Symposium on Computer Architecture, ISCA ’17, pages 457–468, New York, NY , USA, 2017. ACM

work page 2017
[4]

Anderson

James P. Anderson. Computer Security Technology Planning Study. Technical Report ESD-TR-73-51, V ol. I, AD-758 206, Electronic Sys- tems Division, Deputy for Command and Management Systems HQ Electronic Systems Division (AFSC), L. G. Hanscom Field, Bedford, Massachusetts 01730, USA, October 1972

work page 1972
[5]

Sparsemem Memory Model

Andy Whitcroft. Sparsemem Memory Model. https://lwn.net/ Articles/134804/, Aug 2019

work page 2019
[6]

Appel and Kai Li

Andrew W. Appel and Kai Li. Virtual Memory Primitives for User Programs. In Proceedings of the Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS IV , pages 96–107, New York, NY , USA, 1991. ACM

work page 1991
[7]

Development Tools and Software: Fast Mod- els

ARM Ltd. Development Tools and Software: Fast Mod- els. https://www.arm.com/products/development-tools/ simulation/fast-models, August 2019. 11

work page 2019
[8]

Rossbach, and Onur Mutlu

Rachata Ausavarungnirun, Joshua Landgraf, Vance Miller, Saugata Ghose, Jayneel Gandhi, Christopher J. Rossbach, and Onur Mutlu. Mo- saic: A GPU Memory Manager with Application-transparent Support for Multiple Page Sizes. In Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO-50 ’17, pages 136–150, New York, NY , USA...

work page 2017

Show all 40 references

[9]

It’s Time to Think About an Operating System for Near Data Processing Architectures

Antonio Barbalace, Anthony Iliopoulos, Holm Rauchfuss, and Goetz Brasche. It’s Time to Think About an Operating System for Near Data Processing Architectures. In Proceedings of the 16th Workshop on Hot Topics in Operating Systems, HotOS ’17, pages 56–61, New York, NY , USA, 2017. ACM

2017
[10]

Popcorn: Bridging the Programmability Gap in heterogeneous-ISA Platforms

Antonio Barbalace, Marina Sadini, Saif Ansary, Christopher Jeles- nianski, Akshay Ravichandran, Cagil Kendir, Alastair Murray, and Binoy Ravindran. Popcorn: Bridging the Programmability Gap in heterogeneous-ISA Platforms. In Proceedings of the Tenth European Conference on Comp...

2015
[11]

The Multikernel: A New OS Architecture for Scalable Multicore Systems

Andrew Baumann, Paul Barham, Pierre-Evariste Dagand, Tim Harris, Rebecca Isaacs, Simon Peter, Timothy Roscoe, Adrian Schüpbach, and Akhilesh Singhania. The Multikernel: A New OS Architecture for Scalable Multicore Systems. In Proceedings of the ACM SIGOPS 22Nd Symposium on Ope...

2009
[12]

Secure Microkernels, State Monads and Scalable Reﬁnement

David Cock, Gerwin Klein, and Thomas Sewell. Secure Microkernels, State Monads and Scalable Reﬁnement. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’08, pages 167–182, Berlin, Heidelberg, 2008. Springer- Verlag

2008
[13]

Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock, and Manuel M. T. Chakravarty. Running the Manual: An Approach to High-assurance Microkernel Development. In Proceedings of the 2006 ACM SIGPLAN Workshop on Haskell, Haskell ’06, pages 60–71, New York, NY , USA, 2006. ACM

2006
[14]

Veriﬁed Protection Model of the seL4 Microkernel

Dhammika Elkaduwe, Gerwin Klein, and Kevin Elphinstone. Veriﬁed Protection Model of the seL4 Microkernel. In Proceedings of the 2Nd International Conference on Veriﬁed Software: Theories, Tools, Experiments, VSTTE ’08, pages 99–114, Berlin, Heidelberg, 2008. Springer-Verlag

2008
[15]

Authorization, Protection, and Allocation of Memory in a Large System

Simon Gerber. Authorization, Protection, and Allocation of Memory in a Large System. PhD thesis, ETH Zurich, 2018

2018
[16]

Not Your Parents’ Physical Address Space

Simon Gerber, Gerd Zellweger, Reto Achermann, Kornilios Kourtis, Timothy Roscoe, and Dejan Milojicic. Not Your Parents’ Physical Address Space. In Proceedings of the 15th USENIX Conference on Hot Topics in Operating Systems, HOTOS’15, pages 16–16, Berkeley, CA, USA, 2015. USEN...

2015
[17]

CertiKOS: An Extensible Archi- tecture for Building Certiﬁed Concurrent OS Kernels

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Wu, Jieung Kim, Vil- helm Sjöberg, and David Costanzo. CertiKOS: An Extensible Archi- tecture for Building Certiﬁed Concurrent OS Kernels. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OS...

2016
[18]

Multiple Physical Mappings: Dynamic DRAM Channel Sharing and Partitioning

Marius Hillenbrand, Mathias Gottschlag, Jens Kehne, and Frank Bel- losa. Multiple Physical Mappings: Dynamic DRAM Channel Sharing and Partitioning. In Proceedings of the 8th Asia-Paciﬁc Workshop on Systems, APSys ’17, pages 21:1–21:9, Mumbai, India, 2017

2017
[19]

HSA Runtime Programmer’s Reference Manual, version: 1.1.4 edition, Oct 2016

HSA Foundation. HSA Runtime Programmer’s Reference Manual, version: 1.1.4 edition, Oct 2016

2016
[20]

Qureshi, and Karsten Schwan

Jian Huang, Moinuddin K. Qureshi, and Karsten Schwan. An Evo- lutionary Study of Linux Memory Management for Fun and Proﬁt. In Proceedings of the 2016 USENIX Conference on Usenix Annual Technical Conference, USENIX ATC ’16, pages 465–478, Berkeley, CA, USA, 2016. USENIX Association

2016
[21]

Intel Xeon Phi Coprocessor System Software Devel- opers Guide, 2014

Intel Corporation. Intel Xeon Phi Coprocessor System Software Devel- opers Guide, 2014

2014
[22]

The OpenCL Speciﬁcation, version: 2.0, document revision: 29 edition, July 2015

Khronos OpenCL Working Group. The OpenCL Speciﬁcation, version: 2.0, document revision: 29 edition, July 2015

2015
[23]

seL4: Formal Veriﬁcation of an OS Kernel

Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal Veriﬁcation of an OS Kernel. In Proceedings of the ACM SIG...
[24]

Protection

Butler W Lampson. Protection. ACM SIGOPS Operating Systems Review, 8(1):18–24, 1974

1974
[25]

V AST: The Illusion of a Large Memory Space for GPUs

Janghaeng Lee, Mehrzad Samadi, and Scott Mahlke. V AST: The Illusion of a Large Memory Space for GPUs. InProceedings of the 23rd International Conference on Parallel Architectures and Compilation, PACT ’14, pages 443–454, New York, NY , USA, 2014. ACM

2014
[26]

Henry M. Levy. Capability-Based Computer Systems. Butterworth- Heinemann, Newton, MA, USA, 1984

1984
[27]

Thunderclap: Exploring Vulnerabilities in Operating System IOMMU Protection via DMA from Untrustworthy Peripherals

A Theodore Markettos, Colin Rothwell, Brett F Gutstein, Allison Pearce, Peter G Neumann, Simon W Moore, and Robert NM Watson. Thunderclap: Exploring Vulnerabilities in Operating System IOMMU Protection via DMA from Untrustworthy Peripherals. In NDSS, 2019

2019
[28]

True IOMMU Pro- tection from DMA Attacks: When Copy is Faster Than Zero Copy

Alex Markuze, Adam Morrison, and Dan Tsafrir. True IOMMU Pro- tection from DMA Attacks: When Copy is Faster Than Zero Copy. In Proceedings of the Twenty-First International Conference on Archi- tectural Support for Programming Languages and Operating Systems, ASPLOS ’16, pages...

2016
[29]

Bypassing IOMMU Protection against I/O Attacks

Benot Morgan, Eric Alata, Vincent Nicomette, and Mohamed Kaaniche. Bypassing IOMMU Protection against I/O Attacks. In 2016 Seventh Latin-American Symposium on Dependable Computing (LADC), pages 145–150, Oct 2016

2016
[30]

IOMMU Protection Against I/O Attacks: A Vulnerability and a Proof of Concept

Benot Morgan, Eric Alata, Vincent Nicomette, and Mohamed Kaaniche. IOMMU Protection Against I/O Attacks: A Vulnerability and a Proof of Concept. Journal of the Brazilian Computer Society, 24(1):2, Jan 2018

2018
[31]

NVIDIA Parker Series SoC Technical Reference Manual, v.1.0p edition, June 2017

NVIDIA. NVIDIA Parker Series SoC Technical Reference Manual, v.1.0p edition, June 2017

2017
[32]

Uniﬁed Memory in CUDA 6, Nov 2013

NVIDIA Corporation . Uniﬁed Memory in CUDA 6, Nov 2013. https: //devblogs.nvidia.com/unified-memory-in-cuda-6/

2013
[33]

i.MX 8DualXPlus/8QuadXPlus Applications Processor Ref- erence Manual, January 2019

NXP. i.MX 8DualXPlus/8QuadXPlus Applications Processor Ref- erence Manual, January 2019. REV 1, www.nxp.com/docs/en/ user-guide/IMX8QXPMEKHUG.pdf

2019
[34]

A Case for Intelligent RAM

David Patterson, Thomas Anderson, Neal Cardwell, Richard Fromm, Kimberly Keeton, Christoforos Kozyrakis, Randi Thomas, and Kather- ine Yelick. A Case for Intelligent RAM. IEEE Micro, 17(2):34–44, March 1997

1997
[35]

CBufs: Efﬁcient, System-wide Memory Management and Sharing

Yuxin Ren, Gabriel Parmer, Teo Georgiev, and Gedare Bloom. CBufs: Efﬁcient, System-wide Memory Management and Sharing. In Proceed- ings of the 2016 ACM SIGPLAN International Symposium on Memory Management, ISMM 2016, pages 68–77, New York, NY , USA, 2016. ACM

2016
[36]

Romanescu, Alvin R

Bogdan F. Romanescu, Alvin R. Lebeck, and Daniel J. Sorin. Speci- fying and Dynamically Verifying Address Translation-aware Memory Consistency. In Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, ASPLOS XV...

2010
[37]

A Declarative Language Approach to Device Conﬁguration

Adrian Schüpbach, Andrew Baumann, Timothy Roscoe, and Simon Peter. A Declarative Language Approach to Device Conﬁguration. In Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XVI, pages 119–1...

2011
[38]

seL4 Enforces Integrity

Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, and Gerwin Klein. seL4 Enforces Integrity. In Markovan Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving, pages 325–340, Berlin, Heidelberg, 2011. Springer ...

2011
[39]

OMAP44xx Multimedia Device Technical Ref- erence Manual, April 2014

Texas Instruments. OMAP44xx Multimedia Device Technical Ref- erence Manual, April 2014. Version AB, www.ti.com/lit/ug/ swpu235ab/swpu235ab.pdf

2014
[40]

Mind the Gap

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, and Michael Norrish. Mind the Gap. In Proceedings of the 22Nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs ’09, pages 500–515, Berlin, Heidelberg, 2009. Springer-Verlag. 12

2009

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.

[1] [1]

Formalizing Memory Accesses and Interrupts

Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Formalizing Memory Accesses and Interrupts. In Proceedings of the 2nd Workshop on Models for Formal Analysis of Real Systems, MARS 2017, pages 66–116, 2017

work page 2017

[2] [2]

Physical Addressing on Real Hardware in Isabelle/HOL

Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Physical Addressing on Real Hardware in Isabelle/HOL. In Interactive Theorem Proving, ITP’18, pages 1–19, Oxford, United Kingdom, 2018. Springer International Publishing

work page 2018

[3] [3]

Do- It-Yourself Virtual Memory Translation

Hanna Alam, Tianhao Zhang, Mattan Erez, and Yoav Etsion. Do- It-Yourself Virtual Memory Translation. In Proceedings of the 44th Annual International Symposium on Computer Architecture, ISCA ’17, pages 457–468, New York, NY , USA, 2017. ACM

work page 2017

[4] [4]

Anderson

James P. Anderson. Computer Security Technology Planning Study. Technical Report ESD-TR-73-51, V ol. I, AD-758 206, Electronic Sys- tems Division, Deputy for Command and Management Systems HQ Electronic Systems Division (AFSC), L. G. Hanscom Field, Bedford, Massachusetts 01730, USA, October 1972

work page 1972

[5] [5]

Sparsemem Memory Model

Andy Whitcroft. Sparsemem Memory Model. https://lwn.net/ Articles/134804/, Aug 2019

work page 2019

[6] [6]

Appel and Kai Li

Andrew W. Appel and Kai Li. Virtual Memory Primitives for User Programs. In Proceedings of the Fourth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS IV , pages 96–107, New York, NY , USA, 1991. ACM

work page 1991

[7] [7]

Development Tools and Software: Fast Mod- els

ARM Ltd. Development Tools and Software: Fast Mod- els. https://www.arm.com/products/development-tools/ simulation/fast-models, August 2019. 11

work page 2019

[8] [8]

Rossbach, and Onur Mutlu

Rachata Ausavarungnirun, Joshua Landgraf, Vance Miller, Saugata Ghose, Jayneel Gandhi, Christopher J. Rossbach, and Onur Mutlu. Mo- saic: A GPU Memory Manager with Application-transparent Support for Multiple Page Sizes. In Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO-50 ’17, pages 136–150, New York, NY , USA...

work page 2017