Yes, it could be a separate right. EROS, from memory, had a “weak receive” right, which would diminish all caps received by the channel, without requiring send rights to receive undiminished caps. Arguably a cleaner solution. I don’t remember the discussion that lead to the present model. Gernot

On 12 Jul 2017, at 22:00, Jimmy Brush wrote:

That does make sense; however, it still seems surprising to me that the feature isn't its own flag (by perhaps additionally removing the Grant permission on the receiving endpoint cap).

It seems like there might be cases where you want to delegate authority to receive, but not send, against an endpoint, without the intention of setting up confinement. But, I don't have a specific scenario in mind, just thinking through things.

On 07/12/2017 05:22 AM, Gernot.Heiser@data61.csiro.au wrote:

...

Yes, and this makes sense if you think about it.

If you want to guarantee that Alice is confined (i.e. cannot leak information sent to her) then you need to ensure that she has no send rights. Which you cannot if she was able to receive a cap with send rights.

Gernot

...

On 11 Jul 2017, at 19:34, Jimmy Brush wrote:

Hello,

in the 6.0 manual section 3.1.4 the table shows that Write permission on an endpoint cap permits sending to the endpoint.

however, in section 4.2.2 it says without the Write permission on the RECEIVING endpoint cap, any cap sent over IPC gets diminished.

Am I missing something? It seems the Write permission is overloaded to mean two different things.

This would seem to imply that to receive an undiminished capability via IPC you must have both send and receive permission to the endpoint you are receiving against.

Which would mean if you wanted to limit someone to only receiving and never sending against an endpoint by giving them an endpoint cap with only Read permission, they would necessarily also NEVER be able to receive an undiminished capability.

Thanks, JB

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

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

The current model is a simplification of the EROS model for mostly practical reasons. It was based on a combination of need for the use cases at the time, and cost/complexity of verification. There is no fundamental reason it could not be extended to be more expressive to capture other scenarios (we had a non-verified diminish at one point IIRC). It would mean revisiting the cost/complexity of re-establishing verification again. - Kevin -----Original Message----- From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Gernot.Heiser@data61.csiro.au Sent: Wednesday, 12 July 2017 10:30 PM To: devel@sel4.systems Subject: Re: [seL4] Question on endpoint cap write permission Yes, it could be a separate right. EROS, from memory, had a “weak receive” right, which would diminish all caps received by the channel, without requiring send rights to receive undiminished caps. Arguably a cleaner solution. I don’t remember the discussion that lead to the present model. Gernot

On 12 Jul 2017, at 22:00, Jimmy Brush wrote:

That does make sense; however, it still seems surprising to me that the feature isn't its own flag (by perhaps additionally removing the Grant permission on the receiving endpoint cap).

It seems like there might be cases where you want to delegate authority to receive, but not send, against an endpoint, without the intention of setting up confinement. But, I don't have a specific scenario in mind, just thinking through things.

On 07/12/2017 05:22 AM, Gernot.Heiser@data61.csiro.au wrote:

...

Yes, and this makes sense if you think about it.

If you want to guarantee that Alice is confined (i.e. cannot leak information sent to her) then you need to ensure that she has no send rights. Which you cannot if she was able to receive a cap with send rights.

Gernot

...

On 11 Jul 2017, at 19:34, Jimmy Brush wrote:

Hello,

in the 6.0 manual section 3.1.4 the table shows that Write permission on an endpoint cap permits sending to the endpoint.

however, in section 4.2.2 it says without the Write permission on the RECEIVING endpoint cap, any cap sent over IPC gets diminished.

Am I missing something? It seems the Write permission is overloaded to mean two different things.

This would seem to imply that to receive an undiminished capability via IPC you must have both send and receive permission to the endpoint you are receiving against.

Which would mean if you wanted to limit someone to only receiving and never sending against an endpoint by giving them an endpoint cap with only Read permission, they would necessarily also NEVER be able to receive an undiminished capability.

Thanks, JB

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

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

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