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.fernan...@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.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 >
_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
