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:[email protected]] On Behalf Of
[email protected]
Sent: Wednesday, 12 July 2017 10:30 PM
To: [email protected]
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 <[email protected]> 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, [email protected] 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 <[email protected]> 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
>>> [email protected]
>>> https://sel4.systems/lists/listinfo/devel
>>
>> _______________________________________________
>> Devel mailing list
>> [email protected]
>> https://sel4.systems/lists/listinfo/devel
>>
>
>
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
