Re: The Ravenscar profile and capabilities paradigm

[Richard Iswara <haujekchifan@gmail.com>]

On 12/10/2021 02.50, Doctor Who wrote:
> On Mon, 11 Oct 2021 20:36:46 +0100, "Luke A. Guest"
> <laguest@archeia.com> wrote:
> 
>> On 11/10/2021 20:25, Doctor Who wrote:
>>> On Mon, 11 Oct 2021 15:48:37 +0100, "Luke A. Guest"
>>> <laguest@archeia.com> wrote:
>>>
>>>> On 11/10/2021 14:33, Doctor Who wrote:
>>>>> Hello,
>>>>> someone knows how to introduce the capabilities paradigm in Ada,
>>>>> specifically for programs written using the Ravenscar profile ?
>>>>>
>>>>>
>>>>
>>>> Capabilities are just a set of operations that an object / user can
>>>> perform, or not. So, it's merely a bitset. A bitset which can form
>>>> derived bitsets.
>>>>
>>>
>>> no it is another thing,
>>> https://en.wikipedia.org/wiki/Capability-based_security
>>>
>>
>> I know what it is. It is still a set of bits, or, permissions, or
>> capabilities. The capabilities are usually provided by the OS services.
>>
>> But as you didn't specify whether you wanted to map onto an existing OS'
>> capabilities or if you wanted to implement your own, I went with the latter.
> 
> there isn't any existing OS that provides capability-security from the
> ground up, I intend to implement my own.
> 
seL4? The whitepaper includes the proofs also.