- Devel - lists.sel4.systems

Re: Conclusions regarding speculation
by G. Branden Robinson 14 Nov '23

14 Nov '23

[sending a revised verison of this and one other message; Peter was able to confirm that the earlier ones got lost somewhere between exim and mailman--maybe my GPG signature attachment caused problems, so leaving that off] ----- Forwarded message from "G. Branden Robinson" <g.branden.robinson(a)gmail.com> ----- Date: Mon, 13 Nov 2023 02:51:36 -0600 From: "G. Branden Robinson" <g.branden.robinson(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Re: Conclusions regarding speculation At 2023-11-13T08:55:47+0100, Hugo V.C. wrote: > > One might as well just buy multiple laptops and be able to use them > > at the same time. > > *** You can not easily travel with multiple laptops and it is not a > comfortable solution, nor you can sell this idea to anyone. > Instead you can travel with a single laptop with 3 different computing > platforms inside, basically, the user will never know, it will be > transparent. When I was at TS we had a demo system that manifested this sort of partitioning, but I think it furthermore used a windowing system. The project was no longer under development while I was working there--probably it wasn't being actively funded--but the proof of concept seems to have been delivered. It may have had only two tiers, "red" and "black", with the former a data sink only (apart from what your eyeballs could see) and the latter a source and sink. Pretty sure someone else on the list can correct me and say more. (I want to say it was called MDDC? "Multi-Domain Display Controller"?] My other thought is that we're basically talking about putting a KVM ("keyboard/video/mouse", not "kernel virtual machine" :) ) switch inside a chassis with cores, storage, and peripheral ports. That doesn't seem like it should be too hard.[0] The physical dimensions of KVMs seem to be dominated by the sizes of the connectors attached to them. Not an issue inside a chassis. Economically there is a reason to expect this to come to pass as well; with the death of Moore's Law, I submit that we buy multicore CPU packages not because we use them efficiently--I don't, except when running "make -j", and that's a tiny fraction of my interaction time--it is because CPU vendors desire to keep the price point of the minimum configured processor model for consumer machines around USD 100. I guess some kind of commodity market dynamics are thought to set in somewhere below that point, and such dynamics are threatening to the U.S. consumer-facing semiconductor duopoly. (Vertical integration is a classic defense against having to participate in this sort of competition, and is consistent with Apple's in-housing of CPU design and manufacture.) As innovations go, this could be a benign one, and a real improvement if we seize the opportunity on the OS side. (We still need a capability-based OS and, as Hugo points out, a formally verified network stack.) Here's an amusing proof of concept with a mightily retro hardware/software stack. But if a hobbyist can do this in his garage... "Meet the ZedRipper – a 16-core, 83 MHz Z80 powerhouse as portable as it is impractical." http://www.chrisfenton.com/the-zedripper-part-1/ Aside: Just over the past couple of weeks, glibc and other libc implementers have held an open conversation with the Linux man-pages maintainer such that they're seriously trying to get the best available information to C programmers about how to perform the seemingly simple operation of copying strings, and why the silver bullets that have been touted to date, aren't.[1] For decades our industry has labored under the harmful myth that the standard C library, even as it existed in ANSI C89, was perfectly good enough for this, and if you screwed up it was because you're a bad programmer, not because C's infamously weak type system and silly selection of return values in its library[2] laid down a minefield for you to traverse. Rust has caught fire despite all the money Google has thrown at Go,[3] and a few people (not just me, I promise) even remember and point out how Ada got a lot of stuff right 40 years ago that the "close-to-the-metal"/portable-assembly school of hacking keeps getting pwn3d by.[4] gnulib is adding CHERI support as we speak.[5] I don't personally prefer CHERI to using a better language than C/C++ (and ISA than x86) from the ground up, but it is a serious and honest attempt to face the problems with C that code cowboys have waved aside for decades. Could our industry be--at long, long last--tiring of crap security? May it be. By all means put a KVM switch in an 8-package/64-hart RISC-V 64 laptop. I promise not to block the vent. Regards, Branden [0] This is how you know I'm not a hardware guy. [1] https://lore.kernel.org/linux-man/ZU4SDh-Se5gjPny5@debian/T/#mfb5a3fdeb3548… [2] https://www.symas.com/post/the-sad-state-of-c-strings [3] An oft-heard rebuttal to this observation is that Google wasn't/isn't really trying to target the same applications as Rust. That sounds like post hoc sour grapes. It's Google. They put Thompson and Pike on this. They were shooting for the moon. [4] https://lwn.net/Articles/919016/ [5] https://git.savannah.gnu.org/cgit/gnulib.git/log/ ----- End forwarded message -----

1 0

[RFC] Support CHERI/Morello in seL4
by Hesham Almatary 13 Nov '23

13 Nov '23

Hello, I have started working on porting seL4 to CHERI/Morello. Part of that, and as a first step, I submitted an RFC [1] as we aim to ideally upstream this work to make it reusable by others and allow collaborations. Any feedback or comments will be appreciated, happy to discuss further. For those who don't know me, I have worked on seL4 at the TS group from 2016-2018, during which I added FPU and SMP support to the Armv7 32-bit port, and added the RISC-V port. I then did my PhD on "CHERI compartmentalisation for embedded systems." [1] https://sel4.atlassian.net/browse/RFC-15 Regards, Hesham

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 12 Nov '23

12 Nov '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 15, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Where are the interrupts disabled in the kernel mode?
by chenpingyuan＠xiaomi.com 09 Nov '23

09 Nov '23

Hi experts, The sel4 whitepaper says "seL4, like most members of the L4 microkernel family, executes with interrupts disabled while in kernel mode.". But I didn't find the code which disabled interrupts when entering kernel mode, for example, when a syscall is triggered. Can anybody help to point out? Thanks.

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 29 Oct '23

29 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 1, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Camkes-vm-linux tutorial
by felicianidaniele＠gmail.com 26 Oct '23

26 Oct '23

Hi, I modified the vm_tutorial.camkes file to obtain two VMs. It works but I would like to see the two virtual machines on two different consoles. Is it possible? Thanks Daniele

1 0

vm-minimal on raspberry pi4
by felicianidaniele＠gmail.com 18 Oct '23

18 Oct '23

Hi everyone, I would like to run vm-minimal and vm-multi (camkes-vm-manifest repo) on raspberry pi 4 4gb RAM. Can someone help me? Thanks Daniele

1 0

Running Sel4 on Rasberry pi 4 4 gb RAM
by felicianidaniele＠gmail.com 18 Oct '23

18 Oct '23

Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c can someone help me? Thanks Daniele

2 2

Help with navigating the l4v repository
by Typaldos, Athanasios 18 Oct '23

18 Oct '23

Hello, I am from Lin Zhong’s group at Yale University and I am currently looking at the seL4 specifications and proofs. I am interested in finding the invariants at the abstract level regarding the capability management (CNode and CSpace). I would need some help with navigating the repository, because I am relatively new to interactive theorem proving in general. - I think what I am looking for is in the `l4v/proof/invariant-abstract` directory inside the `{CNode, CSpace}*_AI.thy` files. Is this correct ? - How can I distinguish between helper lemmas and the invariants that you state for example in your paper: SeL4: formal verification of an OS kernel<https://dl.acm.org/doi/10.1145/1629575.1629596> ? - Is there any textual artifact that lists the invariants in prose that could help me ? - Can you clarify me the relationship between the specifications in `l4v/spec/abstract` and the proofs in `l4v/proof/invariant-abstract` ? According to my understanding, the abstract specification defines the system in the abstract level, whereas the proofs use these definitions from the specifications to prove properties and invariants about them. So, the invariants are the statements that the proofs prove. Am I on the right track ? Thank you for your help, Thanasis Typaldos

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 15 Oct '23

15 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 18, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0