26 Oct
2019
26 Oct
'19
8 a.m.
Hi,
I know that seL4 provides confidentiality, which is described as a property
that "means that data cannot be read without permission." Given this
wording, I wonder if it is not possible to revoke those permissions in
certain cases. In particular, I would like for one camkes component to be
able to perform runtime measurements, such as heap analysis, on another
component. Or even better, I would like for a component to be able to
perform runtime measurements on a program running within the camkes linux
vm. Is such a feat possible?
Best,
Michael Neises
26 Oct
26 Oct
2:07 p.m.
On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote:
Hi,
I know that seL4 provides confidentiality, which is described as a property that
"means that data cannot be read without permission." Given this wording, I
wonder if it is not possible to revoke those permissions in certain cases. In particular,
I would like for one camkes component to be able to perform runtime measurements, such as
heap analysis, on another component. Or even better, I would like for a component to be
able to perform runtime measurements on a program running within the camkes linux vm. Is
such a feat possible?
Hi Michael
seL4’s confidentiality (and other security) enforcement means that the kernel guarantees
that you can only access objects to which you have been given explicit permission (in the
form of a capability). How those permissions are allocated is a matter of policy, the
kernel doesn’t care, it only enforces.
In particular, it is totally possible in seL4 to give one component access to another
component’s address space, that’s for the user-level policy framework to decide.
Whether the present CAmkES framework supports this is a different question, which I’ll
leave to someone who’s more up to date with CAmkES details.
Gernot
15 Nov
15 Nov
3:59 p.m.
If only considering native components, it would be possible to extend camkes to support
the notion of creating a shared data connector between 2 components that is defined by the
address space of one end. It could currently be done with a custom connector type that
assumed a maximum virtual address of the target component I believe, but adding specific
support into camkes would likely allow specifying the elf program segments as something a
shared connector could be connected to.
But because camkes is a static system where you can specify that the monitor component has
read only access to the other native component.
For native Linux processes in a vm, you would probably need to trust modules inside the
vmm and the Linux kernel to describe where the process's address space ends up in
memory in order to scan it.
________________________________
From: Devel <devel-bounces(a)sel4.systems> on behalf of Heiser, Gernot (Data61,
Kensington NSW) <Gernot.Heiser(a)data61.csiro.au>
Sent: Saturday, 26 October 2019 2:07:23 PM
To: devel(a)sel4.systems <devel(a)sel4.systems>
Subject: Re: [seL4] releasing confidentiality
On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote:
Hi,
I know that seL4 provides confidentiality, which is described as a property that
"means that data cannot be read without permission." Given this wording, I
wonder if it is not possible to revoke those permissions in certain cases. In particular,
I would like for one camkes component to be able to perform runtime measurements, such as
heap analysis, on another component. Or even better, I would like for a component to be
able to perform runtime measurements on a program running within the camkes linux vm. Is
such a feat possible?
Hi Michael
seL4’s confidentiality (and other security) enforcement means that the kernel guarantees
that you can only access objects to which you have been given explicit permission (in the
form of a capability). How those permissions are allocated is a matter of policy, the
kernel doesn’t care, it only enforces.
In particular, it is totally possible in seL4 to give one component access to another
component’s address space, that’s for the user-level policy framework to decide.
Whether the present CAmkES framework supports this is a different question, which I’ll
leave to someone who’s more up to date with CAmkES details.
Gernot
_______________________________________________
Devel mailing list
Devel(a)sel4.systems
https://sel4.systems/lists/listinfo/devel
961
days inactive
982
days old
2 comments
3 participants
participants (3)
-
Heiser, Gernot (Data61, Kensington NSW) -
Mcleod, Kent (Data61, Kensington NSW) -
Michael Neises