- Devel - lists.sel4.systems

CAmkES, Virtual Machines and Multicore Guarantees
by Demi M. Obenour 01 Apr '20

01 Apr '20

> On 18 Mar 2020, at 10:13, Demi Obenour <demiobenour(a)gmail.com> wrote: > > On Tue, Mar 17, 2020, 9:29 PM Klein, Gerwin (Data61, Kensington NSW) < > Gerwin.Klein(a)data61.csiro.au> wrote: > >> >> >> > On 18 Mar 2020, at 08:59, Demi Obenour <demiobenour(a)gmail.com> wrote: >> > >> > On Tue, Mar 17, 2020, 7:32 PM Mcleod, Kent (Data61, Kensington NSW) < >> > Kent.Mcleod(a)data61.csiro.au> wrote: >> > >> > The closest you could get to a multicore system that leverages verified >> >> kernel configurations would be to setup a multikernel implementation >> where >> >> each core had its own instance of a verified seL4 configuration where >> any >> >> hardware resources are strictly partitioned between them. I'm not >> aware of >> >> any examples of this setup but there have been research projects that >> have >> >> used multikernel implementations of seL4 in the past. Also this still >> >> wouldn't give you an overall system with the same guarantees as a >> single >> >> seL4 as the different instances would need to trust each other to not >> >> overwrite each other's kernel data structures and is outside of the >> current >> >> proof assumptions. >> >> >> > >> > Assuming that the root tasks drop capabilities that could be >> problematic, >> > would this still be correct? This seems to follow from the existing >> seL4 >> > specification (no way to get rights to memory from nothing). >> >> You can set up a system to be completely separated from the root task, >> and yes, that would increase confidence. There was a PhD thesis a while ago >> that had a semi-formal but fairly rigorous argument for why and how this >> will work, but you’d still not be running the verified configuration of the >> kernel, i.e. you’d have code in there that was not verified, even if that >> code doesn’t do much in this setup and you can probably convince yourself >> manually that it is fine. >> > > Since the code is deterministic, and will only ever have one initial > condition, is it possible to prove it correct by simply running the binary > and looking at the state after it executes? That is, this code could be > viewed as an extension of the kernel init code. > > > That would work per system, yes, although you’d have to re-do that > certification every time you tweaked something in the setup of that system. > > We’ve thought about this approach also for kernel initialisation in > general, i.e. writing an automated check that the invariants are true after > the system is initialised. There are a lot of expensive calculations in > that check, though, so we haven’t really gone with that. Still remains an > option, though. (Expensive, because the invariants have things like “for > every cap, if there exists another cap to the same object, this cap must > have the following properties” etc, ie. lots of forall/exists combinations > over all of memory, which are no problem in logic, but hard on > computation). > > You’d also still have kernel code that runs later that is not verified, > mostly very simple stuff such as instead of a current thread, you have an > array of current threads (one per CPU). The PhD thesis[1] did look at that > and concluded it’s all fine, but compared to a full code-level verification > that’s obviously lower assurance. The thesis is from 2013, so a lot has > happened since then, but the general idea still holds. > > [1]: > https://ts.data61.csiro.au/publications/nictaabstracts/vonTessin:phd.abstra… > > > > > Also, why is verifying fine-grained locking so difficult? CertiKOS >> managed >> > to do it, so I am probably missing something. >> >> I don’t see that much fine-grained locking in CertKOS, it mostly uses >> separation. It’s easier for it to do so, because it has a significantly >> simpler API (in fact, it’s probably quite similar to a multikernel setup in >> seL4 + messaging between cores. The only setups I’ve seen have precisely >> one VM per core). >> > > I was not aware of that, thank you. > > > It seems to be even worse, actually -- according to the paper that Gernot > posted there is no communication between cores, which if I think back to > the projects I’ve seen is actually true there as well, they used shared > memory between VMs to communicate, not kernel primitives. It also has > cooperative scheduling which is fine for some systems, but not others. It’s > notoriously hard to figure out what features CertiKOS actually has, because > the papers of course concentrate on other aspects such as verification (as > do ours, it’s probably not that easy to figure out what is verified in > which version of seL4 either without a lot of reading, but we do try to be > explicit about it :-)). > > Gernot is obviously not very happy with them from a systems perspective. > From the verification side, they have done some pretty cool things, just > not to the systems level that Gernot would find acceptable ;-) > > > Thank you so much. I view seL4 as universal, in that it should be > possible to build virtually any desired OS on top of it, and I am glad that > a high-performance multicore version with fine-grained locking at least > appears feasible. > > > It’s definitely part of the vision. There is a lot of thinking about > fine-grained vs big-lock, because the seL4 big-lock is about the order of a > Linux fine-grained lock, with some caveats, but the idea is that we want > this to scale. Is it planned to scale beyond the area of small inter-core communication costs? Obviously, transferring large amounts of data between cores on hot paths won't scale. However, I am still not convinced that a multikernel is the best way to go: it has always seemed like a hack to work around kernel limitations, and it seems to make slow-path control-plane userspace code far more complex. Such code often isn't performance critical at all, so forcing it to be distributed seems like unnecessary complexity. Furthermore, replicating data structures (such as page tables) which are almost entirely read-only seems like it could create substantial overhead, although I am not sure if that is an issue in practice. Finally, as someone who writes Rust professionally, I find thread-affine APIs to be quite annoying to deal with. Resources that can't be safely accessed by more than one thread concurrently are easy to wrap in clean APIs, but resources that can't be sent across threads are much harder to wrap. Making kernel resources specifically per-core, and preventing them from being transferred between cores, seems likely to lead to a bunch of userspace frameworks of varying quality that try to work around this limitation. > Are there any papers that I could read to learn more? > > > We don’t have anything really published yet on the verification side, > because it’s all still ongoing work. There is one about the big-lock idea, > though: > > https://ts.data61.csiro.au/publications/nictaabstracts/Peters_DEH_15.abstra… I read and like that idea. My biggest worry, however, is that a big lock won't scale beyond a small number of cores. The idea that fine-grained locking might be possible to verify gives me hope, as I had previously given up on that. > Cheers, > Gerwin Cheers, Demi=

2 1

Get/Set multiple message registers with the one syscall?
by Ben Ph 01 Apr '20

01 Apr '20

I'm looking at `seL4_GetMR()` and `seL4_SetMR()`, which requires a syscall for each get/set. To my naive eye, it seems like you're much better off running `seL4_GetIPCBuffer()->msg` then reading/writing to each index as needed, turning multiple syscalls (one for each get/set) into just the one. Am I missing anything? I was planning on replacing my Get/Set calls with direct array writes, but I'm wondering if I've missed reasons why I shouldn't. Thanks, Ben

2 2

Running cmakes-arm-vm under QEMU.
by Travis Wheatley 01 Apr '20

01 Apr '20

Greetings sel4 developers. Thus far I have successfully been able to build and boot the cmakes-arm-vm project on a Jetson TK1 board. However, my project requires a 64 bit target. I have built the TX1 version of this project but unfortunately do not have a TX1 board to try it out on. I would like to be able to run under QEMU but am not quite sure how to assemble all of the bits needed to do so. I believe what I need is a raw kernel image, a ramdisk, and a dtb file but not sure how to extract these in the proper formats from the files produced in the build process. Is there any existing documentation or guidance that can help me get a 64 bit buildroot kernel running under an sel4 vm to boot under QEMU? — Travis

2 1

Thank you very much. 答复: question about stash and pop between templates
by yadong.li 23 Mar '20

23 Mar '20

-----邮件原件----- 发件人: Matthew Fernandez [mailto:matthew.fernandez@gmail.com] 发送时间: 2020年3月22日 2:00 收件人: yadong.li 抄送: devel(a)sel4.systems 主题: Re: [seL4] question about stash and pop between templates I think I wrote the text you’re quoting, so I’ll attempt an answer. In connection templates, ‘me’ is not unique. I can’t remember exactly how this works, but ‘me’ either refers to the component instance of the end of the template you’re instantiating or to the connection itself. If you want to try and unravel the relevant code, it’s around lines 278-300 of the main function [0]. The ‘stash’ and ‘pop’ functions were implemented to expose some internals to advanced CAmkES users who wanted functionality beyond the template API. They were not widely used, and many of these users sidestepped them and used the even more questionable ‘_stash’ and ‘_pop’ variants. I would not be surprised if they do not work the way the documentation describes, and they should mostly be considered foot guns at this point. This is based on my ~5 year old memories so may be inaccurate or out of date. HTH [0]: https://github.com/seL4/camkes-tool/blob/master/camkes/runner/__main__.py#L… > On Mar 20, 2020, at 22:56, yadong.li <yadong.li(a)horizon.ai> wrote: > > Hi， > Recently, I try to learning about CMAKES > I have some question about stash and pop described as followes: > > “ > Passing Information Between Templates > You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” > What is the meaning of “between templates that share related me references.” ? > It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: > connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from > ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ > where can I found the code to share related ‘me’ between the instance. > > Thanks for your answer _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel

1 0

question about stash and pop between templates
by yadong.li 22 Mar '20

22 Mar '20

Hi， Recently, I try to learning about CMAKES I have some question about stash and pop described as followes: “ Passing Information Between Templates You often wish to do this with two related templates. For example, in the templates that form each side of a connection you often wish to talk about the same object on both sides. None of the templates currently call the low-level helper functions that enable this directly, but if you do want to invoke them, they are stash and pop. stash lets you save a Python object under a given key name and pop retrieves a previously saved Python object by key. Note that these are only usable for passing objects between templates that share related me references.” What is the meaning of “between templates that share related me references.” ? It is my understanding that template will be instantiated, every instance has its own ‘me’ , for example below: connection seL4VirtQueues ping_virtq_conn1(to ping_vqinit1.init, from ping_client.recv, from vm0.send1); To parse the AST, seL4VirtQueues-from.template.c will be called twice for ping_client.recv and vm0.send1, I think they should have their own ‘me’ where can I found the code to share related ‘me’ between the instance. Thanks for your answer

2 1

Plan to remove support for ARMv6 and KZM/imx31
by Mcleod, Kent (Data61, Kensington NSW) 20 Mar '20

20 Mar '20

We are planning on removing support for the KZM ARM11 platform in order to reduce maintenance burden. We are assuming that this is a dead platform and removing support won't affect anyone but it would be useful to know who if anyone is currently using this platform and how much interest there is in ongoing support. The platform was the original verification target of seL4 over 10 years ago and by now there doesn't appear to be any ways to obtain new hardware. It is starting to require more attention as the physical board we have is starting to intermittently fail independently from the KZM Qemu simulation target. Currently, the KZM platform is the only ARMv6 platform that we support and supporting it requires a few work-arounds for emulating mechanisms that newer hardware supports. Removing this platform also implies removing armv6 support. There is an older discourse topic for discussion on this topic here: https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-…

1 0

Would verifying ARM64 be any more difficult than verifying ARM32 was?
by Demi M. Obenour 19 Mar '20

19 Mar '20

Would verifying seL4 on ARM64 be any more difficult than verifying seL4 on ARM32 was? What about other architectures like POWER9? I hope I am not asking too many questions; I am just a curious outsider who hopes they can use seL4 someday. Sincerely, Demi

4 3

CAmkES, Virtual Machines and Multicore Guarantees
by Turner, Ben 18 Mar '20

18 Mar '20

Hi, In the seL4 FAQ section it states: "Multicore is presently supported on x64 and Arm v7 (32-bit) and v8 (64-bit). Verification of the multicore kernel is in progress (but presently as an unfunded background activity)." Considering only seL4 ----------------------------- My interpretation of this is that given a single seL4 application running on a device, it is not possible to currently guarantee the protections seL4 provides if the application invokes multiple threads across more than 1 core. Is this correct? Considering CAmkES ---------------------------- I would also like to know how CAmkES affects this. For example, looking at the vm_multi app for the exynos5422 in the camkes-arm-vm repository, what would the effect be of assigning unique CPU affinities to each of the VM components? Do the guarantees still hold in this situation? Thanks, Ben Turner Senior Engineer Roke Manor Research Ltd Tel: +44 (0)1794 833721 ben.turner(a)roke.co.uk<mailto:ben.turner@roke.co.uk> ________________________________________ Roke Manor Research Limited, Romsey, Hampshire, SO51 0ZN, United Kingdom.Part of the Chemring Group. Registered in England & Wales. Registered No: 00267550 http://www.roke.co.uk _______________________________________ The information contained in this e-mail and any attachments is proprietary to Roke Manor Research Limited and must not be passed to any third party without permission. This communication is for information only and shall not create or change any contractual relationship. ________________________________________

5 4

Configuring pinmux in am335x (beaglebone) can't be done from user mode
by Stephen Sherratt 18 Mar '20

18 Mar '20

Hi all, I've been experimenting with seL4 running on a Ninjablocks (https://www.engadget.com/2013/05/01/ninja-blocks/) that I had lying around. Inside there is a beaglebone, with a custom shield (or cape) containing a microcontroller (atmega328p), some LEDs and a radio. The beaglebone (which normally runs linux) sends json-encoded commands over a serial connection to the on-cape microcontroller, which runs firmware that decodes these commands and controls the LEDs and radio. The complication is that the am335x pins connected to the custom shield are multiplexed, and don't connect to a uart device by default (they are gpio pins by default). The "Control Module" in the am335x can be used to configure pin multiplexing, but it can't be written to in user-mode. From the am335x manual (http://www.ti.com/lit/ug/spruh73q/spruh73q.pdf, page 1449): "Note: For writingto the controlmoduleregisters,the MPUwill need to be in privileged modeof operationand writes will not work fromusermode." To test that the rest of my app works I added the control module to the beaglebone device tree overlay and hacked the kernel to configure the relevant pins to connect to the uart device during boot: https://github.com/stevebob/seL4/commit/4295035ac7fd720fb531b7e0893f1f1191e… And now I have a little rootserver that can control the colours of LEDs on the shield: https://github.com/stevebob/sel4ninja/blob/master/apps/hello-ninja/src/main… What would be the right way of configuring the control module in a seL4-based system, given that it has to happen in kernel mode? To configure the uart pins when running linux on the board, I had to add the following to the device tree: scm@0 { ... pinmux@800 { ... pinmux_uart0_pins { // <-- this was already here pinctrl-single,pins = <0x170 0x30 0x174 0x00>; phandle = <0x20>; }; pinmux_uart1_pins { // <-- I had to add this pinctrl-single,pins = <0x180 0x30 0x184 0x00>; phandle = <0x60>; }; The (seL4) kernel build system already has basic support for interpreting device trees. Would a reasonable solution to my problem be extending this support with a minimal statically-generated control module driver that configures pinmux during boot based on the device tree? There would still be a problem where each board could only have a single pinmux config (as specified by that board's device tree). It seems like an easy fix for this would be a config variable passed to the build system (similar to -DPLATFORM) that overrides the default device tree file. That way projects that want non-standard pinmux configs could bring their own device trees. Cheers, Steve

2 1

seL4 design principles
by Heiser, Gernot (Data61, Kensington NSW) 15 Mar '20

15 Mar '20

I’ve just posted a blog that tries to explain why de do things the way we de in seL4, and why we don’t do some other things, such as hardware abstraction. I hope this helps people understand better which kind of kernel changes are acceptable and which aren’t, and why the API isn’t designed for ease of use. https://microkerneldude.wordpress.com/2020/03/11/sel4-design-principles/ Gernot

3 4