VSpace translation?

Ben Karel

13 Dec 2015 13 Dec '15

5:23 p.m.

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

Attachments:

attachment.html (text/html — 251 bytes)

Show replies by date

Kevin Elphinstone

13 Dec 13 Dec

8:54 p.m.

The original design of the kernel was that whatever user-level service established the mappings (e.g. the root task) could provide the translation info to whomever needs it. Depending on the design of the system built on seL4, it could be as simple as base limit info in the case of static systems, in an ideal case. A mapping table in the case of fragmented allocation. Obtaining the mapping info via system calls has the disadvantage of kernel entry and exit (overhead), though you could populate a mapping table with each call. Also note that system calls are not necessarily accurate either in the case of dynamic systems, unless the mappee has some kind of contract with the mapper to not change the mapping, e.g. a pinning API or similar. If you have a pinning API, you can get the current translation info with the pin RPC. The current frame translate method was a originally a work around an immature user-level that has made it “out in the wild”, so to speak. We have not thought hard about security implications of translate on a page directory, as AFAIK, we had no motivation for an additional translate on top of an existing translate, on top of what could be done at user-level with some book keeping (and complexity). - Kevin From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Ben Karel Sent: Sunday, 13 December 2015 5:23 PM To: devel@sel4.systems Subject: [seL4] VSpace translation? Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)? ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Gerwin Klein

14 Dec 14 Dec

9:54 a.m.

Purely from the proof side, I don’t think it would violate any of the current high-level properties (integrity, inflow, availability, functional correctness). If implemented correctly, of course. Cheers, Gerwin On 13 Dec 2015, at 20:54, Kevin Elphinstone mailto:Kevin.Elphinstone@nicta.com.au> wrote: The original design of the kernel was that whatever user-level service established the mappings (e.g. the root task) could provide the translation info to whomever needs it. Depending on the design of the system built on seL4, it could be as simple as base limit info in the case of static systems, in an ideal case. A mapping table in the case of fragmented allocation. Obtaining the mapping info via system calls has the disadvantage of kernel entry and exit (overhead), though you could populate a mapping table with each call. Also note that system calls are not necessarily accurate either in the case of dynamic systems, unless the mappee has some kind of contract with the mapper to not change the mapping, e.g. a pinning API or similar. If you have a pinning API, you can get the current translation info with the pin RPC. The current frame translate method was a originally a work around an immature user-level that has made it “out in the wild”, so to speak. We have not thought hard about security implications of translate on a page directory, as AFAIK, we had no motivation for an additional translate on top of an existing translate, on top of what could be done at user-level with some book keeping (and complexity). - Kevin From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Ben Karel Sent: Sunday, 13 December 2015 5:23 PM To: devel@sel4.systemsmailto:devel@sel4.systems Subject: [seL4] VSpace translation? Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)? ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Matthew Fernandez

11:48 a.m.

To give some additional context to Kevin's comments, the CAmkES component platform already implements the kind of mapping cache Kevin describes for reversing the mappings of its DMA pool [0], though the template code may be slightly difficult to decipher. [0]: https://github.com/seL4/camkes-tool/blob/master/camkes/templates/component.t... On 14/12/15 09:54, Gerwin Klein wrote:

...

Purely from the proof side, I don’t think it would violate any of the current high-level properties (integrity, inflow, availability, functional correctness). If implemented correctly, of course.

Cheers, Gerwin

...
On 13 Dec 2015, at 20:54, Kevin Elphinstone mailto:Kevin.Elphinstone@nicta.com.au> wrote:

The original design of the kernel was that whatever user-level service established the mappings (e.g. the root task) could provide the translation info to whomever needs it. Depending on the design of the system built on seL4, it could be as simple as base limit info in the case of static systems, in an ideal case. A mapping table in the case of fragmented allocation.

Obtaining the mapping info via system calls has the disadvantage of kernel entry and exit (overhead), though you could populate a mapping table with each call.

Also note that system calls are not necessarily accurate either in the case of dynamic systems, unless the mappee has some kind of contract with the mapper to not change the mapping, e.g. a pinning API or similar. If you have a pinning API, you can get the current translation info with the pin RPC.

The current frame translate method was a originally a work around an immature user-level that has made it “out in the wild”, so to speak.

We have not thought hard about security implications of translate on a page directory, as AFAIK, we had no motivation for an additional translate on top of an existing translate, on top of what could be done at user-level with some book keeping (and complexity).

-Kevin

*From:*Devel [mailto:devel-bounces@sel4.systems]*On Behalf Of*Ben Karel *Sent:*Sunday, 13 December 2015 5:23 PM *To:*devel@sel4.systems mailto:devel@sel4.systems *Subject:*[seL4] VSpace translation?

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

----------------------------------------------------------------------------------------------------

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems mailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

Ben Karel

5:19 p.m.

Thanks for the feedback, all. It's an good point about having (or, rather, disseminating) consistent knowledge in the face of concurrent updates. Seems like a compelling argument for not exposing the translate API. On Sun, Dec 13, 2015 at 7:48 PM, Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:

...

To give some additional context to Kevin's comments, the CAmkES component platform already implements the kind of mapping cache Kevin describes for reversing the mappings of its DMA pool [0], though the template code may be slightly difficult to decipher.

[0]: https://github.com/seL4/camkes-tool/blob/master/camkes/templates/component.t...

On 14/12/15 09:54, Gerwin Klein wrote:

...
Purely from the proof side, I don’t think it would violate any of the current high-level properties (integrity, inflow, availability, functional correctness). If implemented correctly, of course.

Cheers, Gerwin

On 13 Dec 2015, at 20:54, Kevin Elphinstone <

...
Kevin.Elphinstone@nicta.com.au mailto:Kevin.Elphinstone@nicta.com.au> wrote:

The original design of the kernel was that whatever user-level service established the mappings (e.g. the root task) could provide the translation info to whomever needs it. Depending on the design of the system built on seL4, it could be as simple as base limit info in the case of static systems, in an ideal case. A mapping table in the case of fragmented allocation.

Obtaining the mapping info via system calls has the disadvantage of kernel entry and exit (overhead), though you could populate a mapping table with each call.

Also note that system calls are not necessarily accurate either in the case of dynamic systems, unless the mappee has some kind of contract with the mapper to not change the mapping, e.g. a pinning API or similar. If you have a pinning API, you can get the current translation info with the pin RPC.

The current frame translate method was a originally a work around an immature user-level that has made it “out in the wild”, so to speak.

We have not thought hard about security implications of translate on a page directory, as AFAIK, we had no motivation for an additional translate on top of an existing translate, on top of what could be done at user-level with some book keeping (and complexity).

-Kevin

*From:*Devel [mailto:devel-bounces@sel4.systems]*On Behalf Of*Ben Karel *Sent:*Sunday, 13 December 2015 5:23 PM *To:*devel@sel4.systems mailto:devel@sel4.systems *Subject:*[seL4] VSpace translation?

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

----------------------------------------------------------------------------------------------------

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems mailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

3293

Age (days ago)

3294

Last active (days ago)

List overview

Download

4 comments

4 participants

participants (4)

Ben Karel
Gerwin Klein
Kevin Elphinstone
Matthew Fernandez