Hello,
I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system?
Thanks, Robbie VanVossen DornerWorks
Hi Robbie,
it depends on how your root thread is set up.
If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects.
If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode.
You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again.
Cheers, Gerwin
On 20 Nov 2015, at 3:34 am, Robert VanVossen Robert.VanVossen@dornerworks.com wrote:
Hello,
I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system?
Thanks, Robbie VanVossen DornerWorks
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned?
On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:
Hi Robbie,
it depends on how your root thread is set up.
If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects.
If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode.
You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again.
Cheers, Gerwin
On 20 Nov 2015, at 3:34 am, Robert VanVossen <
Robert.VanVossen@dornerworks.com> wrote:
Hello,
I was wondering if I can safely destroy my application root thread after
I have
setup the capabilities and memory mappings for all of my other threads
in the
system?
Thanks, Robbie VanVossen DornerWorks
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Just to make sure we keep the terminology straight: seL4 only has master capabilities, no master objects.
The master cap is the cap that you get when you create the object. It confers full rights to that object. You can copy the cap, i.e. create derived caps to the same object, potentially with restricted rights, so that there is still only the one object, but potentially many caps to it.
If you revoke+delete this master cap, all caps derived from it are deleted, the object is deleted, and the memory can be reused (if there is still an untyped capability around that covers that memory, which allows you to create objects). If you also remove all untyped caps to that memory, the memory becomes inaccessible to the system.
In general, an object is deleted and made available for reuse if the last typed cap to that object is deleted. Memory is available for reuse if there is an untyped cap that covers that memory (potentially existing children of that untyped cap might have to be revoked first as well).
In case of the root thread, it may actually hold the only caps to some objects in the system. For instance, it might have created a frame and mapped it into some thread’s address space, but never given the frame cap to that thread, because it doesn’t want to give the thread any power to remap, unmap, or share the frame. If you now delete the frame cap in the root thread, that frame gets unmapped and made available for reuse. If nobody else has an untyped cap that covers this memory, it becomes inaccessible. If you keep the frame cap in an inert CNode, you force it to be static and available for the entire lifetime of the system. If you give it instead to a trusted OS server personality, it could be reused dynamically during runtime. Just depends on what you want to do and how you set things up.
Cheers, Gerwin
On 20 Nov 2015, at 10:06 am, Raymond Jennings <shentino@gmail.commailto:shentino@gmail.com> wrote:
What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned?
On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein <Gerwin.Klein@nicta.com.aumailto:Gerwin.Klein@nicta.com.au> wrote: Hi Robbie,
it depends on how your root thread is set up.
If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects.
If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode.
You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again.
Cheers, Gerwin
On 20 Nov 2015, at 3:34 am, Robert VanVossen <Robert.VanVossen@dornerworks.commailto:Robert.VanVossen@dornerworks.com> wrote:
Hello,
I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system?
Thanks, Robbie VanVossen DornerWorks
Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
So for objects...all caps go poof means the object is deleted.
But if all the caps for a memory frame go poof, the memory effectively has no owner and becomes abandoned and permanently orphaned from the system?
Hmm...what about the master I/O capability? I assume that if that one went, nobody could do I/O?
On Thu, Nov 19, 2015 at 3:33 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:
Just to make sure we keep the terminology straight: seL4 only has master capabilities, no master objects.
The master cap is the cap that you get when you create the object. It confers full rights to that object. You can copy the cap, i.e. create derived caps to the same object, potentially with restricted rights, so that there is still only the one object, but potentially many caps to it.
If you revoke+delete this master cap, all caps derived from it are deleted, the object is deleted, and the memory can be reused (if there is still an untyped capability around that covers that memory, which allows you to create objects). If you also remove all untyped caps to that memory, the memory becomes inaccessible to the system.
In general, an object is deleted and made available for reuse if the last typed cap to that object is deleted. Memory is available for reuse if there is an untyped cap that covers that memory (potentially existing children of that untyped cap might have to be revoked first as well).
In case of the root thread, it may actually hold the only caps to some objects in the system. For instance, it might have created a frame and mapped it into some thread’s address space, but never given the frame cap to that thread, because it doesn’t want to give the thread any power to remap, unmap, or share the frame. If you now delete the frame cap in the root thread, that frame gets unmapped and made available for reuse. If nobody else has an untyped cap that covers this memory, it becomes inaccessible. If you keep the frame cap in an inert CNode, you force it to be static and available for the entire lifetime of the system. If you give it instead to a trusted OS server personality, it could be reused dynamically during runtime. Just depends on what you want to do and how you set things up.
Cheers, Gerwin
On 20 Nov 2015, at 10:06 am, Raymond Jennings shentino@gmail.com wrote:
What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned?
On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:
Hi Robbie,
it depends on how your root thread is set up.
If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects.
If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode.
You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again.
Cheers, Gerwin
On 20 Nov 2015, at 3:34 am, Robert VanVossen <
Robert.VanVossen@dornerworks.com> wrote:
Hello,
I was wondering if I can safely destroy my application root thread
after I have
setup the capabilities and memory mappings for all of my other threads
in the
system?
Thanks, Robbie VanVossen DornerWorks
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
For objects, once all the caps have been deleted the object must be taken out of use. The "finaliseCap" function in seL4 ("finalise_cap" in the spec) does this cleanup.
Capability delegation works differently though. A parent capability can (usually) be deleted without cleaning up its children. If an initial Untyped is split into objects and the Untyped cap deleted, the objects persist, as long as their caps persist. I think this will be true of the master I/O cap also.
Cheers, Thomas.
On 20/11/15 11:46, Raymond Jennings wrote:
So for objects...all caps go poof means the object is deleted.
But if all the caps for a memory frame go poof, the memory effectively has no owner and becomes abandoned and permanently orphaned from the system?
Hmm...what about the master I/O capability? I assume that if that one went, nobody could do I/O?
On Thu, Nov 19, 2015 at 3:33 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au mailto:Gerwin.Klein@nicta.com.au> wrote:
Just to make sure we keep the terminology straight: seL4 only has master capabilities, no master objects. The master cap is the cap that you get when you create the object. It confers full rights to that object. You can copy the cap, i.e. create derived caps to the same object, potentially with restricted rights, so that there is still only the one object, but potentially many caps to it. If you revoke+delete this master cap, all caps derived from it are deleted, the object is deleted, and the memory can be reused (if there is still an untyped capability around that covers that memory, which allows you to create objects). If you also remove all untyped caps to that memory, the memory becomes inaccessible to the system. In general, an object is deleted and made available for reuse if the last typed cap to that object is deleted. Memory is available for reuse if there is an untyped cap that covers that memory (potentially existing children of that untyped cap might have to be revoked first as well). In case of the root thread, it may actually hold the only caps to some objects in the system. For instance, it might have created a frame and mapped it into some thread’s address space, but never given the frame cap to that thread, because it doesn’t want to give the thread any power to remap, unmap, or share the frame. If you now delete the frame cap in the root thread, that frame gets unmapped and made available for reuse. If nobody else has an untyped cap that covers this memory, it becomes inaccessible. If you keep the frame cap in an inert CNode, you force it to be static and available for the entire lifetime of the system. If you give it instead to a trusted OS server personality, it could be reused dynamically during runtime. Just depends on what you want to do and how you set things up. Cheers, GerwinOn 20 Nov 2015, at 10:06 am, Raymond Jennings <shentino@gmail.com <mailto:shentino@gmail.com>> wrote: What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned? On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein <Gerwin.Klein@nicta.com.au <mailto:Gerwin.Klein@nicta.com.au>> wrote: Hi Robbie, it depends on how your root thread is set up. If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects. If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode. You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again. Cheers, Gerwin > On 20 Nov 2015, at 3:34 am, Robert VanVossen <Robert.VanVossen@dornerworks.com <mailto:Robert.VanVossen@dornerworks.com>> wrote: > > Hello, > > I was wondering if I can safely destroy my application root thread after I have > setup the capabilities and memory mappings for all of my other threads in the > system? > > Thanks, > Robbie VanVossen > DornerWorks > > _______________________________________________ > Devel mailing list > Devel@sel4.systems <mailto:Devel@sel4.systems> > https://sel4.systems/lists/listinfo/devel ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems <mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
That’s precisely it, you can remove the master cap, but leave descendants alive. (The root thread problem occurs if there are no descendants).
And I can confirm that it works that way for the master IO cap as well.
Cheers, Gerwin
On 20 Nov 2015, at 4:37 pm, Thomas Sewell <thomas.sewell@nicta.com.aumailto:thomas.sewell@nicta.com.au> wrote:
For objects, once all the caps have been deleted the object must be taken out of use. The "finaliseCap" function in seL4 ("finalise_cap" in the spec) does this cleanup.
Capability delegation works differently though. A parent capability can (usually) be deleted without cleaning up its children. If an initial Untyped is split into objects and the Untyped cap deleted, the objects persist, as long as their caps persist. I think this will be true of the master I/O cap also.
Cheers, Thomas.
On 20/11/15 11:46, Raymond Jennings wrote: So for objects...all caps go poof means the object is deleted.
But if all the caps for a memory frame go poof, the memory effectively has no owner and becomes abandoned and permanently orphaned from the system?
Hmm...what about the master I/O capability? I assume that if that one went, nobody could do I/O?
On Thu, Nov 19, 2015 at 3:33 PM, Gerwin Klein <Gerwin.Klein@nicta.com.aumailto:Gerwin.Klein@nicta.com.au> wrote: Just to make sure we keep the terminology straight: seL4 only has master capabilities, no master objects.
The master cap is the cap that you get when you create the object. It confers full rights to that object. You can copy the cap, i.e. create derived caps to the same object, potentially with restricted rights, so that there is still only the one object, but potentially many caps to it.
If you revoke+delete this master cap, all caps derived from it are deleted, the object is deleted, and the memory can be reused (if there is still an untyped capability around that covers that memory, which allows you to create objects). If you also remove all untyped caps to that memory, the memory becomes inaccessible to the system.
In general, an object is deleted and made available for reuse if the last typed cap to that object is deleted. Memory is available for reuse if there is an untyped cap that covers that memory (potentially existing children of that untyped cap might have to be revoked first as well).
In case of the root thread, it may actually hold the only caps to some objects in the system. For instance, it might have created a frame and mapped it into some thread’s address space, but never given the frame cap to that thread, because it doesn’t want to give the thread any power to remap, unmap, or share the frame. If you now delete the frame cap in the root thread, that frame gets unmapped and made available for reuse. If nobody else has an untyped cap that covers this memory, it becomes inaccessible. If you keep the frame cap in an inert CNode, you force it to be static and available for the entire lifetime of the system. If you give it instead to a trusted OS server personality, it could be reused dynamically during runtime. Just depends on what you want to do and how you set things up.
Cheers, Gerwin
On 20 Nov 2015, at 10:06 am, Raymond Jennings <shentino@gmail.commailto:shentino@gmail.com> wrote:
What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned?
On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein <Gerwin.Klein@nicta.com.aumailto:Gerwin.Klein@nicta.com.au> wrote: Hi Robbie,
it depends on how your root thread is set up.
If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects.
If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode.
You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again.
Cheers, Gerwin
On 20 Nov 2015, at 3:34 am, Robert VanVossen <mailto:Robert.VanVossen@dornerworks.comRobert.VanVossen@dornerworks.commailto:Robert.VanVossen@dornerworks.com> wrote:
Hello,
I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system?
Thanks, Robbie VanVossen DornerWorks
Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Aye. Sorry for the side post, but my main question was indeed on if master capabilities (I/O, untyped memory, etc) were truly mortal once the kernel handed them off to the bootstrap thread.
Thank you for answering...and actually from a security point of view it's probably more secure to prove that a destroyed master capability is lost forever rather than escheated and put up for grabs again.
Somehow though I got the impression that, at least for memory, it was on a first come first serve basis and anything getting orphaned was recycled and put back up for grabs.
On Thu, Nov 19, 2015 at 9:51 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:
That’s precisely it, you can remove the master cap, but leave descendants alive. (The root thread problem occurs if there are no descendants).
And I can confirm that it works that way for the master IO cap as well.
Cheers, Gerwin
On 20 Nov 2015, at 4:37 pm, Thomas Sewell thomas.sewell@nicta.com.au wrote:
For objects, once all the caps have been deleted the object must be taken out of use. The "finaliseCap" function in seL4 ("finalise_cap" in the spec) does this cleanup.
Capability delegation works differently though. A parent capability can (usually) be deleted without cleaning up its children. If an initial Untyped is split into objects and the Untyped cap deleted, the objects persist, as long as their caps persist. I think this will be true of the master I/O cap also.
Cheers, Thomas.
On 20/11/15 11:46, Raymond Jennings wrote:
So for objects...all caps go poof means the object is deleted.
But if all the caps for a memory frame go poof, the memory effectively has no owner and becomes abandoned and permanently orphaned from the system?
Hmm...what about the master I/O capability? I assume that if that one went, nobody could do I/O?
On Thu, Nov 19, 2015 at 3:33 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:
Just to make sure we keep the terminology straight: seL4 only has master capabilities, no master objects.
The master cap is the cap that you get when you create the object. It confers full rights to that object. You can copy the cap, i.e. create derived caps to the same object, potentially with restricted rights, so that there is still only the one object, but potentially many caps to it.
If you revoke+delete this master cap, all caps derived from it are deleted, the object is deleted, and the memory can be reused (if there is still an untyped capability around that covers that memory, which allows you to create objects). If you also remove all untyped caps to that memory, the memory becomes inaccessible to the system.
In general, an object is deleted and made available for reuse if the last typed cap to that object is deleted. Memory is available for reuse if there is an untyped cap that covers that memory (potentially existing children of that untyped cap might have to be revoked first as well).
In case of the root thread, it may actually hold the only caps to some objects in the system. For instance, it might have created a frame and mapped it into some thread’s address space, but never given the frame cap to that thread, because it doesn’t want to give the thread any power to remap, unmap, or share the frame. If you now delete the frame cap in the root thread, that frame gets unmapped and made available for reuse. If nobody else has an untyped cap that covers this memory, it becomes inaccessible. If you keep the frame cap in an inert CNode, you force it to be static and available for the entire lifetime of the system. If you give it instead to a trusted OS server personality, it could be reused dynamically during runtime. Just depends on what you want to do and how you set things up.
Cheers, Gerwin
On 20 Nov 2015, at 10:06 am, Raymond Jennings shentino@gmail.com wrote:
What happens to those master objects if the capabilities go poof? Do they get locked up forever, or...as I suspect...do they just escheat to the public as abandoned?
On Thu, Nov 19, 2015 at 2:50 PM, Gerwin Klein Gerwin.Klein@nicta.com.au wrote:
Hi Robbie,
it depends on how your root thread is set up.
If it holds remaining master capabilities to objects in the system, you need to make sure those are not destroyed, because deleting them would delete those objects.
If you don’t want to hand out these master caps and untyped caps to the rest of the system (often there are good reasons for that), you would usually leave them in an inert CNode that also has a capability to itself. That CNode could just be the root thread CNode.
You can then safely destroy the root thread, e.g. make it suspend itself. If nobody else has a capability to it, it can never run again.
Cheers, Gerwin
On 20 Nov 2015, at 3:34 am, Robert VanVossen <
Robert.VanVossen@dornerworks.comRobert.VanVossen@dornerworks.com> wrote:
Hello,
I was wondering if I can safely destroy my application root thread
after I have
setup the capabilities and memory mappings for all of my other threads
in the
system?
Thanks, Robbie VanVossen DornerWorks
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Devel mailing listDevel@sel4.systemshttps://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
On 20 Nov 2015, at 23:34 , Raymond Jennings <shentino@gmail.commailto:shentino@gmail.com> wrote:
Somehow though I got the impression that, at least for memory, it was on a first come first serve basis and anything getting orphaned was recycled and put back up for grabs.
that’s the old (V4) L4, that didn’t have a principled resource management model.
Gernot
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-
Gernot Heiser -
Gerwin Klein -
Raymond Jennings -
Robert VanVossen -
Thomas Sewell