--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/62eab175-5a5e-4f94-a833-e059e020e7b3n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CACTLOFqM9o%2B-2nCo9QvpLyxzp%2BrK5ZDpWAbod%3D4t8iVVGrHM4g%40mail.gmail.com.
seL4 has a granularity limit of a page. Are they using Rust to subdivide authority further? Are they using Rust references/protected-pointers as delegatable bearers of authority? At the boundary, are they mapping Rust references to seL4 ocaps, so only code holding a particular Rust reference can invoke the corresponding seL4 ocap?
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAHgd1hGmu%3DtGU-2mV0TpO%2B-5EKNZMgakYZ5bZrHcKpR94gtuYQ%40mail.gmail.com.
The only things I know of trying to leverage the rust language memory
safety as part of their security models are
https://www.theseus-os.com/Theseus/book/index.html
https://www.tockos.org/
On the topic of the system's applications though... can someone tell me what the heck "ambient ML" is supposed to be/mean? 😅
On Monday, 17 October 2022 at 13:29:03 UTC+11 Stewart Webb wrote:Yes it looks like a pretty cool project - with RISC-V involved to some degree too. It was on the seL4 devel list a few months back: https://lists.sel4.systems/hyperkitty/list/de...@sel4.systems/thread/7D4GKRPJHMAXBUUXL2BHGDNWJ4YMG7SB/ , via two of the people involved - June Tate-Gans and Sam Leffler (of BSD fame?).Sam was also kind enough to reach out with some details earlier in the year in response to me asking for some examples of using capability transfer in seL4 projects, for my (University of Melbourne Computer Science Masters) research project into ocap languages on capability-based OSes.--- StewartOn Sunday, 16 October 2022 at 20:52:54 UTC+11 vbell...@gmail.com wrote:
On Tue, 18 Oct 2022 at 12:19, 'Mark S. Miller' via cap-talk <cap-...@googlegroups.com> wrote:seL4 has a granularity limit of a page. Are they using Rust to subdivide authority further? Are they using Rust references/protected-pointers as delegatable bearers of authority? At the boundary, are they mapping Rust references to seL4 ocaps, so only code holding a particular Rust reference can invoke the corresponding seL4 ocap?I have two points of involvement here, so maybe I can add some clarity.The first is why I said "very early days" - I mostly hope this takes off so that I can stop hacking on Coyotos. One big challenge when you are starting to develop against an API like that of Coyotos or seL4 is that very important parts of the API have no natural analogue in the language itself. Say I need to map a physical page, or range of physical pages, directly into my address space. How do I start interacting with the newly mapped pages in a capsafe way? How do I ensure that there were no pointers into the region of space I just clobbered? Maybe at some point we will have more sensible APIs for this, but at present it seems that language protections don't buy you much.
--The second is that there have been requests from both AOS students and industry that they can get started building things in rust on seL4, and some list members here have been present for those discussions. The fact is that anything whatsoever that makes it quick to get started building in rust on seL4 will accelerate system development, even if that simply means nostd for now; and a more complete seL4 uapi crate + lidl integration down the line.I should say that there has been a general impression that endpoints (in both Coyotos and seL4) are not really the ideal semantics for fine-grained objects that applications may want to expose. I have some fun things to say about implementing mutexen on Coyotos, the RequestMayBlock functionality of Coyotos streams, and about the IRQHelper (arguably, the one thing seL4 actually improved on in the Coyotos design) - these all put more emphasis on the need to get async right afaiac. The IPC model described by seL4's core platform is clearly not at the level of abstraction expected to actually build loosely-coupled systems from. We've a while to go before we have usable capabilities in these systems, but we are making progress.William ML Leslie
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAHgd1hGmu%3DtGU-2mV0TpO%2B-5EKNZMgakYZ5bZrHcKpR94gtuYQ%40mail.gmail.com.
On Tue, 18 Oct 2022 at 03:58, William ML Leslie <william.l...@gmail.com> wrote:On Tue, 18 Oct 2022 at 12:19, 'Mark S. Miller' via cap-talk <cap-...@googlegroups.com> wrote:seL4 has a granularity limit of a page. Are they using Rust to subdivide authority further? Are they using Rust references/protected-pointers as delegatable bearers of authority? At the boundary, are they mapping Rust references to seL4 ocaps, so only code holding a particular Rust reference can invoke the corresponding seL4 ocap?I have two points of involvement here, so maybe I can add some clarity.The first is why I said "very early days" - I mostly hope this takes off so that I can stop hacking on Coyotos. One big challenge when you are starting to develop against an API like that of Coyotos or seL4 is that very important parts of the API have no natural analogue in the language itself. Say I need to map a physical page, or range of physical pages, directly into my address space. How do I start interacting with the newly mapped pages in a capsafe way? How do I ensure that there were no pointers into the region of space I just clobbered? Maybe at some point we will have more sensible APIs for this, but at present it seems that language protections don't buy you much.If you use CHERI properly, this is a non-problem - virtual-to-physical mapping is fixed (modulo swap) and so newly mapped pages are necessarily at new addresses - and you can't have pointers for those addresses already existing because until you got access, you didn't have the capability to make them.Note, BTW, that CHERI-aware Rust is in hand...
------The second is that there have been requests from both AOS students and industry that they can get started building things in rust on seL4, and some list members here have been present for those discussions. The fact is that anything whatsoever that makes it quick to get started building in rust on seL4 will accelerate system development, even if that simply means nostd for now; and a more complete seL4 uapi crate + lidl integration down the line.I should say that there has been a general impression that endpoints (in both Coyotos and seL4) are not really the ideal semantics for fine-grained objects that applications may want to expose. I have some fun things to say about implementing mutexen on Coyotos, the RequestMayBlock functionality of Coyotos streams, and about the IRQHelper (arguably, the one thing seL4 actually improved on in the Coyotos design) - these all put more emphasis on the need to get async right afaiac. The IPC model described by seL4's core platform is clearly not at the level of abstraction expected to actually build loosely-coupled systems from. We've a while to go before we have usable capabilities in these systems, but we are making progress.William ML Leslie
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAHgd1hGmu%3DtGU-2mV0TpO%2B-5EKNZMgakYZ5bZrHcKpR94gtuYQ%40mail.gmail.com.
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CABrd9STL19EfqYD1%3D2aTHp%3DhAiQ8X4d3jouyuGOSqOC_BswQ6w%40mail.gmail.com.
Speaking of capabilities, in the security sense, Hubris doesn’t use any. The only object of note in the system is the task, and any task can look up and talk to any other task; we plan to address the most obvious issues with that statement using mandatory access control. Capabilities raise issues around revocation, proxying, branding, etc. that can yield useful results but don’t seem necessary for our application.
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAHgd1hHu9Kp9WfPWtnxeSsbVwZG-y6n3CgqU23iC%3D_ERAEiLNw%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z21jhk2KT3Eu%3DRg2gR%3DM4nTP1zkGPLXMh5iF5J_mmDMzQ%40mail.gmail.com.
On Tue, Oct 18, 2022 at 3:44 AM 'Ben Laurie' via cap-talk <cap-...@googlegroups.com> wrote:On Tue, 18 Oct 2022 at 03:58, William ML Leslie <william.l...@gmail.com> wrote:On Tue, 18 Oct 2022 at 12:19, 'Mark S. Miller' via cap-talk <cap-...@googlegroups.com> wrote:seL4 has a granularity limit of a page. Are they using Rust to subdivide authority further? Are they using Rust references/protected-pointers as delegatable bearers of authority? At the boundary, are they mapping Rust references to seL4 ocaps, so only code holding a particular Rust reference can invoke the corresponding seL4 ocap?I have two points of involvement here, so maybe I can add some clarity.The first is why I said "very early days" - I mostly hope this takes off so that I can stop hacking on Coyotos. One big challenge when you are starting to develop against an API like that of Coyotos or seL4 is that very important parts of the API have no natural analogue in the language itself. Say I need to map a physical page, or range of physical pages, directly into my address space. How do I start interacting with the newly mapped pages in a capsafe way? How do I ensure that there were no pointers into the region of space I just clobbered? Maybe at some point we will have more sensible APIs for this, but at present it seems that language protections don't buy you much.If you use CHERI properly, this is a non-problem - virtual-to-physical mapping is fixed (modulo swap) and so newly mapped pages are necessarily at new addresses - and you can't have pointers for those addresses already existing because until you got access, you didn't have the capability to make them.Note, BTW, that CHERI-aware Rust is in hand...Hi Ben!Anything we can read about CHERI-aware Rust?
--------The second is that there have been requests from both AOS students and industry that they can get started building things in rust on seL4, and some list members here have been present for those discussions. The fact is that anything whatsoever that makes it quick to get started building in rust on seL4 will accelerate system development, even if that simply means nostd for now; and a more complete seL4 uapi crate + lidl integration down the line.I should say that there has been a general impression that endpoints (in both Coyotos and seL4) are not really the ideal semantics for fine-grained objects that applications may want to expose. I have some fun things to say about implementing mutexen on Coyotos, the RequestMayBlock functionality of Coyotos streams, and about the IRQHelper (arguably, the one thing seL4 actually improved on in the Coyotos design) - these all put more emphasis on the need to get async right afaiac. The IPC model described by seL4's core platform is clearly not at the level of abstraction expected to actually build loosely-coupled systems from. We've a while to go before we have usable capabilities in these systems, but we are making progress.William ML Leslie
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAHgd1hGmu%3DtGU-2mV0TpO%2B-5EKNZMgakYZ5bZrHcKpR94gtuYQ%40mail.gmail.com.
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CABrd9STL19EfqYD1%3D2aTHp%3DhAiQ8X4d3jouyuGOSqOC_BswQ6w%40mail.gmail.com.
--Cheers,
--MarkM
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYhkgPGTqgSkk3k8LxZ_xnxUVOTgMxMW5Fif%3D2-pWjwDBg%40mail.gmail.com.
There was this talk at the CHERITech event: https://soft-dev.org/events/cheritech22/slides/Cooksey.pdf
- johnk
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CABrd9SRE8jStq0no96DpuO0pZm9%2BsEQ_9Zoa2rbB_NRJK5ta_w%40mail.gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/540ef3af-2fff-525f-c865-b6cb8d92ef96%40gmail.com.
seL4 has a granularity limit of a page. Are they using Rust to subdivide authority further? Are they using Rust references/protected-pointers as delegatable bearers of authority? At the boundary, are they mapping Rust references to seL4 ocaps, so only code holding a particular Rust reference can invoke the corresponding seL4 ocap?
Before I forget, some may also like Hubris. It only supports fully static systems (a-la most real world use of CAmkES and other capabilities-as-keys systems), but the components are configured in much the same way, and it's all rust - cap invocation is just a synchronous rust function call:
--- Stewart
--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/1a2f6b83-3d86-42de-86ef-20427020805en%40googlegroups.com.
Good slides!So in this Rust-on-Morello, even a program with "unsafe" is still safe, via dynamic CHERI tests rather than Rust static analysis? For this Rust, there would no longer be an escape hatch to say genuinely unsafe things?
To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjonYcCDpC2c2NFOu9Pj5Epw35hXvfxkM2YW2GtiNC1Tg%40mail.gmail.com.
E, Joe-E, Hardened JavaScript (aka SES), Monte, Midori, Emily, all have synchronous calls. Don't be distracted by the fact that some of these, E, Endo (distributed Hardened JS), Monte, and Midori also have asynchronous send. Of the ones I listed here off the top of my head, only Joe-E and Emily are synchronous-only.
FWIW in defense of seL4's non-blocking syscalls, which I've generally
enjoyed using when NBSend'ing on a reply cap it can generally be seen
as the
caller's fault if it isn't waiting for the reply. But it can be very
nice for signaling servers shared by many clients, while not blocking
on any particular client
or having to spawn multiple threads for each client. Rather than fully
async in all directions though, the way I've used it has been blocking
on whom you
await a reply, and async to whom you reply to, reminiscent of a
self-locking worm drive with its resistance to being back-driven
(shrug).
The first is why I said "very early days" - I mostly hope this takes off so that I can stop hacking on Coyotos. One big challenge when you are starting to develop against an API like that of Coyotos or seL4 is that very important parts of the API have no natural analogue in the language itself. Say I need to map a physical page, or range of physical pages, directly into my address space. How do I start interacting with the newly mapped pages in a capsafe way? How do I ensure that there were no pointers into the region of space I just clobbered? Maybe at some point we will have more sensible APIs for this, but at present it seems that language protections don't buy you much.