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.template.c#L73-L103
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.elphinst...@nicta.com.au
<mailto:kevin.elphinst...@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
