Google KataOS and Sparrow

[Valerio Bellizzomi]

https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html

[William ML Leslie]

Very early days, but it looks like a solid foundation - seL4 and rust.

[Valerio Bellizzomi]

Yes William, that's why I posted it here.

[Stewart Webb]

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.

--- Stewart

On Sunday, 16 October 2022 at 20:52:54 UTC+11 vbell...@gmail.com wrote:

https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html

[Stewart Webb]

On the topic of the system's applications though... can someone tell me what the heck "ambient ML" is supposed to be/mean? 😅

[Mark S. Miller]

Are they using Rust as an ocap language?

--
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.

--

  Cheers,
  --MarkM

[Matt Rice]

On Mon, Oct 17, 2022 at 10:19 PM Mark S. Miller <eri...@gmail.com> wrote:
>
> Are they using Rust as an ocap language?
>

I don't think it should be considered that, the ocap layer is still
provided by the
sel4 kernel, but they have syscall stubs for calling seL4 syscalls from rust,
So really it is just within userspace that rust code is involved.

> To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYgYdMKt1negH5Q-0mhHP0hpxh0XjupsmxtowNLmQLdOxg%40mail.gmail.com.

[Mark S. Miller]

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?

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CACTLOFqM9o%2B-2nCo9QvpLyxzp%2BrK5ZDpWAbod%3D4t8iVVGrHM4g%40mail.gmail.com.

[William ML Leslie]

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

[Mark S. Miller]

Awesome! Thanks for the extended answer. All makes sense.

--

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.

--

  Cheers,
  --MarkM

[Matt Rice]

On Tue, Oct 18, 2022 at 2:19 AM '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?
>

Not disagreeing with anything William says, and I haven't looked at
KataOs/Sparrow that closely,
But I do not see anything that is trying to run e.g. mutually
suspicious rust code within the same address space.
Or expanding the protection domains beyond that of the existing seL4
process model.
It appears to me to just replace the C based kernel interface code
with a rust kernel interface,
and libc with rusts std library, etc.

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/

> To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD5Svc7vEpi%2B8dCQpL0S-ub91SPuCRkuB%3DaDptkWYzGwRA%40mail.gmail.com.

[William ML Leslie]

On Tue, 18 Oct 2022 at 13:22, Matt Rice <rat...@gmail.com> wrote:

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/

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:

https://hubris.oxide.computer/

--

William ML Leslie

[Ben Laurie]

On Mon, 17 Oct 2022 at 03:36, Stewart Webb <stewart.j...@gmail.com> wrote:

On the topic of the system's applications though... can someone tell me what the heck "ambient ML" is supposed to be/mean? 😅

Google in general uses "ambient" to describe a future in which the various devices around you collaborate to provide you with ... stuff.

Right now, you have smart devices about the place but they don't really know each other, resulting in annoying things like when you say "ok Google" to your Google Home (or whatever it's called this week) the phone in your pocket wakes up instead.

Incidentally, because we often have to talk about saying "ok Google" at work almost everyone actually says "ok G" so as not to wake their phones, etc, up.

 

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.

--- Stewart

On Sunday, 16 October 2022 at 20:52:54 UTC+11 vbell...@gmail.com wrote:

https://opensource.googleblog.com/2022/10/announcing-kataos-and-sparrow.html

[Ben Laurie]

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.

[Mark S. Miller]

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

[Alan Karp]

The Hubris documentation says, 

• 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.

Did I misunderstand something?

--------------
Alan Karp

--

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.

[William ML Leslie]

Ah no, it's my knowledge that needs updating, sorry.

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z21jhk2KT3Eu%3DRg2gR%3DM4nTP1zkGPLXMh5iF5J_mmDMzQ%40mail.gmail.com.

[Ben Laurie]

On Tue, 18 Oct 2022 at 16:54, Mark S. Miller <eri...@gmail.com> wrote:

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?

I can't find anything much, I'm afraid. We could contact this guy and ask: https://graymalk.in/?

 

 

 

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.

[John Kemp]

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.

[Mark S. Miller]

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/540ef3af-2fff-525f-c865-b6cb8d92ef96%40gmail.com.

--

  Cheers,
  --MarkM

[Stewart Webb]

On Tuesday, 18 October 2022 at 13:19:24 UTC+11 ma...@agoric.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?

Much of the system appears to be implemented within the CAMkES framework that facilitates making static systems for seL4 out of components (which each get locked in their own address space and capability-space) with explicit connections between them. You can see the 'assembly' of all their components and the connections between them here: https://github.com/AmbiML/sparrow-kata-full/blob/main/apps/system/system.camkes

CAMkES inter-component communication can be via seL4 Endpoint IPC (synchronous IPC with seL4_Call()), Notifications (asynchronous IPC via a CPU-word-sized set of binary semaphores), or shared memory regions ('Dataports').

It seems the Sparrow team has added their own 'copyregion' extension to CAMkES to allow having a page of memory shared between components: https://github.com/AmbiML/sparrow-camkes-tool/commit/32f2a71876e406885f34b077513a895dbefdcefe

Sam mentioned a lot of capability wrangling occurred in the MemoryManager service. From his code comments:

// The MemoryManager takes collections of Object Descriptors.

//

// For an alloc request an object descriptor provides everything needed

// to allocate & retype untyped memory. Capabilities for the realized

// objects are attached to the IPC buffer holding the reply in a CNode

// container. For free requests the same object descriptors should be

// provided. Otherwise clients are responsible for filling in

// allocated objects; e.g. map page frames into a VSpace, bind endpoints

// to irq's, configure TCB slots, etc.

I'm pretty sure CAMkES doesn't usually facilitate seL4 capability transfer between components but it seems they've tacked it back on at the point of IPC reply.

CAMkES components by default get their own small (1mb?) heap to back malloc() with - not sure if they are using this or perhaps a larger heap per-component. They would presumably be getting Rust's memory safety benefits at least on this heap.

A big problem trying to overlay ocap paradigms on seL4's cap system (that has come up in my research and that Will has somewhat mentioned before too) is that basically all of seL4's capability operations are synchronous, and most ocap languages are based around asynchronous invocation. Capability transfer in particular has to be synchronous. I think you can technically do nonblocking IPC on seL4 Endpoints but it's only really meant for protocol initialization (see this writeup from "Mr seL4" Gernot Heiser: https://microkerneldude.org/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/, particularly his comment "Any other IPC APIs are only for initiating communication protocols or exception handling.") - and the NBSend call doesn't give any indication of delivery success as part of seL4's information flow guarantees (reporting delivery success would constitute a backchannel). The nonblocking syscalls seem entirely centered around using the Notifications, which really only just let you signal from one process/domain to another.

There aren't any synchronous ocap languages around are there? 😅

--- Stewart

[Stewart Webb]

On Tuesday, 18 October 2022 at 14:58:05 UTC+11 william.l...@gmail.com wrote:

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:

https://hubris.oxide.computer/

I hadn't heard of Hubris (had heard of Oxide though!), cheers for the link.

Their 'lending memory' concept for IPC (https://hubris.oxide.computer/reference/#leases) seems really cool, and would no doubt actually work reasonably well with borrow-checking-like languages guarantees (as the docs indicate).

I think this kind of memory-lending has typically been a big problem in microkernel design though, where page faults get handled by userspace tasks. If you share a page as part of IPC, but then a page fault happens on it mid-syscall... then things get pretty messy!

[Mark S. Miller]

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.

 

--- 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.

--

  Cheers,
  --MarkM

[Matt Rice]

On Thu, Oct 20, 2022 at 7:19 AM Stewart Webb
<stewart.j...@gmail.com> wrote:
>
> the NBSend call doesn't give any indication of delivery success as part of seL4's information flow guarantees (reporting delivery success would constitute a backchannel). The nonblocking syscalls seem entirely centered around using the Notifications, which really only just let you signal from one process/domain to another.
>
> There aren't any synchronous ocap languages around are there? 😅

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).

[Ben Laurie]

On Wed, 19 Oct 2022 at 20:40, Mark S. Miller <eri...@gmail.com> wrote:

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?

CHERI does not enforce the same model as Rust (clearly, or  "good" unsafe code under CHERI would have to fail sometimes) so it can't be "safe" in the Rust sense of safe. But certainly it is safer. :-)

 

To view this discussion on the web visit https://groups.google.com/d/msgid/cap-talk/CAK5yZYjonYcCDpC2c2NFOu9Pj5Epw35hXvfxkM2YW2GtiNC1Tg%40mail.gmail.com.

[Stewart Webb]

On Thursday, 20 October 2022 at 18:44:19 UTC+11 eri...@gmail.com wrote:

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.

Oh, interesting. I had perhaps assumed that asynchronous send was core to most of the ocap languages cos it's featured so much (especially in distributed models with vats with event loops and so on). 

[Stewart Webb]

On Thursday, 20 October 2022 at 20:11:45 UTC+11 rat...@gmail.com wrote:

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).

Yeah it's just been a bit of a problem when trying to map it to most asynchronous language execution models, which seem to be common in distributed ocap languages, and is central to the Pony language and its actor model design. (I picked Pony for my project in the end mainly because it seemed the only ocap lang that compiles to machine code via LLVM)

[Dan Connolly]

On Mon, Oct 17, 2022 at 9:58 PM William ML Leslie <william.l...@gmail.com> wrote:

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.

Genode covers more of the "how do I actually build an operating system out of components using capability security?" than anything else I have seen: kernel, device drivers, windows system, networking, applications, copy-paste, screen recording, filesystems (with encryption), MMU, 3D graphics, and so on.

They also don't use language-level ocaps; their components are a few hundred lines of C++ each, when they get to do the whole design. But sometimes they integrate legacy code. At the coarse end, whole linux VMs. But they're getting better and better at doing individual device drivers with a pretty credible least-authority approach.

https://genode.org/documentation/release-notes/21.08#Linux-device-driver_environment_re-imagined 

One really cool thing they did was turn their display and keyboard session interfaces inside out: formerly, like X11, the server included the device driver, and clients made requests to draw things on the screen. But the norm is that clients rely on services and not the other way around. So if the hardware gets in a frotzed state, you have to take down the server, which takes down all the clients. So they turned it inside out: the part with the hardware is a client, which requests drawing instructions from application servers. When the hardware gets frotzed, you restart the driver client, and everything continues spinning like a top.

https://genode.org/documentation/release-notes/20.08#The_GUI_stack__restacked 

Regarding language level protections... I did manage to get the XS embedded JavaScript interpreter running in genode:

https://github.com/dckc/genode-js-xs

I haven't figured out a scalable approach to integrating with their services, though. They use RPC stubs generated from C++ code.

I did integrate with one method of one service Genode::log(message). I suppose that shows that it's possible to manually stub each of the session interfaces. And I suppose there are only roughly a dozen of them that cover most services... but they have callbacks and stuff... ugh.

The Genode Foundations book is really nice:

https://genode.org/documentation/genode-foundations/22.05/index.html

https://genode.org/documentation/genode-foundations-22-05.pdf

--

Dan Connolly

http://www.madmode.com/