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
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 code@jimmah.com 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
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 code@jimmah.com 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
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 code@jimmah.com 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 code@jimmah.com 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
Main reason was lack of bits to pack into EP caps coupled with us not being able to think of good scenarios where we would need the distinction. Any additional flag eats into the number of badge bits, which is already lower than we’d like. Largely irrelevant on 64 bit platforms, but a trade-off on 32 bit platforms.
Cheers, Gerwin
On 12.07.2017, at 22:29, Gernot.Heiser@data61.csiro.au wrote:
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 code@jimmah.com 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 code@jimmah.com 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
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 code@jimmah.com 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 code@jimmah.com 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
-
Gernot.Heiser＠data61.csiro.au -
Gerwin.Klein＠data61.csiro.au -
Jimmy Brush -
Kevin.Elphinstone＠data61.csiro.au