- Devel - lists.sel4.systems

Use C-parser on seL4 based application
by r2ji＠uwaterloo.ca 20 Nov '23

20 Nov '23

Hi, I have been trying to reuse the seL4 verification framework to verify a toy example I built on seL4, and I am currently stuck on the c-parser step. I am trying to use c-parser to parse the example I built, then conduct refinement verification. The toy example is a normal c project, which includes `sel4.h`. From this thread: https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/3QYNFY… I learned that I am supposed to do $ ./isabelle/bin/isabelle jedit -d . -l CParser toy.thy And the toy.thy file is supposed to begin with `install_C_file("toy.c")`. However, since toy.c includes sel4.h, I am not sure how to preprocess it before I put it into toy.thy. I know the standalone c-parser can have a -I flag to include in all the dependency directories, but it cannot open an interactive window. (From my understanding, the standalone c-parser seems to be only a checking tool) I also know that when sel4 is parsed into HOL, it is preprocessed into a single c file `kernel_all.c_pp`, which is later parsed. I am not sure if the preprocessor tool can be reused for other applications as well. My question is summarized as: 1. Is there a way to add an include directory in interactive CParser? 2. If not, can I reuse the preprocessing approach for sel4 to preprocess my application to a singleton file that can be parsed by c-parser? Any help will be appreciated! Thanks, Ru

2 2

Conclusions regarding speculation
by Demi Marie Obenour 18 Nov '23

18 Nov '23

I talked with a Xen developer and came to these conclusions: - Speculative taint tracking provides complete protection against speculative attacks. This is sufficient to prevent leakage of cryptographic key material, even in fully dynamic systems. Furthermore, it is compatible with fast context switches between protection domains. - Full time partitioning eliminates all timing channels, but it is possible only in fully static systems, which severely limits its applicability. - Time protection without time partitioning does _not_ fully prevent Spectre v1 attacks, and still imposes a large penalty on protection domain switches. Additionally, I am almost certain that: - On properly designed hardware, both time protection and speculative taint tracking can be enabled and disabled by systems software. - Time protection and speculative taint tracking are not mutually exclusive. A cloud provider might use time partitioning to partition different customers from each other, while guest OSs use speculative taint tracking to protect different processes from each other. In short, time protection is excellent, but it is not a sufficient mechanism for general-purpose computing. Speculative taint tracking is a different mechanism that is applicable to many more workloads, and which provides complete protection against speculative attacks. Both mechanisms can be used together depending on system security policy. -- Sincerely, Demi Marie Obenour (she/her/hers)

6 18

CfP: Microkernel and Component-based OS Devroom at FOSDEM 2024
by Martin Decky 16 Nov '23

16 Nov '23

Microkernel and Component-based OS Devroom at FOSDEM 2024 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based, unikernel-based and component-based operating systems will meet as part of FOSDEM 2024 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and other activities related to microkernel-based, unikernel-based, component-based operating systems and similar areas. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * languages, tools and toolchains used * enabling support for hardware (architectures, device drivers) and programming languages * development processes, debugging * maintenance, testing and release engineering * safety, security and robustness * trends and challenges * research and open questions * community and governance * use cases, experiences and status updates * best practices and lessons learned * demos The devroom has been scheduled to Saturday February 3rd 2024 in the afternoon (Central European Time). This is a call for your participation. We kindly ask you to submit your proposals no later than on December 10th 2023 (End of Day, Anywhere on Earth). Please use the pretalx [2] web site to submit your proposals. Note that this is a new submission system and the user accounts from the previous submission system (pentabarf) have not been transferred. Make sure to select the Microkernel and Component-based OS as the track when submitting your proposal and include at least the following information: * title of your proposal * short abstract (one or two paragraphs) * duration (at least 15 minutes and no longer than 40 minutes) * your full name * your short bio You can specify your preferred time slot of your proposal and any other relevant information. The communication language of the devroom is English. Please note that the devroom has been allocated only a half of a day this year. Therefore the final decision on the duration of the talks will be made by the devroom organizers based on the number of accepted proposals. The official devroom schedule (along with the accepted talks) will be announced on December 15th 2023 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will be published on the FOSDEM web site, too. About the Devroom Since the first Microkernel OS Devroom at FOSDEM 2012 [4], this devroom has been a part of each following FOSDEM (with slight variations of the name). The focus gradually widened to include component-based, unikernel-based and other operating systems. By now, it has become a somewhat institutionalized tradition for the open source operating systems community, a kind of "extended family meeting" and it is one of the places where microkernel and unikernel enthusiasts meet regularly. To this date, over two dozen projects have participated in one way or another. Many of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. As every previous year, the devroom will offer the "stage" both to established community members and to newcomers. We like to select the talks in an inclusive manner, while staying true to the main technical topics (system-level software, broadly speaking) and creating a balanced and unbiased schedule. We would like to keep the quality bar of the devroom same as in the previous years. Presenting at FOSDEM implies that the recordings of the talks will be published under Creative Commons license by FOSDEM. By submitting a proposal, the speaker agrees to have the talk made available publicly indefinitely. For organizational purposes, we also need contact information of the speakers of accepted talks. Microkernel Dinner It has also become a habit that the devroom participants dine together somewhere in Brussels. The year 2024 will not be any different, so there is going to be a dinner on Saturday night. We will inform you about the exact arrangements later. About FOSDEM FOSDEM [5] is a two-day conference organized by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognized as one of the largest and best such events worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. In recent years, FOSDEM has been hosting more than 8000 developers annually at the ULB Solbosch Campus in Brussels, Belgium. The participation in FOSDEM is totally free, although the organizers gratefully accept donations and sponsorship. No registration is necessary. Attendees are expected to follow the [6]FOSDEM's code of conduct. Important Dates Recap * 2023-12-10: Deadline for proposal submission * 2023-12-15: Schedule published and speakers notified of acceptance * 2024-02-03: Devroom taking place Contact For any comments, questions and suggestions, please do not hesitate to use the devroom's mailing list [3] to contact the devroom organizers. The primary organizers of the devroom in 2024 are: * Martin Decky * Razvan Deaconescu References [1] https://fosdem.org/2024/ [2] https://pretalx.fosdem.org/fosdem-2024/cfp [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] https://fosdem.org/ [6] https://fosdem.org/2024/practical/conduct/

1 0

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

15 Nov '23

[re-send 2/2] ----- Forwarded message from "G. Branden Robinson" <g.branden.robinson(a)gmail.com> ----- Date: Mon, 13 Nov 2023 04:03:16 -0600 From: "G. Branden Robinson" <g.branden.robinson(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Re: Conclusions regarding speculation Hi Demi, At 2023-11-13T03:39:00-0500, Demi Marie Obenour wrote: > > The difference is QubesOS do not rely on a verified hypervisor while > > the hypothetical system I'm talking about it will have seL4 booting, > > which is a verified piece of code. > > I would love that, but seL4 currently is missing at least five > critical security features on x86: > > 1. Interrupt remapping in the IOMMU. This is the sort of thing that gets solved by putting together a small team of engineers, some very thick manuals from the manufacturer, a contact inside the vendor to address points "accidentally" omitted or erroneously documented, and a not insignificant amount of money. A Simple Matter of Programming, in other words. > 2. Protection against speculative execution attacks the moment the > embargo breaks. > 3. The ability to either choose the appropriate mitigations itself, > or to let userspace choose them. > 4. Properly implemented speculative execution mitigations. These 3 seem to be what you and Gernot are arguing about and I feel unqualified to get into the middle of that. > 5. Microcode update support. This is like (1) except it will never happen with verifiability and reliability because that would either expose, or enable the replacement of, the "secret sauce", by which the profit margin on the chip is protected. And that is why we need fully open cores subject to third-party correctness verification. I've never even seen an argument that you can combine these properties with binary blobs or trade secrets. And as long as that is true we're sure to keep getting trashed by spec ex attacks or the next great innovation in system compromise. > Without all five of these, seL4 is _less_ secure than Xen, which > defeats the entire purpose of using it. As per the discussion in > https://github.com/seL4/seL4/issues/1108 this will not be fixed any > time soon. I may not be completely understanding your argument, but it sounds like you're saying that with Xen/QubesOS you essentially achieve compartmentalization by partitioning one process (in the Unix sense) per processor (in the cores plus shared caches sense). Once you do this, doesn't it start to look a lot like OpenVMS? This would initially be a good way to drive the KVM-switch-in-a-laptop into the market but I think it would run into scaling problems pretty quickly. > That’s why I asked about desktop-class hardware I can actually buy: > the only non-x86 desktop-class hardware I know of are Macs with Apple > silicon and POWER9 machines from Raptor, ...insanely expensive (5 figures USD) last I looked... And Apple won't give up secret sauce of any kind before the extinction of our species. They still curse John Sculley's name. > and seL4 supports neither. > Apple silicon has lots of nonstandard IOMMUs that seL4 would need to > support, and POWER is not supported at all. For the time being, we are simply screwed. We are the cows from which economic rents are milked; this pleases the Street. The only rescue from our plight is Joseph Schumpeter's "creative destruction", opinions of which seem to vary in a consistent way depending on one's temporal distance from an IPO. > (Fun fact: you probably have some formally verified cryptographic code > installed on your system _right now_, since NSS uses fiat-crypto for > some of its cryptographic primitives last I checked.) ! Share a link next time. :) > To be clear: I don’t fault seL4 for focusing on embedded right now. > The reward/effort ratio is vastly more favorable there. That, and I think the larger players in the industry perceive potential risks to the status quo. The promise of lower expenses down the road due to fewer security incidents is a really hard thing to quantify, and much decision making is tied to what can be said in the next quarterly 10-C filing with the SEC. Yes, Heartbleed can give you heartburn big time. But sufficiently large and reliable income streams salve any scald. Quality of implementation is simply not the sort of thing anybody on the financial side of any firm cares about unless it's as dramatic as an airplane falling out of the sky. (I would have said "or life support equipment not being fit for purpose", but that appears not to be the case.[1][2]) > Servers are significantly harder and I suspect desktops and laptops > are the worst-case scenario, because _everything_ is dynamic and > subject to the whim of a human who can and will break any simplifying > assumptions one has made. And this is even before one starts talking > about GPUs and other accelerators, which are a huge attack surface and > yet can be the difference between a system being usable and unusable > for the tasks people expect of it. There is a reason Qubes OS is > going to be supporting GPU acceleration at some point. > > That’s why I am so pessimistic about time protection on desktop: all > of the stuff I have read about it assumes at least some static > partitioning, and in the desktop world, static _anything_ simply > doesn’t exist. I think it's bad, but maybe not quite as bad as you do. I'm going to risk coming off as naïve for a moment. Or saying a bunch of stuff you (or everyone on this list) already knows. Getting back to CS 101 fundamentals, what does a computing system do? A. It computes things (runs instructions). B. It remembers things (has storage). C. It communicates with the world (performs I/O operations). Time division multiplexing is our solution to (A) and (C) when we have more things we want to compute and communicate than we have machine resources for. This is well-studied and reasonably well controlled. We tried cooperative multitasking; it didn't work out because we couldn't solve the halting problem (but mainly because programmers are not infallible). Fine. Limited bandwidth and measurable latencies are so pervasive that we _assume_ unreliability of all I/O (but largely hide it inside network stacks or bus protocols). That leaves (B). So the dynamic system problem boils down to the multiplexing of memory. And I venture that is mainly a problem because when DEC added virtual memory to the PDP-11 and the Berkeley CSRG rewrote the Unix kernel to use it (thus "vmunix"), we all fell into a trap. That trap has a name. Memory overcommit. Your userland application can't overcommit CPU cycles. You'll get preëmpted. You can't overcommit I/O, either; something will throttle you. So we've spent a few decades being fantastically reckless with memory, especially in C and C++. (And, worst of all, JavaScript, according to my htop(1).) Running out of memory was never supposed to be problem in real life; rare enough that, if you were a slouch, you used the return value of malloc/calloc/realloc without thinking, and if you weren't, you just fatal-errored out, proclaiming defeat. I expect that the next generation will start breaking the wretched habit of assuming unbounded memory availability. Here's why. We (desktop users) drastically under-use all these parallel cores in our systems. If we were to partition memory consumption at the application level for large problems, we could more easily apply divide-and-conquer strategies to them. This is not a new insight. "MapReduce" was a buzzword 20+ years ago. As often happens, stuff that got figured out at the "enterprise" level last generation trickles down to the desktop for this one. This time maybe we can do better than J2EE. So, as I see it, the solution to the "insanely dynamic system" problem is to stop being insane. Accept a bound on memory consumption. Stop overcommitting memory, which already causes frustrating problems.[3] Use something like Massif[4] to profile your heap usage. Ask for as much as you will need at process launch, or refactor your memory-hog functions to work within one or more smaller arenas. See what happens. Yes, some stuff that never used to crash will start crashing because its authors didn't bother writing with highly parallel systems in mind, or assumed that memory was infinite. We also used to watch things crash because people treated pointers and ints as equivalent. I'm old enough to remember the DEC Alpha teaching a lot of hard lessons in this area (and also with respect to unaligned memory accesses). We learned. Now, we will slowly learn to stop asking for more than we need, and how to carve up the memory arenas we use. We also may continue our slow migration away from worse-is-better behemoths like C/C++ and Unix kernels. Am I wrong? Could be. Point me to reading material. I try not to talk too much on this list. Tonight I reckon I blew through my quota for the year, and I still had something I wanted to post from the summit... :-| Regards, Branden [1] https://www.fiercebiotech.com/medtech/getinge-life-support-systems-temporar… [2] Take note of the dates mentioned in article [1] and compare it with the five-year share price history of the manufacturer. https://www.google.com/search?q=getinge+share+price If you'd bought in when the first recall started in "late 2020" and held ever since, you would not have lost money. And in fact you could have cashed out with 100+% profit in the second half of 2021. [3] https://lwn.net/Articles/668126/ [4] https://valgrind.org/docs/manual/ms-manual.html ----- End forwarded message -----

1 0

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

15 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 13 Nov '23

13 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 30 Oct '23

30 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 19 Oct '23

19 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 16 Oct '23

16 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

Incorrect dtb in the Microkit tutorial
by Luke Hart 09 Oct '23

09 Oct '23

Hello, It seems that the linux.dtb file supplied with the tutorial code is not correct and does not allocate enough memory for the initrd. The symptoms this issue caused when attempting to run part4 was that the libresolv.so.2 could not be opened and the vmm panic'ed. The linux.dtb supplied in the 'solution' folder in the git repository has 'initrd-end' set to a larger value and this version does work. Thanks, Luke

2 1

Re: The seL4 Microkit tutorial is now available
by Isaac Beckett 05 Oct '23

05 Oct '23

> Date: Wed, 4 Oct 2023 06:36:02 +0000 > From: Ivan Velickovic <i.velickovic(a)unsw.edu.au> > Subject: [seL4] The seL4 Microkit tutorial is now available > To: devel <devel(a)sel4.systems> > > Hello everyone, > > For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. > > The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. > > Thanks, > Ivan Hello, I was going to ask what Microkit was and how it differs from seL4 Core Platform, but I see it’s just a new name. That’s good to know. I’ll definitely be checking out that tutorial Also, where can I find information on comparison between CAMmkES and Microkit/seL4cp? I only have a vague idea of the difference between the two. Thanks, Isaac

2 1

The seL4 Microkit tutorial is now available
by Ivan Velickovic 04 Oct '23

04 Oct '23

Hello everyone, For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. Thanks, Ivan

1 0

Re: [oss-security] Xen Security Advisory 439 v1 (CVE-2023-20588) - x86/AMD: Divide speculative information leak
by Solar Designer 04 Oct '23

04 Oct '23

On Tue, Sep 26, 2023 at 09:59:19PM -0400, Demi Marie Obenour wrote: > These detailed security advisories are one of the things I love about > Xen. It's hard to trust a hypervisor (KVM) that will not issue them, > for then one has no way to know if a particular problem got fixed. I concur. I'd appreciate security advisories from the KVM project. > I'm CCing KVM here to make sure they have a fix. From their Git commit > history, I am almost certain that seL4 does not. I'm CCing the seL4 > developers to alert them of this and suggest that the x86 port be > removed or at least have a big warning. I strongly oppose removal of a port/support for a certain architecture just because some implementations of it are/were problematic. Adding a warning is fine. Alexander P.S. Demi Marie, please note that oss-security list content guidelines explicitly discourage CC'ing other lists(*), and Xen advisories are already stretching this. In this reply, I am still CC'ing many of what you had CC'ed as I am following up on your specific points relevant to those lists, but in general let's be more careful about this. (*) Because we may then get off-topic follow-ups from there, especially if CC'ing project user lists or high-volume lists like LKML. In this specific case, we're lucky so far.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 02 Oct '23

02 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 4, 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

Add GICv3 emulation support for vmm on arm platform
by colorglass4＠outlook.com 27 Sep '23

27 Sep '23

Hi, I am trying to run a guest Linux using seL4's vmm library on the rk3568 platform, which uses gicv3 as its irq controller. But there is only gicv2 emulation officially supported in the vm library. I did find that there are 2 "gicv3" branch of the repository, but they are all outdated and have not being maintained for a long time. Is there any plan to formally add the gicv3 support to vmm library? Thanks.

2 3

Sel4 VMM on zcu102
by An,Jianjun 26 Sep '23

26 Sep '23

Hi I have run sel4 on the development board of zcu102. I found on the official website that the camkes-vm project does not support the platform zcu102. Could you please give me some guidance to make the functions of this vmm run and run a linux on the guest. Thanks

2 4

Bug on sel4 rootserver?
by chenpingyuan＠xiaomi.com 12 Sep '23

12 Sep '23

Hello guys, I'm trying to run sel4 using qemu under macosx, but it looks crash happened(Same steps were done on Ubuntu, but nothing bad happened.). More info: I'm following the doc here with docker as the build environment: https://docs.sel4.systems/GettingStarted.html Any tips are appreciated. Logs: chenpingyuan@in-container:/host/sel4_arm64/build_aarch64$ ./simulate ./simulate: QEMU command: qemu-system-aarch64 -machine virt -cpu cortex-a53 -nographic -m size=2G -kernel images/sel4test-driver-image-arm-qemu-arm-virt Not in hyp mode, cannot reset CNTVOFF_EL2 ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[40a27000..40eed0b7] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 40b61eb8. Loaded DTB from 40b61eb8. paddr=[4023d000..4023efff] ELF-loading image 'kernel' to 40000000 paddr=[40000000..4023cfff] vaddr=[ffffff8040000000..ffffff804023cfff] virt_entry=ffffff8040000000 ELF-loading image 'sel4test-driver' to 4023f000 paddr=[4023f000..40634fff] vaddr=[400000..7f5fff] virt_entry=40e568 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. available phys memory regions: 1 [40000000..80000000] reserved virt address space regions: 3 [ffffff8040000000..ffffff804023d000] [ffffff804023d000..ffffff804023ed11] [ffffff804023f000..ffffff8040635000] Booting all finished, dropped to user space Caught cap fault in send phase at address 0 while trying to handle: unknown syscall 0x476dcc in thread 0xffffff807ffca400 "rootserver" at address 0x460964 With stack: 0x6e3ca0: 0x466a53 0x6e3ca8: 0x460b84 0x6e3cb0: 0x457474 0x6e3cb8: 0x0 0x6e3cc0: 0x6e3f30 0x6e3cc8: 0x0 0x6e3cd0: 0x0 0x6e3cd8: 0x4433f0 0x6e3ce0: 0x0 0x6e3ce8: 0x0 0x6e3cf0: 0x0 0x6e3cf8: 0x0 0x6e3d00: 0x0 0x6e3d08: 0x0 0x6e3d10: 0x0 0x6e3d18: 0x0

2 2

2 weeks left before the seL4 summit; there's still time to register
by June Andronick (seL4 Foundation) 06 Sep '23

06 Sep '23

The seL4 summit 2023 will start in 2 weeks in Minneapolis! There is still time to register if you haven’t done it yet. Summit: https://sel4.systems/Foundation/Summit/2023/ Register: https://events.linuxfoundation.org/sel4-summit/register/ Program: https://sel4summit2023.sched.com/ See you there!

1 0

next seL4 TSC meeting on Tue 12 Sep (Mon 11 Sep in US)
by Gerwin Klein 04 Sep '23

04 Sep '23

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Tue, 12 Sep, 4pm - Central Europe: Tue, 12 Sep, 8am - US West Coast (LA/SF): Mon, 11 Sep, 11pm See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/85916669769 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - action items form last meeting - discuss and vote on RFC-5 (The seL4 Core Platform) - discuss and vote on adding the seL4 Rust support repositories currently at https://github.com/coliasgroup/rust-seL4 to the seL4 GitHub org. - discuss steps for the next seL4 release - if there is time: discuss remaining open RFCs If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 04 Sep '23

04 Sep '23

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

1 0

Standalone experiments
by sean bruno 01 Sep '23

01 Sep '23

I'm investigating some of the different microkernels out there for some graduate exploration. The tutorials were awesome and got me bootstrapped *very* quickly, thank you for the effort on those. I am attempting to build a "hello-world" on my own and seem to be missing a step as base.cmake no longer can see the musllibc that I have in my tree. I'm fairly certain my CMake knowledge here is weak or I just flat out missed a step. My checkout tree looks like the following: $ tree -L 1 ├── build ├── CMakeLists.txt -> tools/cmake-tool/default-CMakeLists.txt ├── init-build.sh -> tools/cmake-tool/init-build.sh ├── kernel ├── projects ├── README.md └── tools $ tree -L 1 projects/ projects/ ├── hello-world ├── musllibc ├── seL4_libs └── util_libs When cmake runs from build, I see the following: ~/build]$ cmake -DCROSS_COMPILER_PREFIX=aarch64-linux-gnu- -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -C ../kernel/configs/AARCH64_verified.cmake ../projects/hello-world/ loading initial cache file ../kernel/configs/AARCH64_verified.cmake -- The C compiler identification is GNU 12.1.1 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /usr/lib64/ccache/aarch64-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 12.1.1 -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /usr/lib64/ccache/aarch64-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/lib64/ccache/aarch64-linux-gnu-gcc -- /home/sbruno/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating from DTB... WARNING:root:Only mapping 4096/16777216 bytes from node /iommu@12000000, region 0. Set kernel_size in YAML to silence. -- CPIO test cpio_reproducible_flag PASSED CMake Error at /home/sbruno/tools/cmake-tool/base.cmake:55 (find_package): By not providing "Findmusllibc.cmake" in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by "musllibc", but CMake did not find one. Could not find a package configuration file provided by "musllibc" with any of the following names: musllibcConfig.cmake musllibc-config.cmake Add the installation prefix of "musllibc" to CMAKE_PREFIX_PATH or set "musllibc_DIR" to a directory containing one of the above files. If "musllibc" provides a separate development package or SDK, be sure it has been installed. Call Stack (most recent call first): CMakeLists.txt:4 (include) -- Configuring incomplete, errors occurred!

2 1

CPU design, Re: Confidentiality and realtime requirements
by Isaac Beckett 27 Aug '23

27 Aug '23

> Date: Sun, 13 Aug 2023 16:18:08 +0000 > From: Gernot Heiser <gernot(a)unsw.edu.au> > Subject: [seL4] Re: Confidentiality and realtime requirements > To: devel <devel(a)sel4.systems> > >>>> On 12 Aug 2023, at 02:07, Demi Marie Obenour <demiobenour(a)gmail.com> wrote: >>>> >>> If you want to relax this, you’ll need a very careful analysis of your security requirements, and deploy TP where needed and omit where it’s not needed. But you can't prevent µarch timing channels without TP. Everybody knows about D-cache channels these days and how easy they are to exploit, and similar with LLC channels. And if you want to prevent at least those, then full TP has no extra cost. >> >> Does time protection require temporal isolation? > > Nope. Time protection is the mechanism that allows providing temporal isolation. > >>> Developing such a framework is on my agenda (it’s a core part of what I said I’m waiting for a good PhD student to work on). Basically I want to be able to make certain security guarantees where components have overt communication channels. An example is tab isolation in a browser: We want to have a fully functional web browser that allows processing of sensitive information in one tab, but guarantee that it cannot be leaked to a different tab. >> >> Another good example is different apps on a mobile device. Android allows any two applications on the same profile to communicate with mutual consent, and yet also allows one application to keep information secret from another. > > Yes. The smartphone space is really interesting. While built on top of the classical Unix security model (but implementable on a much simpler model) it demonstrates that stricter security policies (compared to desktops) can be made acceptable to users. > >> One critical requirement is that such a framework must allow an efficient implementation, both in terms of performance and power consumption. If it isn’t efficient enough to be deployed, then it won’t do people any good. > > Energy is (to first order) proportional to computation, so just looking at “performance” is good enough. > > And performance has always been our driver – see “security is no excuse for bad performance!” ;-) > > As I argued earlier, the performance cost of time protection is not higher than what you need to eliminate just the most easily exploitable cache channels. > > Gernot This makes me wonder if it’d make sense to design a new CPU and/or instruction set with the goal of eliminating timing and other side channels. Like, we had the Lisp machines with hardware support for Lisp, and now most CPUs are optimized for C and similar languages, and in turn those languages are optimized for those CPUs (x86, Arm, etc.). But I can’t say I know enough about computer science at this time to even tinker with the idea. And also, on the other hand maybe it doesn’t make sense to create hardware and accompanying software that are nearly impossible to non-destructively subvert, given the concerning trend of computer manufacturers and tech companies of restricting what code can run on their products. I don’t want to make something that could be set up to prevent an end user from modifying or running their own code. Isaac

4 9

How to understand seL4?
by Jason Long 24 Aug '23

24 Aug '23

Hello,I want to learn seL4 deeply. So that I can figure it out and develop it. Where should I start? Thank you.

2 1

How to enable SMP on qemu-arm-virt
by chenpingyuan＠xiaomi.com 21 Aug '23

21 Aug '23

Hello cool guys, I'm trying SEL4 using qemu-arm-virt platform with command： ../init-build.sh -DPLATFORM=qemu-arm-virt -DSIMULATION=true I noticed that SMP was not enabled by default, so I added: set(KernelMaxNumNodes "4") into kernel\src\plat\qemu-arm-virt\config.cmake. After running it with command ./simulate , I got the following error log and seL4 refused to continue: HVC is not supported for PSCI! My question is how shall I change the build scripts in order to run seL4 with SMP on qemu-arm-virt platform. Regards

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 21 Aug '23

21 Aug '23

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

1 0

A desktop OS based on seL4
by Jason Long 19 Aug '23

19 Aug '23

Hello,Is there an operating system that uses seL4 as a kernel and is suitable for home or server users like GNU/Linux or Windows OS? Thank you.

2 2

sel4cp and networking driver
by Sid Agrawal 14 Aug '23

14 Aug '23

Hi, I would like to setup a working example on sel4 with picoTCP and an eth driver. I came across this [1] from one of the seL4CP/sDDF demos and [2] from the camkes examples. However, I do not have access to those particular boards. I have a rspi4 and a Toradex Colibri iMX8X module with the aster carrier board. This Toradex has the same SoC ( iMX8X) as the tqma8xqp-1gb mentioned on the sel4cp website. Do you folks have any thoughts on how much effort it is getting seL4 working on "Toradex Colibri iMX8X" given it is supported on "tqma8xqp-1gb" which has the same SoC? I do not mind buying a specific development board as long as I know that I can use it for a while :) For folks who are working on sel4cp, what kind of dev setup do you have? I am looking for basic conveniences like flashing the image via USB (so I do not have to add/remove an SD card), TFTPboot, and some simple device drivers. I did see the instructions on TFTPbootat [3]. However, does it matter if the image was built via the sel4test of sel4cp? I think not, but I just wanted to double-check. And lastly, a higher-order question about seL4cp. How does sel4cp tie into the example in seL4_Libs [3], which has barebones libc and a VMM? Which is what I have used so far with sel4test. I understand that both sel4cp and camkes are for static systems, but I thought that I could use sel4cp to start some initial processes, such as a driver, a memory server, and some management processes. And later use process_spawn from seL4 libs to start additional PDs. Best, Sid [1] https://github.com/lucypa/sDDF [2] https://github.com/seL4/global-components/tree/master/components/Ethdriver/… [3] https://docs.sel4.systems/Hardware/GeneralARM

4 10

Confidentiality and realtime requirements
by Demi Marie Obenour 14 Aug '23

14 Aug '23

One of the goals of the MCS scheduler is to allow untrusted parts of the system (such as device drivers) to still have low interrupt latency. However, this seems to interact badly with the domain scheduler, as interrupts can arrive when the domain that will serve them is not scheduled. Worse, it appears that interrupts will generally require an IBPB (or equivalent) on both entry and exit, since they may interrupt any code. Is this accurate? If so, it seems that the “flush all μArch state” instruction coming to some RISC-V CPUs is insufficient, and full speculative taint tracking is required. More generally, requiring mutually distrusting domains to be explicitly marked seems to be problematic for anything that is not a static system: in a dynamic system (one that can run third-party code), one must typically assume that different address spaces are mutually distrusting, with the result that IPC latency will be severely impacted. Am I missing something, or will a general-purpose OS need full speculative taint tracking in hardware if it is to have fast IPCs between mutually-distrusting code on out-of-order CPUs? -- Sincerely, Demi Marie Obenour (she/her/hers)

3 13

Changing the cspace of a TCB while it is listening on a EP
by Sid Agrawal 08 Aug '23

08 Aug '23

Hi, I have a scenario and would like to understand how the kernel is expected to behave when I change the CSpace of a TCB when it is blocked on an EP. 1. A TCB (say TCB_1) is blocked on seL4_reply() on an endpoint (say EP_1). 2. Now, another PD, which has the capability to TCB_1, changes the CSpace of TCB_1 by using seL4_TCB_SetSpace(). Let's assume that the VSpace is identical. This new CSpace can be different from the old CSpace in 4 ways: A. It doesn't have the endpoint EP_1 B. It has the endpoint EP_1 but at a different CSlot. C. It has the endpoint EP_1 at the same CSlot. But since it is a different CSpace(so CNodes shared), it is a minted copy of the EP_1. Let's call it EP_1-prime. D. It has the endpoint EP_1 at the same CSlot, and it is the same EP as I have shared the CNode containing the EP_1 from the original CSpace. New and old CSpaces share the CNode containing that EP_1 like two trees sharing a sub-tree. I think scenario D should work as if nothing happened, but I do not know what to expect in scenarios A, B, and C. I will try these out soon, but I wanted your input as I did not find a clear answer in the manual. Best, Sid

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 07 Aug '23

07 Aug '23

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

1 0

Ultra96V2 in sel4cp_VMM is cautiously here - initial support
by Nataliya Korovkina 06 Aug '23

06 Aug '23

Highlights, briefly... 1. Project "ultra96v2-sel4cpvmm" The project introduces changes to the three components: seL4, sel4CP, sel4cp_VMM. * Xilinx Linux booting requires SMC calls support in seL4. The project uses the SMC cap impelementation offered by DornerWorks (approved but not merged). * Changes in sel4CP relate to the new capability in seL4. * As for sel4cp_VMM, a policy of VM's SMC calls handling will be different from one VMM-PD to another. The project introduces registration of a custom handler by PD application as well as it provides the default handler - the simplest "pipe" passing calls and responses through. The project published as sets of patches to the components. More the details are in the README.md and Issue #1 - https://github.com/malus-brandywine/ultra96v2_sel4cpvmm/issues/1 of the project: https://github.com/malus-brandywine/ultra96v2_sel4cpvmm 2. Project "petalinux-ultra96v2-sel4cpvmm" The project enables generation of linux image and minimal rootfs to run VM with sel4cp_VMM. More details are in README.md of the project: https://github.com/malus-brandywine/petalinux-ultra96v2-sel4cpvmm Status: Linux VM loads to login prompt

1 0

2 weeks left to get the early-bird registration at the seL4 summit
by Birgit Brecknell 04 Aug '23

04 Aug '23

2 weeks left to get the early-bird registration at the seL4 summit! A friendly reminder that the early bird cut-off date is 18 August 2023. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and Dinner Registrations: https://events.linuxfoundation.org/sel4-summit/register/ seL4 summit 2023: https://sel4.systems/Foundation/Summit/2023/<https://sel4.systems/Foundation/Summit/2023/> --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

CMake error “Variable 'KernelArch' is not set.” Happens when building RISCV based seL4 system.
by sueboxian＠gmail.com 25 Jul '23

25 Jul '23

Hi, I met a CMake error, “Variable KernelArch is not set” when I tried to build a seL4 project based on the open source code of the UNSW course, Advanced Operating System, aka. AOS. The original version uses odroidc2 as the building platform, and I want to build it with the riscv gnu toolchain and simulate it on qemu-riscv-virt. Here is the repository: https://github.com/SEL4PROJ/AOS-manifest The building hierachy is as the basic build system structure, with init-build.sh, setting.cmake and CMakeLists.txt in the top level. And the top level contains kernel, tools, and project folders, in which there are CMakeLists.txt and .cmake files. Since I have no experience on cmake, I tried to compare the manifest xml between AOS project and seL4test project. I found that the major difference between them are in “init-build.sh”, “setting.cmake” and the “CMakeList.txt” in the top level. There are also some unused libraries in AOS project. I tried deleting the “set PLATFORM odroidc2” command in the setting.cmake, and added the DCROSSCOMPILER=riscv-unknown-linux-gnu, DPLATFORM=qemu-riscv-virt in the build command. But they doesn’t work. After checking the “/kernel/configs/seL4Config.cmake”, it says that the error is caused since KernelArch is left as empty string… And I want to ask whether I have set anything improperly.... I will appreciate for any help. Thank you for reading my question!

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 24 Jul '23

24 Jul '23

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

1 0

Soft-float problem happens when building seL4test using riscv64-unknown-linux-gnu-gcc toolchain
by sueboxian＠gmail.com 15 Jul '23

15 Jul '23

Hi, I met a problem when building seL4test project with riscv toolchain, with the float operations compiled as soft-float. Here are my configuration commands:  python3 ~/bin/repo init -u https://github.com/seL4/sel4test-manifest  python3 ~/bin/repo sync  mkdir build-riscv  cd build-riscv  ../init-build.sh -DPLATFORM=qemu-riscv-virt -DCROSS_COMPILER_PREFIX=riscv64-unknown-linux-gnu- -DSIMULATION=TRUE  ninja The terminal reported "can't link double-float modules with soft-float modules" errors when compiling fpu.c, and thus stopped compilation. I have tried rebuilding the glibc version riscv toolchain, with multilib enabled. But it doesn't work. I also checked the terminal, it says that I'm compiling with march=riscv64imac_zicsr_zifencei -mabi=lp64, which as the best of my knowledge, means compiling the float as soft-float. I want to know whether I lossed something. I would appreciate for any help. Thanks in advance.

3 6

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jul '23

10 Jul '23

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

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 23 Jun '23

23 Jun '23

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Wed, Jun 28, 7am (UTC), Topics: (open) * Sydney: Wed, Jun 28, 5pm * Central Europe: Wed, Jun 28, 9am * US Pacific Time: Wed, Jun 28, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Bitfield generator EBNF grammar
by June Tate-Gans (ジューン) 07 Jun '23

07 Jun '23

Hey guys, I've been attempting to put together some rust bindings for the seL4 fault handling mechanisms, and I'm afraid the bitfield generator is driving me a bit up a wall at this point. I'd like to find a concise grammar for the language so I can better understand how bitfield_gen.py works, but there doesn't seem to be any explicit BNF for it anywhere. Is there a paper I should be reading or a reference guide somewhere that would help? Thanks! -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

3 5

question about sel4 kernel preemptionPoint
by yadong.li 05 Jun '23

05 Jun '23

Hi: I have one question about sel4 kernel preemptionPoint on smp platform such as ARMv8. Take an example, when kernel takes long time to clear memory when UntypedRetype kernel object on core1, it will check preemptionPoint, when pending IRQ exists on core1, it will handle this irq, and return to userspace let other syscall or cores such as core2 have chance to run, but irq pending only check current cpu(PerCPU), no all cores of smp system, if core1 execute long seL4_Untyped_Retype syscall, core2 has a pending irq, the pending irq will not be checked in current core1, it will block until the execution of long syscall is completed if we take no account of archtimer irq, This phenomenon looks inconsistent at the system level between signal core and mutil core I want to know the current design intent about preemptionPoint of archtimer interrupt and other peripheral interrupts on SMP platform, only take current core interrupt as soon as possible or give other core and high priority task a chance to entry kernel and take big kernel lock? Thanks for your help

2 1

seL4 Rust crates doc links broken
by Hugo V.C. 01 Jun '23

01 Jun '23

Hi all, was looking around the Rust crates to check what is available to play around with seL4 from Rust and just found that most interesting ones (sel4_sys, sel4-start, ...) have documentation pointing doc.robigalia.org which is a broken link. Looks like the only communication way to Robigalia is #robigalia IRC channel... (I don't use IRC since 90s, not used to it anymore...) so I'm publishing this info here as I bet those amazing developers are in this list too and can read this message: please 🙏 fix the link at crates.io. Beside this, I will never get tired of remember the importance of taking care of the "general public" (that is, common developers not familiarized with seL4, common companies that are not security nor technical gurus, etc... that is, the average potential user of seL4 in the future) so it has an "easy/friendly" approach to seL4 as an early adopter. For that reason, checking that (healthy) Rust environment is there available for everyone will be a good starting point. seL4 topic is complex enough with documentation, so without it becomes simply not usable (for humans... 😅). Hoping Robigalia amazing guys can read this here, thank you for your work on Rust, as this is the best interface to seL4 development for people living on this planet. Best,

1 0

porting to a new platform
by steve.burke.56＠gmail.com 01 Jun '23

01 Jun '23

I'm trying to port an old sel4 code base to the latest so I decided to take the sel4test manifest & work through through the following page (https://docs.sel4.systems/projects/sel4/porting.html) The old code base does not add the new platform the same way since the new code seems to have some new CMake macros that do most of the heavy lifting. Is there a test project that does this with an arbitrary platform that I can use as a reference? My platform defines don't seem to be coming through correctly. Is working through the porting page the best way to do and does it seem current? Thanks.

3 2

Reminder seL4 developer hangout
by Birgit Brecknell 29 May '23

29 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 31, 7am (UTC), Topics: (open) * Sydney: Wed, May 31, 5pm * Central Europe: Wed, May 31, 9am * US Pacific Time: Wed, May 31, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Ring 3 iopl is going away, seL4 is ok
by William ML Leslie 21 May '23

21 May '23

Hello, I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me. Here's Intel's RFC: https://www.intel.com/content/www/us/en/developer/articles/technical/envisi… I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways! -- William ML Leslie

3 3

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

Reminder seL4 developer hangout
by Birgit Brecknell 15 May '23

15 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, May 16, 10pm (UTC), Topics: (open) * Sydney: Wed, May 17, 8am * Central Europe: Wed, May 17 12pm midnight * US Pacific Time: Tue, May 16, 3pm Calendar link: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 01 May '23

01 May '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 3, 7am (UTC), Topics: (open) * Sydney: Wed, May 3, 5pm * Central Europe: Wed, May 3, 9am * US Pacific Time: Wed, May 3, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW birgit.brecknell(a)unsw.edu.au 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

One week to go to submit a talk for seL4 summit 2023!
by Birgit Brecknell 17 Apr '23

17 Apr '23

One week to go to submit a talk for seL4 summit 2023 [0]! If you'd like to submit a talk, please upload an abstract of one page or less to the submission portal [1]. The seL4 Summit 2023 will be held 19 - 21 September 2023 at the Elliot Park Hotel, Minneapolis, USA. The summit will be hosted by the Linux Foundation, and will be an in-person event. Registration details to follow soon. We're looking forward to many exciting proposals! [0] https://sel4.systems/Foundation/Summit/2023/cfp [1] https://sel4.systems/Foundation/Summit/2023/submit --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 17 Apr '23

17 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 18, 10pm (UTC), Topics: (open) * Sydney: Wed, Apr 19, 8am * Central Europe: Wed, Apr 19, 12pm midnight * US Pacific Time: Tue, Apr 18, 3pm Calendar link: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Release of the CAmkES to seL4CP Transition Guide
by Jingyao Zhou 14 Apr '23

14 Apr '23

Hi all, The initial version of the CAmkES to seL4CP Transition Guide has been released. The guide aims to provide information and advice for those who are migrating applications built using CAmkES to the seL4 Core Platform. The main focus of this guide is on device driver development and virtual machine (monitor) development. The PDF version of this guide can be found on the Trustworthy Systems web page: https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4… <https://stage.trustworthy.systems/projects/TS/sel4cp/2304-11-camkes-to-sel4…> The source of this guide can be found in the Trustworthy Systems GitHub repository: https://github.com/au-ts/camkes_to_sel4cp_guide <https://github.com/au-ts/camkes_to_sel4cp_guide> Please don’t hesitate to provide feedback! Regards, Jade.

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 03 Apr '23

03 Apr '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Apr 5, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 5, 5pm * Central Europe: Wed, Apr 5, 9am * US Pacific Time: Wed, Apr 5, 12pm (midnight) Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

seL4 summit: deadline extension to 24th of April
by June Andronick (seL4 Foundation) 31 Mar '23

31 Mar '23

The deadline to submit a presentation to the seL4 summit 2023 is extended by 2 weeks. You now have until the 24th of April 2023 to propose a talk, by uploading an abstract of one page or less to: https://sel4.systems/Foundation/Summit/2023/submit The reason for the extension is that we want to let you know the definite dates for the summit before the deadline :) Current tentative (and very likely) dates are 19-20-21 September 2023, to be confirmed very soon. Looking forward to receiving your proposals. We want to hear about your cool seL4 work! And spread the word! If you want to hear about specific seL4 work, ping people around you or let us know at summit(a)sel4.systems <mailto:summit@sel4.systems> June

1 0

Issue for setting up the seL4 IPC tutorial
by zhliao＠iastate.edu 26 Mar '23

26 Mar '23

Hi all, I got the following issue when I followed the IPC tutorial to set up an environment. I can build and run the "Hello world" and "Capabilities" tutorials, so I think I have fulfilled the prerequisites for running the IPC tutorial. However, when I built the ipc tutorial using the command "./init --tut ipc --solution" or "./init --tut ipc", and ran the "ninja" command, the following error messages were given: [54/208] Generating capDL-tool/parse-capDL FAILED: capDL-tool/parse-capDL cd /home/zhliao/sel4_tutorials_manifest/ipc_build/capDL-tool && printf capDL-tool/parse-capDL:\ > /home/zhliao/sel4_tutorials_manifest/ipc_build/capDL-tool/parse-capDL.d && find -L /home/zhliao/sel4_tutorials_manifest/projects/capdl/capDL-tool/ -type f -printf %p\ >> /home/zhliao/sel4_tutorials_manifest/ipc_build/capDL-tool/parse-capDL.d && cp -a /home/zhliao/sel4_tutorials_manifest/projects/capdl/capDL-tool/* . && /usr/bin/cmake -E env make stack build --fast Downloading lts-19.12 build plan ... RedownloadInvalidResponse Request { host = "raw.githubusercontent.com" port = 443 secure = True requestHeaders = [] path = "/fpco/lts-haskell/master//lts-19.12.yaml" queryString = "" method = "GET" proxy = Nothing rawBody = False redirectCount = 10 responseTimeout = ResponseTimeoutDefault requestVersion = HTTP/1.1 } "/home/zhliao/.stack/build-plan/lts-19.12.yaml" (Response {responseStatus = Status {statusCode = 404, statusMessage = "Not Found"}, responseVersion = HTTP/1.1, responseHeaders = [("Connection","keep-alive"),("Content-Length","14"),("Content-Security-Policy","default-src 'none'; style-src 'unsafe-inline'; sandbox"),("Strict-Transport-Security","max-age=31536000"),("X-Content-Type-Options","nosniff"),("X-Frame-Options","deny"),("X-XSS-Protection","1; mode=block"),("Content-Type","text/plain; charset=utf-8"),("X-GitHub-Request-Id","35BE:17FF:128736E:17D5D97:641FC551"),("Accept-Ranges","bytes"),("Date","Sun, 26 Mar 2023 04:08:49 GMT"),("Via","1.1 varnish"),("X-Served-By","cache-lga21983-LGA"),("X-Cache","MISS"),("X-Cache-Hits","0"),("X-Timer","S1679803730.680346,VS0,VE66"),("Vary","Authorization,Accept-Encoding,Origin"),("Access-Control-Allow-Origin","*"),("X-Fastly-Request-ID","87538dc12b06e4fb615de6c1a4159b9af113e3a6"),("Expires","Sun, 26 Mar 2023 04:13:49 GMT"),("Source-Age","0")], responseBody = (), responseCookieJar = CJ {expose = []}, responseClose' = ResponseClose}) make: *** [Makefile:51: parse-capDL] Error 1 [62/208] Invoking muslc build system ninja: build stopped: subcommand failed. I am wondering if you got the similar issues or have any idea for this problem? Thanks, Zhonghao

1 0

KataOS modifications to seL4
by Isaac Beckett 23 Mar '23

23 Mar '23

> Message: 1 > Date: Tue, 21 Mar 2023 10:52:40 -0500 > From: June Tate-Gans (ジューン) <jtgans(a)google.com> > Subject: [seL4] Bitfield generator EBNF grammar > To: devel <devel(a)sel4.systems> > Message-ID: > <CAOPTAH0q0UABvFhffnmJ6ygDuPmpf8fMjxBawmYbhCjjJT8MTA(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > > Hey guys, > > I've been attempting to put together some rust bindings for the seL4 fault > handling mechanisms, and I'm afraid the bitfield generator is driving me a > bit up a wall at this point. I'd like to find a concise grammar for the > language so I can better understand how bitfield_gen.py works, but there > doesn't seem to be any explicit BNF for it anywhere. > > Is there a paper I should be reading or a reference guide somewhere that > would help? > > Thanks! > > -- > June Tate-Gans > Software Engineer > Techlead, Kata OS / AmbiML, Google Hello June, I have a question about something I read on the announcement post for KataOS: > The current GitHub release includes most of the KataOS core pieces, including the frameworks we use for Rust (such as the sel4-sys crate, which provides seL4 syscall APIs), an alternate rootserver written in Rust (needed for dynamic system-wide memory management), and the kernel modifications to seL4 that can reclaim the memory used by the rootserver. And we've collaborated with Antmicro to enable GDB debugging and simulation for our target hardware with Renode. Are these changes being formally verified? I understand it involves a not insignificant amount of labor to do so, but I worry about bugs being introduced that undermine the security properties of seL4 if care isn’t taken here. Thanks, Isaac Beckett PS: I decided to post this to the mailing list because I thought it may be of interest to some folks here.

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 20 Mar '23

20 Mar '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Mar 21, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 22, 8am * Central Europe: Tue, Mar 21, 10pm * US Pacific Time: Tue, Mar 21, 2pm Calendar link: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

shoehorn & fudge factor
by Sam Leffler 14 Mar '23

14 Mar '23

I have a target platform with only 4M of memory. When the system image is generated and the shoehorn helper script is used to find a place in memory to load the build artifacts it tacks on an extra 4M of memory use (aka fudge_factor). The comment in the code <https://github.com/AmbiML/sparrow-seL4_tools/blame/master/cmake-tool/helper…> says this is to accommodate sel4test_driver. Needless to say this breaks on my 4M target platform. So I made the fudge-factor settable from the cmd line with a default of 0 and changed the sel4test build glue to set 4M when building elfloader. Works fine for my target platform. But this change breaks building a bootable image for rpi3 (AARCH64=1 bcm28367)--shoehorn places elfloader s.t. it overlaps the image; e.g. ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 > paddr=[335000..51a0ff] > No DTB passed in from boot loader. > Looking for DTB in CPIO archive...found at 378778. > Loaded DTB from 378778. > paddr=[237000..23afff] > ELF-loading image 'kernel' to 0 > paddr=[0..236fff] > vaddr=[ffffff8000000000..ffffff8000236fff] > virt_entry=ffffff8000000000 > ELF-loading image 'capdl-loader' to 23b000 > paddr=[23b000..33bfff] > vaddr=[400000..500fff] > virt_entry=4009a8 > ERROR: image load address overlaps with ELF-loader! > ERROR: Physical address range invalid > ERROR: Could not load user image ELF Debug output of shoehorn for this case: shoehorn: debug: found CPIO identifying sequence b'070701' at offset 0x40 > in > /usr/local/google/home/sleffler/shodan/out/cantrip/aarch64-unknown-elf/release/elfloader/archive.o > shoehorn: debug: encountered CPIO entry name: kernel.elf > shoehorn: debug: encountered CPIO entry name: kernel.dtb > shoehorn: debug: encountered CPIO entry name: capdl-loader > shoehorn: debug: setting marker to 0x0 (region 0 start) > shoehorn: debug: setting marker to 0x237000 (kernel_end) > shoehorn: debug: setting marker to 0x23b000 (dtb_end) > shoehorn: debug: setting marker to 0x335000 (end of rootserver) So two questions: 1. Where is the 4M under-count of sel4test_driver? (the code indicates this might be explained in JIRA SELFOUR-2335 but I couldn't locate it) 2. Should zero'ing fudge_factor work? If yes, where should I look to remedy the above? I looked upstream for changes that might address this issue but didn't see anything. I suspect I can invert my logic and default fudge_factor to some value and then override as needed (e.g. 0 for my sparrow platform & 4M for sel4test builds). -Sam

3 5

memory zero'ing
by Sam Leffler 12 Mar '23

12 Mar '23

I'm chasing an issue that looks like retype'd memory has nonsense data. If I read the kernel code correctly it looks like the object returned by an seL4_UntypeRetype syscall should be zero'd (looks to happen when an untyped memory object is reset here <https://github.com/seL4/seL4/blob/master/src/object/untyped.c#L254>). Is that correct? I don't see anything called out in the manual. -Sam

6 9

Reminder seL4 developer hangout
by Birgit Brecknell 06 Mar '23

06 Mar '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Mar 8, 6am (UTC), Topics: (open) * Sydney: Wed, Mar 8, 5pm * Central Europe: Wed, Mar 8, 7am * US Pacific Time: Tue, Mar 7, 10pm Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

UnknownSyscall Exception Handler for non-seL4 syscall API
by lukas-graber＠protonmail.com 28 Feb '23

28 Feb '23

Hello, I am working on a syscall handler in user-space and want to implement a trap-and-emulate like mechanism. Firstly, some background information and motivation. I see that the seL4 system call API uses negative syscall numbers. This allows me theoretically to use positive syscall numbers to implement an additional syscall API. The seL4 kernel triggers an UnknownSyscall Exception whenever it encounters different syscalls and leads it to the fault handler endpoint in user space of the corresponding CAmkES component. I work with CAmkES and was able to create a fault handler similar to the one implemented in GDBMem with the help of templates. I am generally able to catch the exception in a thread in the same component and get the corresponding arguments. What I don't seem to manage is redirecting the program flow of the control thread so that we return to right after the faulting syscall instruction (should be faultIP + 2). It generally just retriggers the same exception or a different one (the VMFault exception). To better understand what I did, I quickly provide the code: - My C code: Triggers the system call number 60 with 6 arguments: ```bash int run(void) { while(1){ register int rax __asm__ ("rax") = 60; register int rdi __asm__("rdi") = 1; register int rsi __asm__("rsi") = 2; register int rdx __asm__("rdx") = 3; register int r10 __asm__("r10") = 4; register int r8 __asm__("r8") = 5; register int r9 __asm__("r9") = 6; __asm__ __volatile__ ( "syscall" : "+r" (rax) : "r" (rdi), "r" (rsi), "r" (rdx), "r" (r10), "r" (r8), "r" (r9) : "rcx", "r11", "memory"); printf("After the syscall instruction!\n"); } } ``` - My CAmkES code: We connect two threads of the component CompA, the faultIn thread is related to the From Template, the faultOut thread is related to the To template. ```bash connector camkesFaultHandlerThread { from Procedure; to Procedure; } procedure CAmkES_FaultHandlerThread { void bla(); } component CompA { control; uses CAmkES_FaultHandlerThread faultIn; provides CAmkES_FaultHandlerThread faultOut; } assembly { composition { component CompA compA; connection camkesFaultHandlerThread fault0 (from compA.faultIn, to compA.faultOut); } } ``` - The to Template: gets triggered with every fault, should handle the system call and then redirect program flow ```bash /*- set fault_ep = alloc("fault", seL4_EndpointObject, read=True, write=True, grantreply=True) -*/ /*- set info = c_symbol('info') -*/ int /*? me.interface.name ?*/__run(void) { seL4_Word fault_type; seL4_Word length; seL4_Word delegate_tcb; seL4_UserContext regs; seL4_MessageInfo_t info; while (1) { info = seL4_Recv(/*? fault_ep ?*/, &delegate_tcb); seL4_Fault_t fault = seL4_getFault(info); fault_type = seL4_MessageInfo_get_label(info); if(fault_type == seL4_Fault_UnknownSyscall){ printf("faulting PC: %zx\n",seL4_Fault_UnknownSyscall_get_FaultIP(fault)); //handle the syscall ... length = seL4_MessageInfo_get_length(info); seL4_TCB_ReadRegisters(delegate_tcb, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs); // Which registers should I set for the faultIn thread?, right now simply jump over the syscall instruction regs.rip += 2; // Write registers back seL4_TCB_WriteRegisters(delegate_tcb, false, 0, sizeof(seL4_UserContext) / sizeof(seL4_Word), &regs); // Resume the caller seL4_MessageInfo_t info = seL4_MessageInfo_new(0, 0, 0, length); seL4_Reply(info); } else if(fault_type = seL4_Fault_VMFault){ // Why do we get in here after replying to UnknownSyscallException? } } } ``` I simply want to handle the UnknownSyscall Exception (in the faultOut thread) and then return to the instruction right after the original syscall in the control thread. But no matter how I change the IP, it just retriggers the exception or causes a VM Fault Exception. I see that there is a NextIP virtual register field in kernel/include/arch/x86/arch/64/mode/machine/registerset.h. Can I somehow set this one from userspace with setRegister? Has anyone ever tried something similar? Help would be very much appreciated. Thank you very much! Kind Regards, Lukas

2 2

Slowpath IPC mechanism
by mincheol＠vt.edu 22 Feb '23

22 Feb '23

Hi, I am wondering how the slowpath IPC mechanism works. Does it use shared memory to transfer the IPC message?

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 21 Feb '23

21 Feb '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Feb 21, 9pm (UTC), Topics: (open) * Sydney: Wed, Feb 22, 8am * Central Europe: Tue, Feb 21, 10pm * US Pacific Time: Tue, Feb 21, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

2 1

Re: U-boot for Raspberry PI
by Michal Podhradsky 08 Feb '23

08 Feb '23

Hello, thank you for prompt replies! I used the default U-boot, however now I am stuck in the next phase of booting - specifically loading and booting the sel4 test image. Following the instructions in the docs ( https://docs.sel4.systems/Hardware/Rpi4.html) I do: *U-Boot> fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711** Reading file would overwrite reserved memory **Failed to load 'sel4test-driver-image-arm-bcm2711* Which is odd. Perhaps the memory map on Rpi has changed recently? Picking another memory location gets me further (although it is unclear that it is a correct location): *U-Boot> fatload mmc 0 0x00008000 sel4test-driver-image-arm-bcm27115164988 bytes read in 235 ms (21 MiB/s)U-Boot> bootefi 0x00008000* Now, the image gets loaded but the boot fails with an seL4 assertion fail: *U-Boot> bootefi 0x00008000Card did not respond to voltage select! : -110No EFI system partitionBooting /sel4test-driver-image-arm-bcm2711ELF-loader started on CPU: ARM Ltd. Cortex-A72 r0p3 paddr=[6603000..ffffffffffffffff] dtb=6af2000Looking for DTB in CPIO archive...found at 674d958.Loaded DTB from 674d958. paddr=[123f000..1245fff]ELF-loading image 'kernel' to 1000000 paddr=[1000000..123efff] vaddr=[ffffff8001000000..ffffff800123efff] virt_entry=ffffff8001000000ELF-loading image 'sel4test-driver' to 1246000 paddr=[1246000..164bfff] vaddr=[400000..805fff] virt_entry=40ef20Enabling MMU and pagingJumping to kernel-image entry point...Bootstrapping kernelavailable phys memory regions: 3 [1000000..3b400000] [40000000..fc000000] [100000000..200000000]reserved virt address space regions: 3 [ffffff8001000000..ffffff800123f000] [ffffff800123f000..ffffff800124556b] [ffffff8001246000..ffffff800164c000]Booting all finished, dropped to user spaceseL4 failed assertion 'isSchedulable(candidate)' at /tmp/kernel/src/kernel/thread.c:371 in function schedulehalting...Kernel entry via Interrupt, irq 0* Any suggestions what am I missing? Regards Michal On Thu, Jan 19, 2023 at 5:53 PM Sudvarg, Marion <msudvarg(a)wustl.edu> wrote: > I have a version of U-boot that works. I would have to go back through > piles of notes to see what I did to make it work, but I can share the file > with you if it's helpful. > > I also had to change config.txt to set the GPU and coprocessor frequency > to a fixed value; I had issues with boot (which is handled by the GPU) and > UART without that. > > Happy to help with the process if you like. > > Marion Sudvarg > Washington University in St. Louis > > -----Original Message----- > From: mpodhradsky(a)galois.com <mpodhradsky(a)galois.com> > Sent: Thursday, January 19, 2023 7:02 PM > To: devel(a)sel4.systems > Subject: [seL4] U-boot for Raspberry PI > > Hello! > > The instructions for building seL4 for Raspberry Pi 3 and 4 mention ask > for a custom compiled U-boot. The note mentions that an automatic revert of > the specified commit no longer works. Is this patched U-boot still > necessary, or will a vanilla version work? If the customization is still > needed, do you have a modified version available? It is not clear how to > modify the recent U-boot, since it has changed significantly. > > Regards > Michal > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems To unsubscribe send an email to > devel-leave(a)sel4.systems >

4 5

Reminder seL4 developer hangout
by Birgit Brecknell 06 Feb '23

06 Feb '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Feb 8, 6am (UTC), Topics: (open) * Sydney: Wed, Feb 8, 5pm * Central Europe: Wed, Feb 8, 7am * US Pacific Time: Tue, Feb 7, 10pm Calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

kernel builds w/ different memory configurations
by Sam Leffler 27 Jan '23

27 Jan '23

I have a target platform w/ 2 pre-defined memory configs. I've created separate .dts files w/ the different memory sizes and then in src/plat/sparrow/config.cmake do: if(KernelDebugBuild) list(APPEND KernelDTSList "tools/dts/sparrow-debug.dts") else() list(APPEND KernelDTSList "tools/dts/sparrow.dts") Overloading KernelDebugBuild is awkward (it seems contrary to it's purpose) and fragile. How is this handled for existing platforms? -Sam

2 2

help with Nvidia Jetson Xavier port
by Axel Heider 27 Jan '23

27 Jan '23

Hi, we are working on porting seL4 to the Nvidia Jetson Xavier. The kernel is booting, but then there are random crashes in user mode where the cores seem to stop completely within a minute, no crash output is visible. Our test applications are just doing some integer number crunching to create load, there are no drivers involved (besides a bit of UART output). It looks like this also happened to others, a similar problem was described in this post: https://forums.developer.nvidia.com/t/illegal-instruction-with-i-cache-disa… Did anybody get seL4 userland running stable there? Axel

1 0

Inquiry to Verified Components
by Seoyeon Hwang 26 Jan '23

26 Jan '23

Hello, From this document https://apps.dtic.mil/sti/pdfs/AD1027690.pdf <https://urldefense.com/v3/__https://apps.dtic.mil/sti/pdfs/AD1027690.pdf__;…>, we figured out that system call APIs are verified (except for their composition with sel4 kernel proofs). However, we are not sure whether other process/thread-spawning APIs are also verified. We use the APIs (listed below) in our project, hoping to develop a formally verified root-of-trust architecture atop seL4. Could you let us know if they are all verified, and if so, could you also point out the resources we can cite in our paper? Thanks, Seoyeon APIs used in our projects are: Initial Process-related APIs platsupport_get_bootinfo simple_default_init_bootinfo bootstrap_use_current_simple allocman_make_vka simple_get_cnode simple_get_pd Thread Spawning APIs vka_alloc_tcb vka_alloc_frame seL4_ARCH_Page_Map vka_alloc_page_table seL4_ARCH_PageTable_Map vka_alloc_endpoint vka_mint_object seL4_TCB_Configure seL4_TCB_SetPriority sel4utils_set_instruction_pointer sel4utils_set_stack_pointer seL4_TCB_WriteRegisters sel4runtime_write_tls_image sel4runtime_set_tls_variable seL4_TCB_SetTLSBase seL4_TCB_Resume Process Spawning APIs sel4utils_bootstrap_vspace_with_bootinfo_leaky vspace_reserve_range bootstrap_configure_virtual_pool process_config_default_simple sel4utils_configure_process_custom vka_cspace_make_path sel4utils_mint_cap_to_process sel4utils_create_word_args sel4utils_spawn_process_v IPC/System call APIs seL4_MessageInfo_new seL4_MessageInfo_get_length seL4_SetMR seL4_GetMR seL4_Call seL4_Recv seL4_Reply seL4_Wait seL4_Yield

7 10

sel4test:nested timeout fault test flaky?
by Sam Leffler 25 Jan '23

25 Jan '23

We run sel4test regularly for a 64-bit raspi target under qemu and occasionally see failures like this: Starting test 129: TIMEOUTFAULT0003 > Running test TIMEOUTFAULT0003 (Nested timeout fault) > Error: Check badge(3) == expected_badge(2) failed. at line 9 This is a stock sel4test <https://github.com/AmbiML/sparrow-sel4test> + dep libs but an older kernel <https://github.com/AmbiML/sparrow-kernel>. Anyone know if this is an old (presumably fixed) bug or known issue? -Sam

3 5

Reminder seL4 developer hangout
by Birgit Brecknell 25 Jan '23

25 Jan '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Jan 24, 9pm (UTC), Topics: (open) * Sydney: Wed, Jan 25, 8am * Central Europe: Tue, Jan 24, 10pm * US Pacific Time: Tue, Jan 24, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

Sel4 on RISC-V AllwinnerD1 MangoPi MQ1PH boot problem
by alex＠nixd.org 19 Jan '23

19 Jan '23

Hello, I just have a small question because I found the documentation about booting the Sel4 on RISC-V systems a bit confusing and not answering my questions. 1) I have ported all necessary code and I have successful compiled the `sel4test`. 2) I have flashed a SPL and U-Boot to 'mmc' which was built including OpenSBI fw_dynamic.bin but against most recent version (Sel4 was also compiled against most recent version OpenSBI v1.2 U-Boot SPL 2022.10-38338-g528ae9bc6c-dirty (Jan 11 2023 - 01:07:54 +0100)). 3) SPL and U-boot runs perfectly. 4) Sel4 does not want to boot. Why? So, in the DTS which I extracted from SDK it is said: ` /memreserve/ 0x40000000 0x200000; /* opensbi */ /memreserve/ 0x42000000 0x100000; /* dsp used 1MB */ memory@40000000 { device_type = "memory"; reg = <0x0 0x40000000 0x0 0x8000000>; }; ` For the elfloader objdump reports the `_start at 0x40a21000` so I hardcoded it into the following #define CONFIG_BOOTCOMMAND \ "if mmc rescan; then " \ "echo SD/MMC found on device ${mmc_dev};" \ "fatload mmc 0 0x40a21000 elfloader;" \ "fatload mmc 0 0x40a27940 archive.archive.o.cpio;" \ "bootelf 0x40a21000;" \ "fi;" \ And it reported an error: "Unhandled exception: Load access fault EPC: 000000007ffbd308 RA: 000000007ffbd33a TVAL: 00000005c66db5aa EPC: 0000000042e50308 RA: 0000000042e5033a reloc adjusted Code: 69a2 6145 8082 7480 1793 0069 9426 943e (641c) resetting ..." It seems that it relocates itself to 42e5033a (or not?) what actually I was trying to do manually. U-boot reports (for the domain0) the next address which is 0x0000000042e00000. And when I am loading elfloader there, it exists back to uboot shell without any errors and nothing happens. I can not understand what I am doing wrong, because FreeBSD and Linux starts normally. The #define seL4_UserTop is generated from DTS file if I understood correctly. But it seems it is incorrect. I will be happy for any hint. Thank you.

3 2

Can I launch two rumprun instances at the same time?
by mincheol＠vt.edu 06 Jan '23

06 Jan '23

Hi, I am trying to run two rumprun instances on seL4. I called launch_process(bin_name, CONFIG_RUMPRUN_COMMAND_LINE, 1); launch_process(bin_name, CONFIG_RUMPRUN_COMMAND_LINE, 2); in run_rr() of rumprun-sel4-demoapps/roottask/src/main.c. Then I got below: <<seL4(CPU 0) [decodeCNodeInvocation/107 T0xffffff801fe14400 "roottask" @4166c1]: CNode Copy/Mint/Move/Mutate: Source slot invalid o> sel4utils_move_cap_to_process@process.c:157 Failed to move cap <<seL4(CPU 0) [decodeX86PortControlInvocation/147 T0xffffff801fe14400 "roottask" @451efa]: IOPortControl: Some ports in range alread> arch_copy_IOPort_cap@arch.c:25 Failed to get IO port cap for range cf8 to cff I don't understand why I got these errors. launch_process() gets rump_process_t *process from process_from_id(id) so I should get a different slot with the different process id.

1 0

Question about non-blocking notification
by mincheol＠vt.edu 31 Dec '22

31 Dec '22

Hi, Do I need to use seL4-NBSend() for sending a non-blocking signal (cause seL4_Signal() is blocking)?

3 5

Question about sel4-tutorial dynamic-2 and dynamic-3
by mincheol＠vt.edu 29 Dec '22

29 Dec '22

Hi, I have two questions regarding dynamic-2 and dynamic-3 tutorials. 1. In dynamic-2 TASK 4, Why is the ipc_buffer_vaddr put in seL4_ARCH_PageTable_Map()? ipc_buffer_vaddr is the virtual address of the new physical frame allocated for the IPC buffer. I think seL4_ARCH_PageTable_Map's 3rd parameter is the virtual address of the page table frame. 2. In dynamic-3, it uses sel4utils_configure_process_custom() to create a new thread. I looked into the function and found that it created a vspace for the new thread. However, the tutorial's learning outcomes section says "this time the two threads will only share the same vspace", so I am confused. Does this tutorial create a new vspace for the new thread? Mincheol

2 2

Any reliable way to determine if a thread is suspended?
by Andrew Warkentin 28 Dec '22

28 Dec '22

Is there any reliable way to determine if a thread is suspended? seL4_TCB_Suspend() succeeds even if the thread was already suspended. I can force all calls to seL4_TCB_Suspend() and seL4_TCB_Resume() to go through a wrapper that updates a user-level flag (since my OS manages pretty much all capabilities in the root server and will only expose TCBs to regular user processes through a special filesystem); however, this leaves a race when a thread is suspended due to a fault instead of an API call (since the thread will already be suspended before the fault handler updates the "thread running" flag). My initial use for checking if a thread is running is to allow easy atomic updates of some metadata (shared between the root server and the non-root thread, and optionally shared between threads) for my IPC transport layer that implements Unix-like file descriptors on top of seL4 endpoints (and eventually notifications). To add an FD to a thread's list, the root server allocates a copy of the endpoint (and reply if the FD is server-side) into the thread's CSpace, suspends the thread, updates the metadata (which includes the underlying capabilities), and then resumes the thread if it was running. Obviously, I don't want to resume threads that weren't running in the first place. I don't want to use locks here since the root server can't trust regular user processes. Another use is to allow cancelling any in-progress transfers on FDs when they get closed and returning a status to the waiting threads, which I am planning to do by replacing the endpoint with a copy of a global "clunk endpoint" associated with a thread that repeatedly sends a "file descriptor closed" message (actually there will be two such threads - one for clients, and one for servers) and then resuming the thread.

1 0

problem Ethdriver 82574 on Qemu X86_64
by reza yazdanparast 25 Dec '22

25 Dec '22

Hi. I'm working on a new camkes-based project. This project is simulated by using Qemu, on a Q35 machine for X86_64 arch and e1000e eth. I am using an intel controller driver (82574 controller) for network communication. My project has been built successfully and the intel network driver has been initialized. But when using the network in my application in Qemu, no network packet is sent and received! Qemu command: ``` sudo qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu host, -netdev tap,id=netdev0,ifname=tap0,script=no,downscript=no -device e1000e,id=nic0,netdev=netdev0,mac=52:55:00:d1:55:01 -nographic -serial mon:stdio -m size=4G -device intel-iommu -kernel ./target/debug/images/kernel-x86_64-pc99 -initrd ./target/debug/images/capdl-loader-image-x86_64-pc99 ``` . Appendix: Create tap0 command: ``` export TAP_DEV=tap0 sudo ip tuntap add dev $TAP_DEV mode tap sudo ip addr flush dev $TAP_DEV sudo ip addr add 10.10.100.1/24 brd 10.10.100.255 dev $TAP_DEV sudo ip link set dev $TAP_DEV addr 02:00:ca:fe:01 sudo ip link set dev $TAP_DEV up ``` . how to fix this problem? Thank you.

1 0

any fun holiday hacks with sel4?
by ember arlynx 25 Dec '22

25 Dec '22

merry christmas :) i've been thinking about reviving some rusty robigalia-ish things. how are you all doing, this stormy sunday? -- ember

1 0

next seL4 TSC meeting on Fri 16 Dec (15 Dec in US and Europe)
by Gerwin Klein 16 Dec '22

16 Dec '22

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: - Sydney: Fri, 16 Dec, 8am - Central Europe: Tue, 15 Dec, 10pm - US West Coast: Tue, 15 Dec, 1pm See also the seL4 calendar feed available from here: https://sel4.systems/contact/home.pml The meeting is by Zoom, and you can join from here: https://unsw.zoom.us/j/5510249963 Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: - election (or re-election) of TSC chair - split C-Parser/AutoCorres out from l4v repository - RFCs: - SMC https://sel4.atlassian.net/browse/RFC-9 - MCS: Improve constraints on grant via reply https://sel4.atlassian.net/browse/RFC-13 - MCS: set fault and timeout handler parameters while configuring TCBs https://sel4.atlassian.net/browse/RFC-11 - The seL4 Core Platform https://sel4.atlassian.net/browse/RFC-5 - The seL4 Device Driver Framework https://sel4.atlassian.net/browse/RFC-12 - Ability to build additional bootloaders inside the seL4 build system https://sel4.atlassian.net/browse/RFC-4 - SIG chair nominations - discuss process for establishing SIGs If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

1 1

Reminder seL4 developer hangout
by Birgit Brecknell 12 Dec '22

12 Dec '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Dec 14, 6am (UTC), Topics: (open) * Sydney: Wed, Dec 14, 5pm * Central Europe: Wed, Dec 14, 7am * US Pacific Time: Tue, Dec 13, 10pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Call for nominations for Special Interest Group Chairs
by Gerwin Klein 05 Dec '22

05 Dec '22

At this year's seL4 summit the community expressed strong interest in starting a number of special interest groups (SIGs) around seL4 and in particular around the following topics: - Virtual machines and virtual machine monitors (SIG VMM) - Drivers (SIG Drivers) - Multicore design + verification (SIG Multicore) The multicore verification topic also showed large overlap with interest in user-level verification at the summit. One suggestion would be to cover both topics in that SIG. To start these SIGs, we are calling for the nomation of a chair for each of them. Anyone can nominate anyone from the seL4 community, including themselves. If there is more than one nomination who is willing to do the job for a specific SIG, we will organise a vote and if possible appoint a chair + vice-chair (for backup). The appointement will be confirmed by the technical steering committee TSC. The main job of the chair of a SIG will be (lightweight) moderatation, keeping the conversation going, and to be a point of contact with the TSC. An initial task for the chair would be to lead the discussion on what the SIG will be about in more detail and what it wants to achieve. Examples could be: - to coordinate concrete work - to discuss the topic of the SIG - to make recommendations to the TSC - to work together on RFCs on the topic of the SIG This should result in a short description that we can use on the seL4 website and discourse groups for the SIG to describe what its purpose is. We suggest that the main communciation medium for SIGs be the seL4 discourse forum, where each SIG could have its own topic area, but we are happy for SIGs to self-organise differently if they prefer. Please send nominations to Gerwin Klein <kleing(a)unsw.edu.au>. Please indicate which SIG they are for. Cheers, Gerwin (seL4 TSC chair)

1 0

[FOSDEM'23] Submit talk for the "Microkernel and Component-based OS" devroom
by Razvan Deaconescu 05 Dec '22

05 Dec '22

Hi. I am Razvan Deaconescu, I'm from University POLITEHNICA of Bucharest (working on Unikraft unikernel) and I'm managing the "Microkernel and Component-based OS" devroom[2] at FOSDEM'2023[1]. The devroom will take place in person, at FOSDEM'23, in Brussels, on Sunday, February 5, 2023. If you have an interesting topic to talk about it would be great if you made a submission. This is something easy to do, takes about 15-20 minutes on Pentabarf[3]. The deadline for submission is today, Friday, December 2, 2022. [1] https://fosdem.org/2023/ [2] https://fosdem.org/2023/schedule/track/microkernel_and_component_based_os/ [3] https://penta.fosdem.org/submission/ Razvan

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 28 Nov '22

28 Nov '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Nov 29, 9pm (UTC), Topics: (open) * Sydney: Wed, Nov 30, 8am * Central Europe: Tue, Nov 29, 10pm * US Pacific Time: Tue, Nov 29, 1pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Survey about the seL4 summit 2023's location
by June Andronick (seL4 Foundation) 21 Nov '22

21 Nov '22

Dear seL4 friends, With the great success of the seL4 summit 2022 behind us, we are now already looking at the seL4 summit 2023! This should happen around Sep/Oct 2023. We have started investigating options for the location, and we would like your feedback. We would very much appreciate if you could fill in this very short survey to tell us your opinion between USA (likely Minneapolis) and Australia (likely Sydney) or any other feedback you have: https://forms.gle/k4XxYaYeudYUie9U8 <https://forms.gle/k4XxYaYeudYUie9U8> Please do so by Nov 22nd 2022. Feel free to forward to anyone you believe may want to attend the summit next year. Many thanks! June -- June Andronick CEO of the seL4 Foundation https://sel4.systems/Foundation

1 1

Experimental project on seL4 microbenchmarking
by Nataliya Korovkina 20 Nov '22

20 Nov '22

Hi seL4 friends, I’d like to share an experimental project on seL4 microbenchmarking inspired with my experience with sel4bench suite. Your thoughts on the concept and its practical use will be greatly appreciated. Motivation (informal) Measuring execution times of short code paths, which we can meet in seL4 microbenchmarking, is a good way to immerse oneself into the domain of compiler and microarchitectural optimizations. Implementation of “early processing” measurement methodology in sel4bench suite (for Notification delivery case, as a trial step; PR #26) was an amazing experience in that respect. So, I gladly share the work highlights to explain my motivation. First, latencies of some microarchitectural events can be comparable with execution time of a measured code path. So, if microarchitectural event not planned by a benchmark design happens during a measuring period, deviation of the observed value considerably increases. Second, the both kinds of optimizations of instrumental code cause instability of measured values from one measurement iteration to another. Third, debugging the instrumental code is very challenging. Injection of diagnostic code into it changes effects of the both types of optimizations; therefore, initially witnessed symptoms effectively transform to other ones. When you think about how to control optimizations effects, the situation appears uninspiring, considering the need to treat various microarchitectures and optimization features. As a result, the situation left me with the question on hands: how to distance a benchmark design from necessity to control optimizations effects in instrumental code that impair repeatability? Eventually, it reduced to the foundational one: What we measure, and Why? This experimental work is attempt to find and try the solution for the challenge: designing more predictable measurement context. The work was published in github. Description paper https://github.com/malus-brandywine/sel4KanataBench-papers/blob/main/Kanata… Project repository https://github.com/malus-brandywine/sel4KanataBench Project manifest repository https://github.com/malus-brandywine/sel4KanataBench-manifest Tables of data collected on four TS platforms: files KBenchTable-xxxx.pdf in https://github.com/malus-brandywine/sel4KanataBench-papers Thank you!

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 14 Nov '22

14 Nov '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Nov 16, 6am (UTC), Topics: (open) * Sydney: Wed, Nov 16, 5pm * Central Europe: Wed, Nov 16, 7am * US Pacific Time: Tue, Nov 15, 10pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 31 Oct '22

31 Oct '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Nov 1, 9pm (UTC), Topics: (open) * Sydney: Wed, Nov 2, 8am * Central Europe: Tue, Nov 1, 10pm * US Pacific Time: Tue, Nov 1, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Cross Core IPC
by Sid Agrawal 24 Oct '22

24 Oct '22

Hi, I came across Gernot Heiser's blog post on "How to use seL4 IPC" [1]. The article explicitly says that doing cross-core IPC is a bad idea. This statement led to a series of questions for me, which I hope you guys can help me with. Scenario ------------ We have a system with two cores. Let's say that a physical memory server is running on core0, my application is on core1, and they are somehow pinned to those cores. The application wants some physical memory (frame capabilities) from the memory server. Questions ------------- Q1. Will the application be able to invoke the endpoint given that the TCB which will respond to it is on a separate core? If yes, will sending a capability back via cross-core IPC be allowed? I did not read anything in the manual which said otherwise. Q2. Why is a cross-core IPC a bad idea? This might be a loaded question, but I am not able to appreciate the badness of the idea :) Q3. What would be the right way to do it? For example, in Barrelfish(limited experience from a course), the application(on core1) would make an IPC to a monitor running on the same core1. This monitor did synchronization with another monitor running on the other core(core0) via a shared memory region (all in user space). That monitor(core0) then sent an IPC to the memory server running on core0. And then back again via the monitors. Best, Sid [1] https://microkerneldude.org/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/

3 2

Suitability for a project
by James Hillman 19 Oct '22

19 Oct '22

Hi Sel4 developers, I am new to this forum and hoping this is the right place to bounce my project idea off. I typically use FPGA to enforce security in my products but there are lots of reasons why FPGAs are not suitable for all use cases. I have also used low end microcontroller where one can review all the code to understand the security risks. My latest project however involves two USB processes (one for each physical connection) with high throughput expectations. And to pass data streams at high typical throughput between them. Due to the wide range of USB type of devices I fear this would be too much code to review - it feels very OS like. Note, I don't need a GUI, it's headless. So I'm interested in sel4 as I could run the processes in Linux VMs if I understand sel4 correctly. And whilst it's not the smallest processors I think they need to be more powerful to support the speeds. So this is fine . I am unsure how much of this project is already done, mainly thinking the usb driver perspective. Thanks in advance, Best wishes James

5 10

new RFC: seL4 Device Driver Framework
by Gerwin Klein 19 Oct '22

19 Oct '22

A new RFC has just landed: https://sel4.atlassian.net/browse/RFC-12 If you have any feedback, please comment there. Cheers, Gerwin

8 16

Re: Suitability for a project
by James Hillman 19 Oct '22

19 Oct '22

Thanks Gernot. Thoughts on throughput rates thats might be achieved?

1 0

Re: Suitability for a project
by James Hillman 19 Oct '22

19 Oct '22

I was interested to see the Google news re. KataOS which I suspect confirms that my sort of requirement / entry point is someway out. I was also reading about ARM Morello / CHERI work. Although I appreciate this is taking a different, perhaps flawed, path of some new hardware memory protection. Appreciate any feedback you can humour me with.

2 1

seL4 dev hangout reminder
by Gerwin Klein 17 Oct '22

17 Oct '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Oct 19, 6am (UTC), Topics: (open) * Sydney: Wed, Oct 19, 5pm * Central Europe: Wed, Oct 19, 8am * US Pacific Time: Tue, Oct 18, 11pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Devel Digest, Vol 171, Issue 3
by Isaac Beckett 08 Oct '22

08 Oct '22

> From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] new RFC: seL4 Device Driver Framework > To: sel4 <devel(a)sel4.systems> > Cc: "tsc-members(a)sel4.systems" <tsc-members(a)sel4.systems> > Message-ID: <55BB3266-24A1-488B-A623-5B912461AD7F(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > A new RFC has just landed: https://sel4.atlassian.net/browse/RFC-12 > > If you have any feedback, please comment there. > > Cheers, > Gerwin Ooh, exciting. I wonder if something similar to Mesa could be implemented for graphics, to ease porting existing Mesa drivers.

1 0

High-throughput asyncrhonous driver API?
by Andrew Warkentin 05 Oct '22

05 Oct '22

I remember talk in one of the developer hangouts I was in about a proof of concept for a high-throughput asynchronous driver layer for seL4 (presumably based on notifications). Has code for this been released anywhere? I'm going to be starting on my own IPC transport layer and I want to include asynchronous message passing as an option.

1 0

Device pass-through in qemu-qrm-virt
by ybbekele＠aggies.ncat.edu 03 Oct '22

03 Oct '22

Hello I am trying to do a device pass-through for a qemu-arm-virt implementation of seL4. Although there are no resources on how to do it on ARM, I followed the procedures for x86 found here [1]. There are differences between the two architectural implementations thus can't be successful. I tried to pass the image as an argument to Simulate, parser.add_argument('--extra-qemu-args', dest='qemu_sim_extra_args', type=str, help="Additional arguments to pass onto QEMU", default="-device virtio-blk-pci,drive=drive0 -drive file=/****/***/****/projects/camkes-vm-images/qemu-arm-virt/sdcard.img,format=raw,if=none,id=drive0") The machine can start successfully, but it keeps dropping to the initramfs and there is no sda in /dev/. Is there someone who is successful in passing through a device to qemu-arm-virt? Are there any documents to do that? Thank you [1] https://docs.sel4.systems/projects/camkes-vm/

1 0

Entry of user program
by mincheol＠vt.edu 30 Sep '22

30 Sep '22

Hi, I am trying to benchmark seL4's cross core IPC. I was able to run the IPC tutorial program and am now trying to run the server and the client on different VCPU. I found seL4_TCB_SetAffinity() but need to know the entry point of user program. Can anyone point it out for me? Mincheol

2 1

I need help with the IPC tutorial
by mincheol＠vt.edu 30 Sep '22

30 Sep '22

Hi, I can't figure out what to code in server.c for the ipc tutorial. What can I code after "// TODO use cap transfer to send the badged cap in the reply" line in the tutorial template (server.c) Can anyone share the fully working source.c?

3 3

Reminder seL4 developer hangout
by Birgit Brecknell 30 Sep '22

30 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Oct 4, 9pm (UTC), Topics: (open) * Sydney: Wed, Oct 5, 8am * Central Europe: Tue Oct 4, 11pm * US Pacific Time: Tue, Oct 4, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Raspberry Pi SMP?
by dave＠synergy.org 30 Sep '22

30 Sep '22

Hello, Is there any intent to enable SMP on the Raspberry Pi? I am using the Raspberry Pi 3B+. I'd like to be able to use all 4 CPUs. Thanks, David

2 2

Support for Sel4 Project
by simone cataldo 29 Sep '22

29 Sep '22

Good morning, We are a small test team, investigating seL4 microkernel to evaluate its use it as core component for a novel “open avionics” drone concept. Essentially, we are starting from scratch, basing ourselves on the provided tutorials such as “hello world”. We were trying to modify its source code for evaluating basic thing simple functions, basic programs and custom libraries. However, it looks like the memory allocation is static and embedded in the original project: once we increase the complexity of the program it evidently causes trouble. We have not found any documentation about how to set the memory allocation at compile time, and how to include external dependencies (i.e. static libraries). We would like to have some guideline to get us started and direction to some in-depth documentation to acquire enough knowledge to build a full project of our own. We are looking forward to hearing from you soon. Best regards, Simone CATALDO

5 5

Reminder seL4 developer hangout
by Birgit Brecknell 19 Sep '22

19 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Sep 21, 7am (UTC), Topics: (open) * Sydney: Wed, Sep 21, 5pm * Central Europe: Wed, Sep 21, 9am * US Pacific Time: Wed Sep 21, 12 midnight Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Proper seL4 APi/ABI design
by Eric Jacobs 17 Sep '22

17 Sep '22

Jumping off from the recent thread, I was curious if anyone had any thoughts about how to optimally design API's for seL4. I noticed we had a bit of info about what not to do (don't do long IPC, don't implement Posix, don't use messaging as synchronization, etc.) Are there any shining examples of what _to_ do with an API? Thanks, -Eric

5 11

Reminder seL4 developer hangout
by Birgit Brecknell 05 Sep '22

05 Sep '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Sep 6, 10pm (UTC), Topics: (open) * Sydney: Wed, Sep 7, 8am * Central Europe: Wed, Sep 7, 12 midnight * US Pacific Time: Tue, Sep 9, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

tool to report per-component memory / resource use from system.cdl
by Sam Leffler 27 Aug '22

27 Aug '22

I'm looking for a script/tool that can break down memory by component given a system.cdl file. I've been doing this by hand (sorta) but figured I should ask before doing something more organized. -Sam

1 0

Project Sparrow / KataOS Initial Open Source Release
by June Tate-Gans (ジューン) 23 Aug '22

23 Aug '22

Hey guys! Sam and I have been hard at work at releasing our source code for the Project Sparrow work we've been working on for the last year or so, and we just managed to get our first release up at < https://github.com/AmbiML/sparrow-manifest>. So, we thought we'd announce it to the devel list! A bit of background: Sparrow is a project to build an open source low-power secure embedded platform for Ambient ML applications. Our target platform leverages RISC-V and OpenTitan, and all our contributions are licensed under the Apache-2 open source license. The Sparrow software includes a home-grown operating system named KataOS, that runs on top of seL4 and is written almost entirely in Rust. We’ve pushed some foundational pieces of KataOS to GitHub together with build glue to run seL4 CAmkES test applications on a 64-bit ARM platform (running in simulation on qemu). These are intended to show the direction we’re headed and enable anyone to start building their own systems in Rust on top of seL4. This initial tranche of code includes: frameworks (e.g. the sel4-sys crate that provides seL4 syscall apis), an alternate rootserver (needed for dynamic system-wide memory management), and the kernel modifications that enable reclaiming the memory used by the rootserver. This push does not, as yet, include the CAmkES services that support dynamic loading+running of applications–that will be published as we deem it ready for sharing until eventually all of Sparrow (software and hardware designs) will be available. While we are developing for an experimental 32-bit RISC-V platform, we intend to push code that runs on aarch64 platforms. Help is welcome to make the code base run on more platforms. In the long run, we're planning on opening up everything we can, so please watch this space! -- June Tate-Gans Software Engineer Techlead, Kata OS / AmbiML, Google

4 5

Reminder seL4 developer hangout
by Birgit Brecknell 22 Aug '22

22 Aug '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Aug 24, 7am (UTC), Topics: (open) * Sydney: Wed, Aug 24, 5pm * Central Europe: Wed, Aug 24, 9am * US Pacific Time: Aug 24, 12 midnight Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: QubesOS+seL4
by Gernot Heiser 11 Aug '22

11 Aug '22

[ Redirecting this inquiry to the more appropriate ailing list] On 2 Aug 2022, at 05:55, ossgroup <ossgroup(a)protonmail.com<mailto:ossgroup@protonmail.com>> wrote: I'm interested in porting QubesOS to seL4. Is there already an initiative for this? If not, would you mind pointing me in the right direction to get started? People have been playing with this on-and-off, including a honours thesis here at UNSW years ago. The closest current activity I’m aware off is our Makatea project which, in collaboration with Swiss company Neutrality, has a (presently) more limited aim of isolating servers on a private cloud: https://trustworthy.systems/projects/TS/makatea A full Qubes port would be cool but a fair bit of work. I’d definitely like to see it done, and it’s clearly a more secure approach than having Xen (and therefore a whole Linux) in your trusted computing base. Gernot

3 2

Re: QubesOS+seL4
by Demi Marie Obenour 09 Aug '22

09 Aug '22

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512 On Mon, Aug 08, 2022 at 03:24:51PM +0200, Hugo V.C. wrote: > You are absolutely rigth Demi. Anyway, I think the point here is not to > "switch" from Xen to seL4, which is an giant task, but to start > "something", some port of QubesOS, based on seL4. Obviously, it will lack > most features, bad hardware support, etc, but I guess that as soon there's > something that can be run, the community will slowly add effort to such > project. If you remember the first versions of Linux, desktop support was > horrible... But at some point there should be people starting new > challenging stuff. I don't think we can have a QubesOS based on seL4 at > short term, but if we start now, it can be a reality in few years. I can > smell lot of interest on it... - From a Qubes OS perspective, the approach I would prefer is to first get Qubes OS working on seL4, with the control plane running in a Linux VM as it does now. This is definitely less than optimal, but it is likely the quickest way to get Qubes on seL4 working at all, and therefore the solution that is the most likely to actually be finished. Over time, more and more of the code can be replaced by native seL4 components as those components become available. For instance, the firewall is currently based on Linux, but it is a stand-alone component that already has an alternative implementation based on MirageOS. Therefore, it would be an excellent candidate for replacement with a firewall running natively on seL4. - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab -----BEGIN PGP SIGNATURE----- iQIzBAEBCgAdFiEEdodNnxM2uiJZBxxxsoi1X/+cIsEFAmLxkk0ACgkQsoi1X/+c IsH9Kg//U+FlcwVOtDXGfjJI2WCkRrLFbIC2Mvh6k1/m+f+aGtc7jvqj0xAFXxm3 JpvIYgil2LGGsdpC3dvyTH+7xqGQUVgzcYYyJDwbdRv0gBau1T+z3xkagYvOE1E8 94aEHLmvZV6GvXZ+6LdwZjkLgOQ0qnupOSkOJtmNW86tZdXC99u6cGhszejrCSG7 GzlWPaXfP7Niy16RA9QOf4nSusXvpetQwNhzTBvn1y2XrcnvitV9MNyhp23uyWMI 4VCMaA4tYbxyZdH0whQEpjrc75S2j/ewNuuiZ3VVnkOPxid0XG8UCsLGpWtoMIak /pO/JkZ25QuHAJv5ef4JpmDD5EO410vzrs70yswEb9Xcb6Fr+RnyCLmutAS1mpan zQs31KSXVOe0R5glO3p28wpkXLO80hjYrjVITnNknWv+uujHIGE1LiF8yRFaWMNa XpAUnKcTIBSqr/VkRwphBWRHkXMxKUBFbYBwV3WaUJ0fqOsGpUD4wLpLpE6N6Lb9 hRRfdM6raJ5LXNiSuheGKCh2Hxb5WejbQCH9vSCxd0Ew6j5NZf21YY84iykT47aR dO+o2XF04s4lfeBUhd8zMTSrKA6zIyAVdbtYfThT+ONXQd15YkkLWm0f7UJBCx4X kEsgYlCHXdJIQ9mkJZI4WIGRXO39sW+NCe3bs9w/YYwuVhmQKqg= =BkM1 -----END PGP SIGNATURE-----

2 4

Reminder seL4 developer hangout
by Birgit Brecknell 08 Aug '22

08 Aug '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue Aug 9, 10pm (UTC), Topics: (open) * Sydney: Wed, Aug 10, 8am * Central Europe: Wed, Aug 10, 12 midnight * US Pacific Time: Tue, Aug 9, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

section type mismatch on aarch64
by Sam Leffler 03 Aug '22

03 Aug '22

I'm building for aarch64 and hitting: /usr/local/google/home/sleffler/camkes-aarch64-rootserver/kernel/include/arch/arm/arch/64/mode/kernel/vspace.h:55:36: error: ‘mode_reserved_region’ causes a section type conflict with ‘avail_p_regs’ 55 | static const region_t BOOT_RODATA *mode_reserved_region = NULL; ... /usr/local/google/home/sleffler/camkes-aarch64-rootserver/build/kernel/gen_headers/plat/machine/devices_gen.h:67:37: note: ‘avail_p_regs’ was declared here 67 | static const p_region_t BOOT_RODATA avail_p_regs[] = { Looking at the commit history I see this commit: https://github.com/seL4/seL4/commit/680ce96b590295c1d49db6a2a34f77ac22e8475a followed by this commit: https://github.com/seL4/seL4/commit/8a87015a7c289f8bc2b5799d61e7c91482ad1cb2 I'm using gcc 11.2 from arm's prebuilt toolchain repo: https://developer.arm.com/tools-and-software/open-source-software/developer… Removing the clang band-aid fixes things. My source tree is "tracking" upstream but not directly based off it. Have I missed a change that resolves this? Is the 11.2 release just not being used yet (assuming it's a change in gcc? -Sam

3 4

Thread Scheduling Domains
by June Tate-Gans (ジューン) 02 Aug '22

02 Aug '22

Hey folks, So Sam and I are at the point now where we're attempting to get our untrusted user threads running in a different scheduling domain, and it's not exactly clear how this is supposed to work in terms of enabling more than one domain in the kernel. So far, I've set KernelNumDomains to 2 in the easy-settings.cmake for our project, but unless I provide a separate implementation of kernel/config/default_domain.c by overriding KernelDomainSchedule, the resulting kernel will only think it has one domain and only ever schedule domain 0 for execution. Are we expected to override the default_domain.c file with our own in the project, like sel4test seems to do? Thanks! -- June Tate-Gans Software Engineer

2 5

Reminder seL4 developer hangout
by Birgit Brecknell 25 Jul '22

25 Jul '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Wed, Jul 27, 7am (UTC), Topics: (open) * Sydney: Wed, Jul 27, 5pm * Central Europe: Wed, Jul 27, 9am * US Pacific Time: Wed, Jul 27, 12 midnight * Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 1

Sydney get-together on seL4 Day?
by Gernot Heiser 20 Jul '22

20 Jul '22

This is only of interest for those physically in Sydney. We have seL4 Day coming up (29 July, the 13th anniversary of completion of the seL4 verification and 8th anniversary of its open-sourcing). It would be great to use the occasion to get together. The continuing abnormal (i.e. very wet) weather in Sydney makes planning such an event difficult (and I’ll be on leave and out of town until the evening of the 28th), so things may have to happen on short notice. But weather permitting, a BYO BBQ in Maroubra would be great, and I would really love to catch up with the rest of the Sydney-based seL4 community. So I suggest people interested save the date (and let us know if you’re interested). Gernot

1 0

suggestion; update faq reference to ODROID-C2
by Van Ly 18 Jul '22

18 Jul '22

Hello, The faq section on "How can I build a system with seL4?" [1] has an obsoleted/discountinued product pointing to ODROID-C2 [2] a current product such as the one from OnLogic can replace, perhaps. [3] ``` If you have access to an Odroid-C2, you should be able to do the project work yourself as a way of familiarising yourself with seL4. ``` [1] https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html [2] https://www.hardkernel.com/shop/odroid-c2/ [3] https://www.onlogic.com/industrial-raspberry-pi/ -- vl

6 7

Systems with multiple PCI root complexes
by Peter Chubb 18 Jul '22

18 Jul '22

Has anyone extended the code in https://github.com/seL4/util_libs libpci to handle multiple root complexes? See bug https://github.com/seL4/util_libs/issues/131 I know genode added code to handle this, but they don't use that library. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

seL4 kernel memory footprint
by Sam Leffler 14 Jul '22

14 Jul '22

I'm trying to figure out the physical memory used by the kernel. This is for riscv if it matters. -Sam

4 13

sel4 smmuv2.0 on tx2 related questions
by Tao Heng 陶恒-SW 13 Jul '22

13 Jul '22

Hi sel4-devs, I have been trying to make some understandings of smmuv2.0 features provided by sel4. According to the vmm project for the tx2 platform, such as the vm_minimal apps, after all the compiling, there will be two caps,vm0_sid and vm0_cb,which is supposed to be used for stage2 address translation. My questions are as followed: 1. Which smmu device was the sid cap assigned to ? 2. How were these two caps created in the cdl file? There seems no special configuration for Cmakes that is related to the caps. 3. According to the tx2.dts, there are many sid numbers assigned to the smmu device. Why was there just one sid cap created by sel4? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 2

Anyone using capability transfer in an seL4 project? Looking for examples for research
by sjwebb＠student.unimelb.edu.au 12 Jul '22

12 Jul '22

Hi all, I'm working on a Masters research project looking into mapping an object-capability programming language onto seL4, in a way that includes some kind of mapping from the language object capabilities onto seL4's capabilities (or vice versa). I'm at a stage of the project now where it would be really helpful to have some 'motivating examples' for transferring caps between threads/CSpaces. So I was hoping I could reach out to other seL4 developers to see if they had built any systems that made extensive use of moving capabilities around. Ideally, in an ocap language, these examples would be much easier to program than they currently would be in C... The simplest example I can think of is a memory allocation server, but that wouldn't necessarily involve handing caps on beyond the one (requesting) process, which is the kind of thing I think more interesting examples would comprise of. Cheers, Stewart Webb [Masters Research student at University of Melbourne]

2 2

Re: Running RISC-V seL4 in QEMU 7.0.50
by Ahmed Charles 12 Jul '22

12 Jul '22

I'm having similar issues getting seL4test to work on riscv32/64 on QEMU 6.0.0 and 7.0.0. I tried debugging with a connected gdb, but I'm new at this and setting breakpoints in user mode seems to fail, so I'm not sure what happens once the root task starts, other than it eventually runs an infinite loop (0: j 0b, specifically). Any ideas? Thanks.

5 7

How to boot sel4 with a VGA output
by Cong Guo 12 Jul '22

12 Jul '22

Hi, I am new to sel4. I find how to run sel4test on an x86_64 machine, but with only serial output. How can I run sel4test or another sel4 system image using a normal VGA output? Thank you.

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 11 Jul '22

11 Jul '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Jul 12, 10pm (UTC), Topics: (open) * Sydney: Wed, Jul 13, 8am * Central Europe: Wed, Jul 13, midnight * US Pacific Time: Tue, Jul 12, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

How to Get Input Via Keyboard -SeL4
by Sriram 07 Jul '22

07 Jul '22

Im new to SeL4 and figuring out how to get input from a keyboard and print it as of now What api calls do I use and How to do it Thanks and Regards R.Sriram

2 1

CAmkES components for security auditing.
by Comet 06 Jul '22

06 Jul '22

Hi, Is there an existing CAmkES component that can persistently store seL4 logs for security auditing? So that I can audit data in real time. Comet

1 0

Re: seL4 on TX1
by Yiliang Wan 03 Jul '22

03 Jul '22

Hi! I encountered similar problem on TX1. I tried to boot via DFU, and get exactly the same output as @yjy from time to time. The artifacts in https://github.com/seL4/seL4/actions/runs/1715169793#artifacts are already expired. Could you please provide the latest available sel4test pre-build image for TX1. The original link for the post is： https://103.230.158.80/hyperkitty/list/devel@sel4.systems/message/P3Q5SDSPE… Thank you!

2 2

Camkes Cross VM Tutorial
by Sriram 30 Jun '22

30 Jun '22

Greetings, I have been trying to build Camkes Cross VM tutorial but it fails at the end, similarily when we boot Camkes VM Linux, We were not able to input anything from the keyboard and the Serial Output is as follows """ Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left : OK Failed to locate device consumes_event. Failed to locate device emits_event. Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done """" Is there any changes to be made in the source files or any other modifications And are there any pre-built images for x86_64 for easier implementation Keenly Awaiting for your Reply Thanks and Regards R.Sriram

1 0

Some questions about porting seL4 to CHERI(Morello)
by Sid Agrawal 29 Jun '22

29 Jun '22

Hi sel4-devs, As I had mentioned in the last developer call, I am porting seL4 to morello architecture. To be exact, I plan to run a hybrid kernel with hybrid userspace. The hybrid mode essentially means that you define CHERI capability pointers explicitly, but if not stated, everything is just a standard 64bit pointer. Based on browsing the code, I have jotted down the following list of items I need to change. 1,2 are just observations, and 3 is where I need some input. 1. Change the type of "registers" field in TCB in the kernel to store 128 bits instead of 64 bits per reg. This ties into the kernel_enter and restore_user_context code. It ensures that if a user app explicitly uses CHERI capabilities, it is not lost on a context switch.[1,2] - Done. 2. Change the syscall and IPC APIs to allow for passing CHERI caps. CHERIcaps are just 128 bits, so we should be able to pass them as arguments in IPC. The use case I have in mind is as follows - Imagine a mmap server. This server would return a VA to the caller, which in the CHERI world would be a CHERI capability. This mmap-server would allocate the memory and map it into the callee's virtual address space. Do you think this is a valid use case? 3. Update seL4_UserContext code to read and write newer regs from the user space. The seL4_UserContext struct will need to be updated to accommodate the new register DDC(default data capability reg). It will also need to be updated to accommodate 128 bit regs instead of 64 bits. This is where I ran into an issue - an assert statement in the build directory checks the size of the seL4_UserContext structure. Looks like it gets its info from the sel4arch.xml file[4]. I am not sure how to change XML processing to have it generate the correct size value for that struct. I have not created ifdef guard for morello yet, as this is just a hacky pass to get it working. My diff so far is available at [3] if anyone wants to take a look. Any help and suggestions on the approach would be greatly appreciated. Thanks, Sid [1] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/include… [2] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/include… [3] https://gitlab.com/arm-research/security/icecap/seL4/-/compare/pre-morello-… [4] https://gitlab.com/arm-research/security/icecap/seL4/-/blob/morello/libsel4…

1 0

SMP documents
by 603644559＠qq.com 23 Jun '22

23 Jun '22

I mainly want to know how threads is scheduled in SMP configuration. Is there any documents or manuals on SMP configuration?

2 1

Details on involvement of Data61/Trustworthy Systems with DARPA, esp. regarding UAVs?
by Isaac Beckett 23 Jun '22

23 Jun '22

Hello, in your answer about camkes VMs, you mentioned a collaboration with DARPA on their SMACCM/HACMS project. While seL4 is undoubtedly a good choice for mixed criticality systems like avionics on a UAV, I’m somewhat frustrated to hear y’all had done a contract for DARPA considering what they *use* those drones to do. Is there somewhere I can read more in detail about this and other military-adjacent contracts?

2 1

SeL4 Tutorial - Camkes CrossVM
by Sriram 22 Jun '22

22 Jun '22

Greetings, We have followed step by step and tried the CAMKES Linux VM tutorial, We have build it successfully but while booting via USB flash drive The Serial Output Stops after root Login and doesn't take any input SERIAL OUTPUT """ Starting network[ 0.810972] ip (679) used greatest stack depth: 6732 bytes left : OK Failed to locate device consumes_event. Failed to locate device emits_event. Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done """" This is the serial output we got Is there any modifications of the source code required to make it work if so kindly provide the necessary details. Thanks and Regards R.Sriram

1 0

How can I ensure the security of a system developed by Camkes?
by Comet 22 Jun '22

22 Jun '22

Hi, I am using Camkes to develop VM virtualization, but I have a question that is how can I ensure isolation security between virtual machines? If a virus with a Trojan is installed on the VMM, will the virtual machines attack each other? and will the kernel be corrupted ? I didn't find some security instructions about the system developed by Camkes, or the implementation principle of Camkes, that is, how is resource mapping between seL4 and Camkes? Are there any related articles? Thanks, Comet959

2 1

SeL4 Source Code Documentation
by Sriram 20 Jun '22

20 Jun '22

Greetings, We are trying to understand the SeL4 Source Code, is there any documentation available that explains the source code and libraries Thanks and Regards R.Sriram

2 2

Re: SeL4 Source Code Documentation
by Isaac Beckett 20 Jun '22

20 Jun '22

Are those Haskell sources used to generate the C code, or are they an older version of the spec, or something? This is my first time hearing of them, so not sure what they’re used for.

3 2

Page fault on starting VM
by WILLIAMS Stephen 16 Jun '22

16 Jun '22

We’re currently working on formalising VM support for an iMX8 platform (the Avnet MaaXBoard) building upon the existing sylvain/imx8 and sylvain/gicv3 branches. However on start of the VM we’re seeing the following page fault: >>>>>> Booting all finished, dropped to user space .[0m.[30;1m<<.[0m.[32mseL4(CPU 0).[0m.[30;1m [decodeUntypedInvocation/205 T0x80bf81c400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>.[0m Install gic v3 Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:652 module name: map_frame_hack install_linux_devices(a)main.c<mailto:install_linux_devices@main.c>:652 module name: init_ram libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 Waiting recv Ok -------- .[31;1mPagefault from [Linux]: read prefetch fault @ PC: 0x200 IPA: 0x200, FSR: 0x82000005 Context: x0: 0xb2000000 x1: 0x0 x2: 0xff058169ac x3: 0x3ec6 x4: 0x5527eb8 x5: 0x80000 x6: 0x58169c0 x7: 0x45dad8 x8: 0x5816a00 x9: 0x8c3a000038000000 x10: 0x1100000028000000 x11: 0x10000000 x12: 0x543a00003a040000 pc: 0x200 x14: 0x0 sp: 0x480a58 spsr: 0x3c5 x13: 0x0 x15: 0x1000000 x16: 0xb2000000 x17: 0x480a58 x18: 0x5816bd0 x19: 0x664616f6c x20: 0xb2000000 x21: 0xb0080000 x22: 0x5816a10 x23: 0x405524 x24: 0x5816ab0 x25: 0x5816a40 x26: 0x0 x27: 0xb2000000 x28: 0x480a58 x29: 0x480a50 x30: 0xc63e0000edfe0dd0 .[3.[0mm-------- main_continued(a)main.c<mailto:main_continued@main.c>:1134 Failed to run VM <<<<<< From existing reports it is my understanding that the “insufficient memory” and the “error attempting sys call 215” errors are to be expected and are not a concern; please correct me if that is not the case! Any suggestions as to the possible cause of the page fault or hints on how to progress with debugging this issue would be greatly appreciated. Thanks for your help, Stephen This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

3 5

seL4 gdb + renode support
by Sam Leffler 16 Jun '22

16 Jun '22

As I mentioned on yesterday's zoom call Antmicro has released support for debugging seL4 applications (esp CAmkES). https://antmicro.com/blog/2022/06/sel4-userspace-debugging-with-gdb-extensi… I've used it extensively and find it very useful. -Sam

2 1

Invitation: Reminder seL4 developer hangout @ Tue Jun 14, 2022 3pm - 4pm (PDT) (devel@sel4.systems)
by agrawal.sidhartha＠gmail.com 15 Jun '22

15 Jun '22

You have been invited to the following event. Title: [seL4] Reminder seL4 developer hangout - rump kernel - arm assembly question. When: Tue Jun 14, 2022 3pm – 4pm Pacific Time - Vancouver Where: https://unsw.zoom.us/j/82640784431 Calendar: devel(a)sel4.systems Who: * agrawal.sidhartha(a)gmail.com - organizer * birgit.brecknell(a)unsw.edu.au * devel(a)sel4.systems Event details: https://calendar.google.com/calendar/event?action=VIEW&eid=NWozdWplbDZwZmk3… Invitation from Google Calendar: https://calendar.google.com/calendar/ You are receiving this courtesy email at the account devel(a)sel4.systems because you are an attendee of this event. To stop receiving future updates for this event, decline this event. Alternatively you can sign up for a Google account at https://calendar.google.com/calendar/ and control your notification settings for your entire calendar. Forwarding this invitation could allow any recipient to send a response to the organizer and be added to the guest list, or invite others regardless of their own invitation status, or to modify your RSVP. Learn more at https://support.google.com/calendar/answer/37135#forwarding

3 2

Question about rumpkernel on seL4
by Sid Agrawal 15 Jun '22

15 Jun '22

Hello sel4-devs, I came across the rumprun-sel4-demo apps [1] repo. There seems to be some bitrot as the kernel version keeps moving forward, But after moving the kernel back to 12.0 and some cmake fixes, I could get many apps(LevelDB, Redis, Memcached) to compile. Though "hello" ran fine, the few others I tried failed with various errors in the simulate step(such as page faults and invalid syscall number). I plan to debug these at some point, but I had a few questions about the setup before that. 1. Is this repo considered abandoned? 2. Is the rumpkernel+app running as a Virtual Machine or as a user process in this setup? Phrased differently, is seL4 acting like an OS or a Hypervisor? 3. Is there a known effort to run another libOS on seL4, such as Unikraft? The current mental model I have for running real apps on seL4 is something like this diagram below: 3. App+LibOS(Redis + rump) ------------------------------------- 2. RootTask + other services* ------------------------------------- 1. sel4 ===================== 0. Hardware Most of my contributions would be in layer-2, i.e. (rootTask + other services). I would then want to expose these new functionalities to the libc inside layer 3. The kernel itself should be mostly untouched. Thanks, Sid [1] https://github.com/seL4/rumprun-sel4-demoapps

2 2

Query about the aarch64 Context Switch Code
by Sid Agrawal 15 Jun '22

15 Jun '22

Hi, I had a few questions about the context switch code in seL4 for aarch64. I spent a couple of days trying to make sense of it, so I thought it would be better to ask as I might be missing something that is not obvious. It looks like kernel_enter in traps.S [1] saves the user process's register immediately after an exception. And restore_user_context() in c_traps.c [2] is restoring them. Looks like the regs are stored in the TCB in the "tcbContext.registers" array. The restore code makes sense to me. It puts the ptr value of "(NODE_STATE(ksCurThread)->tcbArch.tcbContext.registers" in to the sp and starts loading the regs from there. However, the code in kernel_enter is a bit unclear to me. 1. What is the value of sp when executing the kernel_enter macro? Is that the SP_EL1, or somewhere else the sp was set to the address of the faulting thread's "tcbContext.registers". On reading the arm32's arm_swi_syscall [3] function, it looks like it is the latter, but I am unsure how that is being accomplished. It might be more to do with aarch64 than seL4. 2 Furthermore, when not specified, does sp mean SP_EL1 in EL1 and SP_EL0 in EL0, Or does lower case "sp" have a special meaning? I know that seL4 is configured to use SP_ELx at ELx based on value of SPEL in [4] 3 Lastly, what is lsp_i trying to do? Are we switching the value of sp from something else to the real kernel stack by storing the kernel's stack address in tpidr_el1? Thanks a lot, as always! Sid [1] https://github.com/seL4/seL4/blob/master/src/arch/arm/64/traps.S#L72 [2] https://github.com/seL4/seL4/blob/master/src/arch/arm/64/c_traps.c#L29 [3] https://github.com/seL4/seL4/blob/master/src/arch/arm/32/traps.S#L51 [4] https://github.com/seL4/seL4/blob/master/src/arch/arm/64/head.S#L78

1 1

SeL4: Cannot Input after booting VM Linux (x86_64)
by Sriram 15 Jun '22

15 Jun '22

Greetings, We built hello world program and recieved exact output as given in the tutorial while booting. Then we built the seL4 CamKes VM Linux and Optiplex 9020 for x86_64 platform and got the following results while booting through usb using syslinux commands "" Welcome to Buildroot buildroot login: [ 1.431752] clocksource: tsc: mask: 0xffffffffffffffff max_cycles: 0x31015f85297, max_idle_ns: 440795334135 ns [ 1.442241] clocksource: Switched to clocksource tsc [ 2.811817] random: fast init done [ 134.023597] random: crng init done "" After this we are not able to type anything (username and password to login ) We have both VTd and VTx enabled, What changes or approach should be done to solve this. Thanks and Regards R.Sriram

3 3

Canceled event: Reminder seL4 developer hangout @ Tue Jun 14, 2022 3pm - 4pm (PDT) (devel@sel4.systems)
by agrawal.sidhartha＠gmail.com 14 Jun '22

14 Jun '22

This event has been canceled. Title: [seL4] Reminder seL4 developer hangout - rump kernel - arm assembly question. When: Tue Jun 14, 2022 3pm – 4pm Pacific Time - Vancouver Where: https://unsw.zoom.us/j/82640784431 Calendar: devel(a)sel4.systems Who: * agrawal.sidhartha(a)gmail.com - organizer Invitation from Google Calendar: https://calendar.google.com/calendar/ You are receiving this courtesy email at the account devel(a)sel4.systems because you are an attendee of this event. To stop receiving future updates for this event, decline this event. Alternatively you can sign up for a Google account at https://calendar.google.com/calendar/ and control your notification settings for your entire calendar. Forwarding this invitation could allow any recipient to send a response to the organizer and be added to the guest list, or invite others regardless of their own invitation status, or to modify your RSVP. Learn more at https://support.google.com/calendar/answer/37135#forwarding

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 10 Jun '22

10 Jun '22

Hi all A friendly reminder that the seL4 developer hangout is on again next week: Tue, Jun 14, 10pm (UTC), Topics: (open) * Sydney: Wed, Jun 15, 8am * Central Europe: Wed, Jun 15, midnight * US Pacific Time: Tue, Jun 14, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

sel4 on bare-metal | Questions and comments
by Sid Agrawal 10 Jun '22

10 Jun '22

Hi, As per instructions from here[1, 2], I tried booting seL4 on an x86_64-desktop, x86_64-server as RPi4. I was able to get it to work on RPi4 with one minor change to the instructions, but I could not boot it on the x86_64-desktop or the x86_64-server. Below is my experience and the issues I faced. RPi4 ------ Spec: 8GB standard Rpi4 The final command "fatload mmc 0 0x10000000 sel4test-driver-image-arm-bcm2711" gave the following error: ** Reading file would overwrite reserved memory ** Failed to load 'sel4test-driver-image-arm-bcm2711 I could get around it by using a load address that was smaller by a factor of 0x10.( 0x1000000 instead of 0x10000000 i.e. one less zero). I cannot claim I understand why the first address failed and the second worked. Any pointers on that would help. After the change in the address, I saw the sel4 tests run as expected. x86_64 server ------------------ Spec: Dell R520, two quad-core Xeons (E5-2407 v2 @ 2.40GHz), 32GB of memory. The server's serial is redirected to the IPMI console. On the IPMI console, I see many messages related to the bios, etc. And finally, I see this: MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading rootserver... ok But nothing after this. Any thoughts of what could be going wrong here? I did not see any sel4 prints. x86_64 Desktop ---------------------- Spec: Core 2 Quad, 4 GB ram It was able to find the pinout for the serial port on the motherboard and connected to it(just like for RP). There was no output on the serial console. Even when bios-related messages were printed on the monitor, there was no output on the serial pins. I might need to enable the serial output on those pins in the bios or something similar. Fortunately, even though the serial pins did not have any output, the monitor output was the same as for the server. Unfortunately, it did not get any farther along than the server. MBR SYSLINUX 6.04 EDD [...] Loading sel4kernel... ok Loading rootserver... ok Any pointers here would be helpful. Thanks, Sid UBC Graduate Student ARM Research Intern [1] https://docs.sel4.systems/Hardware/IA32 [2] https://docs.sel4.systems/Hardware/Rpi4.html

2 5

Implementation of SeL4
by Sriram 10 Jun '22

10 Jun '22

Greetings This is Sriram Prakash, currently working on a project on secure system applications for avioics and found the concept and key use case of seL4 microkernel aligned to our main application : creating a secure OS on bareboard application We are facing certain issues as follows: - Booting via flashdrive, Output on Screen shows "Loading sel4 OK","Loading rootserver OK" and no other output in display, we recieved junk values using serial port Output. - We have put up a query on sel4Discourse : https://sel4.discourse.group/t/sel4-vm-linux-boot-in-x86-64-platform-pc/527, about the issues we are facing. - How to receive output in Display - Booting Linux VM on top of seL4 Any insights regarding the issues would be grateful, thank you for your time Regards R.Sriram Prakash

3 2

Running RISC-V seL4 in QEMU 7.0.50
by porter.188＠osu.edu 03 Jun '22

03 Jun '22

Hello, I'm trying to run sel4test in QEMU 7.0.50. I can compile successfully but sel4test hangs at "Jumping to kernel-image entry point...". Is there something different required now that sel4 is using OpenSBI? $ qemu-system-riscv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/sel4test-driver-image-riscv-spike OpenSBI v0.8 ____ _____ ____ _____ / __ \ / ____| _ \_ _| | | | |_ __ ___ _ __ | (___ | |_) || | | | | | '_ \ / _ \ '_ \ \___ \| _ < | | | |__| | |_) | __/ | | |____) | |_) || |_ \____/| .__/ \___|_| |_|_____/|____/_____| | | |_| Platform Name : ucbbar,spike-bare,qemu Platform Features : timer,mfdeleg Platform HART Count : 1 Boot HART ID : 0 Boot HART ISA : rv64imafdcsuh BOOT HART Features : pmp,scounteren,mcounteren BOOT HART PMP Count : 16 Firmware Base : 0x80000000 Firmware Size : 96 KB Runtime SBI Version : 0.2 MIDELEG : 0x0000000000001666 MEDELEG : 0x0000000000f0b509 PMP0 : 0x0000000080000000-0x000000008001ffff (A) PMP1 : 0x0000000000000000-0xffffffffffffffff (A,R,W,X) ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..8066a037] Looking for DTB in CPIO archive...found at 802d2128. Loaded DTB from 802d2128. paddr=[84020000..84020fff] ELF-loading image 'kernel' to 84000000 paddr=[84000000..8401ffff] vaddr=[ffffffff84000000..ffffffff8401ffff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' to 84021000 paddr=[84021000..843f6fff] vaddr=[10000..3e5fff] virt_entry=1b982 Enabling MMU and paging Jumping to kernel-image entry point...

3 4

UNSW tenure-track position
by Gernot Heiser 01 Jun '22

01 Jun '22

Any recent or soon PhD graduates whose work is around seL4? If os you might be interested in the operating system faculty position we have open at UNSW: https://external-careers.jobs.unsw.edu.au/cw/en/job/502766/lecturersenior-l… Gernot

1 0

Re: Reminder seL4 developer hangout
by Isaac Beckett 31 May '22

31 May '22

Oh boy, 3AM! I hope to make it, but if I sound tired, that’s why. > Date: Mon, 30 May 2022 00:08:16 +0000 > From: Birgit Brecknell <birgit.brecknell(a)unsw.edu.au> > Subject: [seL4] Reminder seL4 developer hangout > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Message-ID: <MEAPR01MB44693624005ED9CB8CFDD3A7DEDD9(a)MEAPR01MB4469.aus > prd01.prod.outlook.com> > Content-Type: text/plain; charset="iso-8859-1" > > Hi all > > A friendly reminder that the seL4 developer hangout is on again this week: > > Wed, Jun 1, 7am (UTC), Topics: (open) > > * Sydney: Wed, Jun 1, 5pm > * Central Europe: Wed, Jun 1, 9am > * US Pacific Time: Wed, Jun 1, 12 midnight > > Zoom link: https://unsw.zoom.us/j/82640784431 > > cheers > Birg > > > > --- > > Dr. Birgit Brecknell > > Project Officer > > Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> > > seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> > > 0433 880 571 > > > > Mon 9am-5pm > > Wed 9am-12pm > > Fri 9am-5pm

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 30 May '22

30 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, Jun 1, 7am (UTC), Topics: (open) * Sydney: Wed, Jun 1, 5pm * Central Europe: Wed, Jun 1, 9am * US Pacific Time: Wed, Jun 1, 12 midnight Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Running RISC-V seL4 in QEMU 7.0.50
by porter.188＠osu.edu 28 May '22

28 May '22

Hello, I am trying to run a simple hello world project in seL4 RISC-V in QEMU. It seems to hang at "Jumping to kernel-image entry point..." This same behavior happens on sel4test as well. In the past this was due to a bios option in QEMU changing. Is there something else going on here? I know seL4 uses OpenSBI instead of BBL for RISC-V but is there something else in QEMU or some other switch we need to add? The commands I run are: $ qemu-system-riscv64 -machine spike -cpu rv64 -nographic -serial mon:stdio -m size=4095M -bios none -kernel images/sel4test-driver-image-riscv-spike OpenSBI v0.8 ____ _____ ____ _____ / __ \ / ____| _ \_ _| | | | |_ __ ___ _ __ | (___ | |_) || | | | | | '_ \ / _ \ '_ \ \___ \| _ < | | | |__| | |_) | __/ | | |____) | |_) || |_ \____/| .__/ \___|_| |_|_____/|____/_____| | | |_| Platform Name : ucbbar,spike-bare,qemu Platform Features : timer,mfdeleg Platform HART Count : 1 Boot HART ID : 0 Boot HART ISA : rv64imafdcsuh BOOT HART Features : pmp,scounteren,mcounteren BOOT HART PMP Count : 16 Firmware Base : 0x80000000 Firmware Size : 96 KB Runtime SBI Version : 0.2 MIDELEG : 0x0000000000001666 MEDELEG : 0x0000000000f0b509 PMP0 : 0x0000000080000000-0x000000008001ffff (A) PMP1 : 0x0000000000000000-0xffffffffffffffff (A,R,W,X) ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..8066a037] Looking for DTB in CPIO archive...found at 802d2128. Loaded DTB from 802d2128. paddr=[84020000..84020fff] ELF-loading image 'kernel' to 84000000 paddr=[84000000..8401ffff] vaddr=[ffffffff84000000..ffffffff8401ffff] virt_entry=ffffffff84000000 ELF-loading image 'sel4test-driver' to 84021000 paddr=[84021000..843f6fff] vaddr=[10000..3e5fff] virt_entry=1b982 Enabling MMU and paging Jumping to kernel-image entry point...

1 0

Getting Badge Value of a badged EP capability
by Sid Agrawal 22 May '22

22 May '22

Hi seL4-devs and users, I have a question about implementing server and client using badged endpoints. Below I have laid out the scenario, the issue, and some questions. *Scenario* I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knows which object the client is trying to manipulate. The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object. *Issue* I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and give the badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has no way to look up the badge of the second cap, it cannot look up the underlying object for obj_T2. So my questions are: 1. Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask. 2. Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it? 3. As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why. Thanks for the help, everyone! Sid CS Graduate Student @ UBC sid-agrawal.ca

3 7

Untyped tutorial on RISC-V
by inf19109＠lehre.dhbw-stuttgart.de 18 May '22

18 May '22

Dear seL4 devs and community, I'm trying to do the seL4-tutorials on a RISC-V architecture. Now I'm stuck on the untyped tutorial. I tried to run the solution of the tutorial but I get the following error: <<seL4(CPU 0) [decodeUntypedInvocation/128 T0xffffffc17fee7200 "rootserver" @103fc]: Untyped Retype: Destination cap invalid or read-only.>> main@main.c:48 [Cond failed: error != seL4_NoError] Failed to retype seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc17fee7200 "rootserver" halting... I'm calling the function as follows: seL4_Untyped_Retype(parent_untyped, seL4_UntypedObject, // type untyped_size_bits, //size seL4_CapInitThreadCNode, // root 0, // node_index 0, // node_depth child_untyped, // node_offset 1 // num_caps ); parent_untyped = info->untyped.start + i (where i is incremented until (info->untypedList[i].sizeBits >= untyped_size_bits && !info->untypedList[i].isDevice) untyped_size_bits = seL4_TCBBits+1 child_untyped = info->empty.start It seams as if the function is not allowed for RISC-V. I don't know where the problem lies and I would appreciate any help or ideas. Best regards Miriam

2 3

Reminder seL4 developer hangout
by Birgit Brecknell 16 May '22

16 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, May 17, 10pm (UTC), Topics: (open) * Sydney: Wed, May 18, 8am * Central Europe: Wed, May 18, 12 midnight * US Pacific Time: Tue, May 17, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

VPPI IRQ 27 dropped on vcpu 3
by Han JingLong 韩景龙 11 May '22

11 May '22

Dear seL4 devs and community, I had made VMM work well on my platform(armv8, six A55 cpus, RAM is 8G) based on vm_multi with Linux Guest OS(vm0.num_vcpus = 4;) and Android Guest OS(vm1.num_vcpus = 6;). But I meet an error(vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3) when I enable SMP support with -DNUM_NODES=6. Actually, VPPI IRQ 27 dropped on some vcpu number is not fixed, maybe 1 or 2 or 3. Once this error appears, it will brush the screen crazily, the recurrence rate is about 10%. 1.Some logs are added for debugging this issue: --- a/seL4_projects_libs/libsel4vmmplatsupport/src/arch/arm/psci.c +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/arch/arm/psci.c @@ -53,18 +53,24 @@ int handle_psci(vm_vcpu_t *vcpu, seL4_Word fn_number, bool convention) uintptr_t target_cpu = smc_get_arg(&regs, 1); uintptr_t entry_point_address = smc_get_arg(&regs, 2); uintptr_t context_id = smc_get_arg(&regs, 3); + printf("[hjl] handle_psci target_cpu:%d\n", target_cpu); vm_vcpu_t *target_vcpu = vm_vcpu_for_target_cpu(vcpu->vm, target_cpu); if (target_vcpu == NULL) { target_vcpu = vm_find_free_unassigned_vcpu(vcpu->vm); if (target_vcpu && start_new_vcpu(target_vcpu, entry_point_address, context_id, target_cpu) == 0) { + printf("[hjl] handle_psci vm:%p vcpu_id:%d on success\n", vcpu->vm, target_vcpu->vcpu_id); smc_set_return_value(&regs, PSCI_SUCCESS); } else { + printf("[hjl] handle_psci vm:%p vcpu_id:%d on failure\n", vcpu->vm, target_vcpu->vcpu_id); smc_set_return_value(&regs, PSCI_INTERNAL_FAILURE); } } else { if (is_vcpu_online(target_vcpu)) { + printf("[hjl] handle_psci vm:%p target_cpu is online\n", vcpu->vm); smc_set_return_value(&regs, PSCI_ALREADY_ON); } else { + printf("[hjl] handle_psci vm:%p target_cpu is not online\n", vcpu->vm); smc_set_return_value(&regs, PSCI_INTERNAL_FAILURE); } } --- a/seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c +++ b/seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c @@ -570,6 +570,9 @@ static int vgic_dist_enable_irq(struct vgic_dist_device *d, vm_vcpu_t *vcpu, int vgic = vgic_device_get_vgic(d); DDIST("enabling irq %d\n", irq); set_enable(gic_dist, irq, true, vcpu->vcpu_id); + if (irq == 27) { + printf("[hjl] enabling irq:%d on vcpu:%d\n", irq, vcpu->vcpu_id); + } virq_data = virq_find_irq_data(vgic, vcpu, irq); if (virq_data) { /* STATE b) */ @@ -619,6 +622,7 @@ static int vgic_dist_set_pending_irq(struct vgic_dist_device *d, vm_vcpu_t *vcpu return err; } else { + printf("[hjl] virq_data:%p, gic_dist->enable:%d, is_enabled:%d\n", virq_data, gic_dist->enable, is_enabled(gic_dist, irq, vcpu->vcpu_id)); /* No further action */ DDIST("IRQ not enabled (%d) on vcpu %d\n", irq, vcpu->vcpu_id); return -1; } 2.The detailed log is as follows: [hjl] enabling irq 27, vcpu->vcpu_id:0 [hjl] handle_psci target_cpu:256 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:1 on success [hjl] enabling irq 27, vcpu->vcpu_id:1 [hjl] handle_psci target_cpu:512 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:2 on success [hjl] enabling irq 27, vcpu->vcpu_id:2 [hjl] handle_psci target_cpu:768 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:3 on success [hjl] enabling irq 27, vcpu->vcpu_id:3 [hjl] enabling irq 27, vcpu->vcpu_id:0 [hjl] handle_psci target_cpu:256 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:1 on success [hjl] enabling irq 27, vcpu->vcpu_id:1 [hjl] handle_psci target_cpu:512 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:2 on success [hjl] enabling irq 27, vcpu->vcpu_id:2 [hjl] handle_psci target_cpu:768 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:3 on success [hjl] enabling irq 27, vcpu->vcpu_id:3 [hjl] IRQ not enabled (27) on vcpu 3 virq_data:0x15794ad0, gic_dist->enable:1, is_enabled:0 vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3 [hjl] IRQ not enabled (27) on vcpu 3 virq_data:0x15794ad0, gic_dist->enable:1, is_enabled:0 vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3 ...... 3.Present situation: At present, I tracked and found that secondary cpus has been on by Host, but Guest OS's secondary_start_kernel function seem like not excuted. Does anyone know what caused it? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

camkes q's
by Sam Leffler 11 May '22

11 May '22

1. I need multiple VSpace "holes" to map page frames. This is the equivalent of what capdl_loader_app sets up in init_copy_frame. To do this I setup named static arrays and unmap the frame caps in camkes.c:post_main. This works but using a per-component attribute to enable this was awkward so I ended up adding a "copyregion" primitive to camkes. Is there a way to do this without adding to the camkes' syntax? It would also be nice not to allocate page frames only to release them at start but I didn't see a way to do this in capdl; is it possible (e.g. an easy way to leave an empty slot in the pt/pd)? 2. I pass capabilities with ipc msgs using camkes' rpc-connector templates. This requires multiple small changes that I want to enable only when being used (e.g. parameters to seL4_MessageInfo_new). My current plan is to add an optional keyword to a connection defn to enable support; e.g. connection seL4RPCCall foo(xfer_caps, from a, to b); Does this make sense or is there a better way? I rejected creating new connector templates that enable xfer_caps because I see this as a concept that applies to any ipc-based connector.

2 2

Information for Smmuv3 support of Sel4
by Tao Heng 陶恒-SW 06 May '22

06 May '22

Hi, list We are trying to porting Sel4 Vmm project on our platform.But we found there was no information about smmuv3 support of Sel4. Do you have some related development work for supporting this? Or can you give us some advice for supporting Smmuv3 on Sel4? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

One week left to propose a talk at the seL4 summit 2022!
by June Andronick (seL4 Foundation) 06 May '22

06 May '22

A reminder that you have until Monday 9th of May 2022 to propose a talk for the seL4 Summit 2022 :) http://sel4.systems/news/2022 <http://sel4.systems/news/2022> http://sel4.systems/Foundation/Summit/ <http://sel4.systems/Foundation/Summit/> http://sel4.systems/Foundation/Summit/cfp <http://sel4.systems/Foundation/Summit/cfp>

1 1

Reminder seL4 developer hangout
by Birgit Brecknell 02 May '22

02 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 4, 7am (UTC), Topics: (open) * Sydney: Wed, May 4, 5pm * Central Europe: Wed, May 4, 9am * US Pacific Time: Wed, May 4, 12 midnight Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

The seL4 Summit 2022 will be in Munich, Germany, on 10-12 Oct 2022
by June Andronick (seL4 Foundation) 29 Apr '22

29 Apr '22

It is our pleasure to confirm that the seL4 Summit 2022 will be in: Munich, Germany in the week of Oct 10th, 2022 It will be hosted by seL4 Foundation member Hensoldt Cyber. It will be a hybrid in-person/online event (if you'd like to propose a talk to be delivered remotely, please notify it in the submission). Remember that you have until Monday 9th of May 2022 to propose a talk. https://sel4.systems/news/2022 https://sel4.systems/Foundation/Summit/ https://sel4.systems/Foundation/Summit/cfp

1 0

Sending extraCaps over IPC | Unable to send 2 caps
by Sid Agrawal 29 Apr '22

29 Apr '22

Hello seL4 devs and users, I am trying to send two capabilities from one process to another via the extraCaps mechanism in the IPC. I can get it working when I send just 1 cap, but when I am sending 2 caps, the 2nd one never makes it. The extraCaps field on the receiver side is somehow always 1. Looking at the seL4 manual, I understood that I could send more than 1 capability via an IPC. But since on the receiver side, I can only specify one receive slot, I assumed that if more than 1 capability is received, it will be put in the consecutive slots. Not sure if this is a valid assumption. Looking at kerne/libsel4/include/sel4/constants.h <https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/constants.h#L…>, I see that seL4_MsgMaxExtraCaps is set to 2, so I think I should be able to send 2 caps. I have spent about 3 days trying to make this work and thought that at this stage, it would be best to ask :) My C code on the sender side looks something like this: seL4_CPtr cap1 = <alloc some capability> seL4_CPtr cap2 = <alloc some capability> seL4_SetMR(0, 0xabcd); seL4_SetCap(0, cap1); seL4_SetCap(1, cap2); seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 2, 1); tag = seL4_Call(receivers_ep_cap, tag); On the receive side, the code looks something like this: /* Allocate one csapce slot */ cspacepath_t received_cap_path_1; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_1); <- slot = 2786 assert(error == 0); /* Allocate another csapce slot */ cspacepath_t received_cap_path_2; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_2); <- slot = 2785(somehow decreasing) assert(error == 0); /* Since the allocated slots are decreasing in count, I pick the lesser one as my first slot * assuming that if more than 1 cap is received it will be put in the next slot */ seL4_CPtr min_cptr = MIN(received_cap_path_1.capPtr, received_cap_path_2.capPtr); seL4_SetCapReceivePath( /* _service */ received_cap_path.root, /* index */ min_cptr, /* depth */ received_cap_path.capDepth); tag = recv(&sender_badge); assert(seL4_MessageInfo_get_extraCaps(tag) == 2); <--- This asser fails. Thanks again!! Sid Graduate Student @ UBC

2 2

RTReply and cap xfer
by Sam Leffler 22 Apr '22

22 Apr '22

The kernel supports attaching a capability to an RTReply xfer. sel4test even checks this WAI. But capdl doesn't seem to support it as I see no way to express the set of rights associated with a capability to an RTReply object. I added capdl support so I can mark the Grant right and verified cap xfer works. TWas this intentional? -Sam

1 0

Running vm_multi app on qemu-arm-virt platform, udhcpc can not return
by ybbekele＠aggies.ncat.edu 22 Apr '22

22 Apr '22

Hi, I tried to build vm_multi for qemu-arm-virt using the procedures in this link https://docs.sel4.systems/projects/camkes-vm/. After building, I used the generated simulation file to do ./simulate in my build directory. After displaying 'welcome to buildroot', the console always prints the log "udhcpc: sending discover",which indicates udhcpc can not return. The related log was shown below: Starting syslogd: OK Starting syslogd: OK Starting syslogd: OK Starting klogd: OK Starting klogd: OK Starting klogd: OK Running sysctl: OK Running sysctl: OK Running sysctl: OK Initializing random number generator... [ 7.195263] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.315113] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.300770] random: dd: uninitialized urandom read (512 bytes read) done. Starting network: OK Starting network: OK Starting network: OK udhcpc: started, v1.31.0 udhcpc: started, v1.31.0 ifconfig: SIOCGIFFLAGS: No such device [ 9.077855] random: mktemp: uninitialized urandom read (6 bytes read) [ 9.177878] random: mktemp: uninitialized urandom read (6 bytes read) Welcome to Buildroot udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover As the simulation process progresses there was an error: _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x10080000 alloc_vm_device_cap@main.c:938 Grabbing the entire cap for device memory alloc_vm_device_cap@main.c:941 Failed to grab the entire cap My question is: 1. Is the two things have dependencies (The error and the hang at booting the system up)? 2. How can this issue be solved? 3. Is this issue related to the TimeServer component being imported to Qemu (as this is indicated as a requirement to run multi_vm on qemu-arm-virt)? Thank you for your time

1 0

Why vppi is sent from kernel to vmm by fault endpoint but not by notification ?
by wtliang785 21 Apr '22

21 Apr '22

hello devel, Why vppi , such as vtimer interrupt to guest, is sent from kernel to vmm by fault endpoint but not by notification? I see that spi to guest is sent from kernel to vmm by notification. thank you.

1 0

Reminder seL4 developer hangout/video call
by Gerwin Klein 19 Apr '22

19 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 19, 10pm (UTC) * Sydney: Wed, Apr 20, 8am * Central Europe: Wed, Apr 20, 12 midnight * US Pacific Time: Tue, Apr 19, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Combatting spam on this list
by Isaac Beckett 13 Apr '22

13 Apr '22

Thanks Peter! In my experience posts like that, linking to pornographic websites, are not made by humans anyway, but rather by bots. I don’t think this will effect humans too much except at the very beginning. It may make sense to implement a different captcha, as often the developers of those bots can outsource solving common captcha providers to underpaid humans. Using an uncommon or home-grown captcha solution will make it less likely that bots will be able to get around them using that method. And attacks like these aren’t targeted, usually, so I doubt the bot writers will adapt for one specific mailing list. That will stop bots from signing up in the first place, hopefully. We could also maybe report abuse of free email services like Gmail or Hotmail or similar in a semi-automated fashion. Would not surprise me if there is some sort of API for that. But on the other hand with the way those companies work it could be a waste of time and effort, since they might not do anything. And it may also make sense to keep track of which domains non-malicious users are sending email from. That way we can ban entire domains without worrying about getting rid of legitimate users unintentionally. For example, a small webmail service that we may not realize is a public email service at first, could be used by both a malicious user and a legitimate one. That way we’re only banning domains controlled by spammers exclusively. There’s lots of resources for this stuff thankfully, you can go on a whole tangent reading about email spam prevention on Wikipedia. I wish you luck with figuring out how to stop this annoying nonsense.

3 2

Unrecognized OPCODE fence.i/csrw
by porter.188＠osu.edu 13 Apr '22

13 Apr '22

I'm trying to setup a development machine for seL4 work. I would like to use v12.1.0. I setup seL4test-manifest per instructions here https://docs.sel4.systems/Hardware/spike.html repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir cbuild cd cbuild ../init-build.sh -DPLATFORM=spike -DRISCV64=1 # The default cmake wrapper sets up a default configuration for the target platform. # To change individual settings, run `ccmake` and change the configuration # parameters to suit your needs. ninja # If your target binaries can be executed in an emulator/simulator, and if # our build system happens to support that target emulator, then this script # might work for you: ./simulate I used repo init -u https://github.com/seL4/sel4test-manifest.git -b refs/tags/12.1.0 to be sure I got 12.1.0 but it doesn't matter, both branches/tags give the same error when I configure/compile. $ ../init-build.sh -DPLATFORM=spike -DRISCV64=1 -DSIMULATION=1 loading initial cache file /mnt/data/sel4test/projects/sel4test/settings.cmake -- Set platform details from PLATFORM=spike -- KernelPlatform: spike -- Setting from flags KernelSel4Arch: riscv64 -- Found seL4: /mnt/data/sel4test/kernel -- Found GCC with prefix riscv64-unknown-linux-gnu- -- Found GCC with prefix riscv64-unknown-linux-gnu- -- The C compiler identification is GNU 10.2.0 -- The CXX compiler identification is GNU 10.2.0 -- The ASM compiler identification is GNU -- Found assembler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Check for working C compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc - skipped -- Detecting C compile features -- Detecting C compile features - done -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Check for working CXX compiler: /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-g++ - skipped -- Detecting CXX compile features -- Detecting CXX compile features - done -- Found elfloader-tool: /mnt/data/sel4test/tools/seL4/elfloader-tool -- /mnt/data/sel4test/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... -- CPIO test cpio_reproducible_flag PASSED -- Found musllibc: /mnt/data/sel4test/projects/musllibc -- Found util_libs: /mnt/data/sel4test/projects/util_libs -- Found seL4_libs: /mnt/data/sel4test/projects/seL4_libs -- Found sel4_projects_libs: /mnt/data/sel4test/projects/sel4_projects_libs -- Found sel4runtime: /mnt/data/sel4test/projects/sel4runtime -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- libmuslc architecture: 'riscv' (from KernelSel4Arch 'riscv64') -- Detecting cached version of: musllibc -- Found Git: /usr/bin/git (found version "2.25.1") -- Not found cache entry for musllibc - will build from source -- Found PythonInterp: /usr/bin/python (found version "2.7.18") CMake Warning (dev) at /home/user/.local/lib/python3.8/site-packages/cmake/data/share/cmake-3.22/Modules/FindPackageHandleStandardArgs.cmake:438 (message): The package name passed to `find_package_handle_standard_args` (NANOPB) does not match the name of the calling package (Nanopb). This can lead to problems in calling code that expects `find_package` result variables (e.g., `_FOUND`) to follow a certain pattern. Call Stack (most recent call first): /mnt/data/sel4test/tools/nanopb/extra/FindNanopb.cmake:340 (FIND_PACKAGE_HANDLE_STANDARD_ARGS) /mnt/data/sel4test/tools/seL4/cmake-tool/helpers/nanopb.cmake:29 (find_package) /mnt/data/sel4test/projects/sel4_projects_libs/libsel4nanopb/CMakeLists.txt:11 (include) This warning is for project developers. Use -Wno-dev to suppress it. -- Found NANOPB: /mnt/data/sel4test/tools/nanopb -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/sel4test/build user@user-KVM:/mnt/data/sel4test/build$ ninja [42/267] Building ASM object kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj FAILED: kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj /usr/bin/ccache /mnt/data/opt/riscv/bin/riscv64-unknown-linux-gnu-gcc --sysroot=/mnt/data/sel4test/build -I/mnt/data/sel4test/kernel/include/plat/default -I/mnt/data/sel4test/kernel/include -I/mnt/data/sel4test/kernel/include/64 -I/mnt/data/sel4test/kernel/include/arch/riscv -I/mnt/data/sel4test/kernel/include/arch/riscv/arch/64 -I/mnt/data/sel4test/kernel/include/plat/spike -I/mnt/data/sel4test/kernel/include/plat/spike/plat/64 -I/mnt/data/sel4test/kernel/libsel4/include -I/mnt/data/sel4test/kernel/libsel4/arch_include/riscv -I/mnt/data/sel4test/kernel/libsel4/sel4_arch_include/riscv64 -I/mnt/data/sel4test/kernel/libsel4/sel4_plat_include/spike -I/mnt/data/sel4test/kernel/libsel4/mode_include/64 -I/mnt/data/sel4test/build/kernel/gen_config -I/mnt/data/sel4test/build/kernel/autoconf -I/mnt/data/sel4test/build/kernel/gen_headers -I/mnt/data/sel4test/build/kernel/generated -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -MD -MT kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -MF kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj.d -o kernel/CMakeFiles/kernel.elf.dir/src/arch/riscv/head.S.obj -c /mnt/data/sel4test/kernel/src/arch/riscv/head.S /mnt/data/sel4test/kernel/src/arch/riscv/head.S: Assembler messages: /mnt/data/sel4test/kernel/src/arch/riscv/head.S:24: Error: unrecognized opcode `fence.i' /mnt/data/sel4test/kernel/src/arch/riscv/head.S:31: Error: unrecognized opcode `csrw sscratch,x0' [44/267] Invoking muslc build system /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c: In function 'getcwd': cc1: warning: function may return address of local variable [-Wreturn-local-addr] /mnt/data/sel4test/projects/musllibc/src/unistd/getcwd.c:9:7: note: declared here 9 | char tmp[PATH_MAX]; | ^~~ ninja: build stopped: subcommand failed. I tried riscv-gcc 10.2.0 and 11.1.0 with the same results. $ riscv64-unknown-linux-gnu-gcc --version riscv64-unknown-linux-gnu-gcc (gca312387ab1) 10.2.0 Copyright (C) 2020 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Is there some extension I need to add to get this working? Where do I do that?

2 2

答复: Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 12 Apr '22

12 Apr '22

Hi The root cause of this problem has been found, when Guest OS do the virtio console driver probe, if virtqueue's desc addr allocated by alloc_pages_exact() in the setup_vq() function is >= 0x100000000 (it is common when the memory of VM allocated exceeds 3G), at first It will be shifted right 12 bits by Guest OS(turn into a value >= 0x100000), and then use iowrite32(iobase + VIRTIO_PCI_QUEUE_PFN) to notify Host, after unsigned int type data be shifted left 12 bits by Host, the higest bits 0x1 of virtqueue's desc addr will be lost. I have submitted a PR for the amendment, waiting for the review and merge into the main branch. https://github.com/seL4/seL4_projects_libs/pull/43 BR. Allen 发件人: Han JingLong 韩景龙发送时间: 2022年3月21日 20:27 收件人: 'devel(a)sel4.systems' <devel(a)sel4.systems> 主题: Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157<mailto:vm_ram_touch@guest_ram.c:157> Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157<mailto:vm_ram_touch@guest_ram.c:157> Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Combatting spam
by David Barrass 12 Apr '22

12 Apr '22

Hi Peter, Thank you for raising this issue - it is an annoying distraction. The general standard of the list is very high as one would expect and it is a shame to see this kind of behaviour polluting the discussions. I am very happy to have to earn a privilege to post and am happy for anything I post to be moderated. I would welcome any proposition to keep spammers off the list whilst keeping it open but I don't think any solution should impose additional burdens on the moderators. I think that this warrants a bit of thought and will give this some consideration. Your proposal sounds good and I support it. In the meantime thank you and many thanks to all the team who make this happen. I find the work on seL4 very valuable and relevant. best regards to all, David

1 0

Combatting spam on this list
by Peter Chubb 12 Apr '22

12 Apr '22

Hi Folks, We're trying hard to avoid spam coming through this list. In particular we moderate all emails coming from non-members, and only let through on-topic postings. Recently, however, we've had some people join the list, and then posting spam. I'm proposing that the first post a person makes will always be moderated; and we'll turn off the moderation after the first on-topic posting. Anyone who posts spam will have that address marked as discard immediately. This means that *all* next posts will be moderated until I or one of the other moderators lets them through, because I'll be changing the default processing. Comments? I'd rather keep things as open as possible, but spammers are making it hard. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

RFC 10
by Gerwin Klein 11 Apr '22

11 Apr '22

This is a last call for comments for RFC-10 before the TSC votes on it this week: https://sel4.atlassian.net/browse/RFC-10 The RFC is about consolidating AArch64 page table objects and has been uncontroversial so far, just wanted to make sure people are aware of it. Cheers, Gerwin

2 1

Does the lastest master branch support gic v3 virtulization?
by wtliang785 10 Apr '22

10 Apr '22

hello devel, We want to use Sel4 in our project, but the gic version is v3. I know sel4 kernel 12.1.0 version does not support v3 virtuliazation. My question is that what is the status for supporting the v3 virtulization in lastest sel4 kernel master branch? Does the lastest master branch support gic v3 virtulization? thank you Peter Wang

2 1

capDL-tool fix for empty CNode slots
by Sam Leffler 07 Apr '22

07 Apr '22

If you generate capdl for a CNode with empty slots, capDL-tool incorrectly calculates CDL_CapMap::num because it uses Map.size which doesn't include empty slots. The right way to calculate "num" is by taking the max of the key values +1. diff --git a/capDL-tool/CapDL/PrintC.hs b/capDL-tool/CapDL/PrintC.hs index ec0eda9..b4a2cbb 100644 --- a/capDL-tool/CapDL/PrintC.hs +++ b/capDL-tool/CapDL/PrintC.hs @@ -224,7 +224,7 @@ memberSlots objs obj_id slots irqNode cdt ms = showSlots objs obj_id (Map.toList slots) irqNode cdt ms +++ "}," where - slot_count = Map.size slots + slot_count = if Map.null slots then 0 else (fst $ Map.findMax slots) + 1 printInit :: [Word] -> String printInit argv = -Sam

2 3

Interrupt handling - General Purpose Timer
by JENKINSON Mark 07 Apr '22

07 Apr '22

Hi seL4 Devel, We are trying to use the General Purpose Timer1 for our i.MX8MQ-based board within a simple CAmkES app. GPT1 is initialising and starting OK, but the interrupt handler for handling rollover is not being triggered. Through instrumenting the code with printf's, the GPT initialisation looks reasonable, and the expected rollover interrupt is being generated and seen within handleInterrupt(); however, the interrupt handler routine that has been registered is not being called. I'm hoping that someone can give me some ideas where to investigate next please? A few more details: From gpt_init() (in util_libs/libplatsupport/src/mach/imx/gpt.c), instrumentation within allocate_irq_callback() confirms that, for: gpt->irq_id = ps_irq_register(&gpt->io_ops.irq_ops, irq, gpt_handle_irq, gpt); our values are: irq->type = 3; // PS_INTERRUPT irq->irq.number = 87 (0x57); // 55 (0x37) + 32 = 87 (0x57) which agrees with the GPT1 entry from our dts file (when combined with the offset of 32, which I've seen explained elsewhere): gpt@302d0000 {... reg = < 0x302d0000 0x10000 >; interrupts = < 0x00 0x37 0x04 >;... And gpt_handle_irq() is registered as the interrupt handler, which resets the rollover flag and manages the counter's high_bits variable. Resulting from this call to ps_irq_register(), gpt->irq_id = 27 (0x1b), although I'm not sure of the significance of this irq_id value. Our test app starts GPT1. After ~3 mins, the timer rolls over, as expected. Instrumentation in handleInterrupt(irq) is triggered with: irq = 87 (0x57); // as expected, the GPT1 rollover interrupt However, gpt_handle_irq() is never called, despite being associated with irq 87 back in the ps_irq_register() call. Instrumentation in handleInterrupt() shows that the IRQSignal case is executed and sendSignal() is called. Within sendSignal, the NtfnState_Idle case is executed, calling ntfn_set_active(ntfnPtr, badge), with badge = 1. I stop tracking the flow there, but pick up again that ackInterrupt() is visited with irq = 87 (0x57). Everything looks in order (the right interrupt is generated at the right time and is detected) except gpt_handle_irq() is not called. The timer app keeps ticking away, but without the rollover management, time ends up skipping. Thanks for your help, Mark. This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

1 0

OpenPower/PowerPC/ppc64le port: major concerns and obstacles
by Isaac Beckett 06 Apr '22

06 Apr '22

Hello seL4 devel! Recently I was on the developer hangout meeting and brought up a ppc port. Interest seemed low, and some even called ppc a “niche” architecture which seems unfair. There was also the much more concrete concerns of funding and overall maintenance. I believe an PPC port would be very valuable, and I plan to do a whole essay/write up of some sort, but I am also not the most familiar with the technical challenges, and could use more information on those. I do think there is definitely people who would want to run seL4 on PowerPC platforms. PowerPC is one of the few ISAs that has existing, modern hardware without closed-source binary blobs, which I believe pose a real threat to the trustworthiness of the hardware seL4 is currently capable of running on.

2 1

A way to reclaim initial thread resources
by Marcin Witkowski 06 Apr '22

06 Apr '22

Hey, I am currently looking for a way to reclaim resources allocated by kernel for the rootserver thread, i.e. memory for CNode, TCB, BootInfo, etc. My current approach looks like this: * in rootserver instead of calling seL4_TCB_Suspend, call custom syscall seL4_ReclaimRootserverResources. This sycall as parameters takes CNode and slot no. after which kernel should be able to freely write new caps. This CNode is main CNode of some component initialized by the rootserver. * implmenetation of this syscall then suspends initial thread, schedules new thread, revokes most of rootserver's resources, notably TCB, BootInfo, IPCBuffer, VSpace and CNode. Then for those now free memory regions new untyped capabilities are created, with the same sizes as the original objects. Lastly, new capabilities are written to subsequent slots in CNode a'la boot.c, so with null MDBNode; mdbRevocable and mdbFirstBadged set to true. This solution has couple of problems. First and foremost, it requires creating additional syscall to handle this. Secondly, even though the component _technically_ has access to this newly created capabilities, it doesn't know where they are, or how big they are. This could be partially band-aided by hardcoding this information in relevant component, but that is far from elegant. This component also recives rest of the untyped memory from rootserver, including bootinfo entries about this memory specification, so that renders solution with hardcoding spec even worse. Last but not least, before the seL4_ReclaimRootserverResources is called, all the components are resumed using seL4_TCB_Resume as part of rootserver's work, so there could be race-condition between calling reclaiming syscall, and component initialization (although I am not 100% sure about that part) Is there maybe a better way to do it, and I am doing it all round? The perfect solution would be to somehow extend bootinfo and/or remaining untypeds that were given by the kernel to the rootserver.

2 3

Reminder seL4 developer hangout/video call
by Birgit Brecknell 04 Apr '22

04 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Wed, Apr 6, 7am (UTC), Topics: (open) * Sydney: Wed, Apr 6, 5pm * Central Europe: Wed, Apr 6, 9am * US Pacific Time: Wed, Apr 6, 12 midnight (There are too many time zones in the world to cite them all :-)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

The Call for Presentations for the seL4 summit 2022 is out!
by June Andronick (seL4 Foundation) 01 Apr '22

01 Apr '22

We are calling for proposals to present at the seL4 Summit 2022! Share your seL4 work. Share your seL4 experience. Share your seL4 thoughts. Share your seL4 questions. Check the full Call For Presentations and topics of interest at: https://sel4.systems/Foundation/Summit/cfp <https://sel4.systems/Foundation/Summit/cfp> To propose a talk, send an abstract of one page or less by Monday 9th of May 2022 to summit(a)sel4.systems <mailto:summit@sel4.systems>. Please do spread the word and also encourage others to submit a talk if you like their work! Thanks, June

1 0

Overlapping pointer returned by memalign
by WILLIAMS Stephen 01 Apr '22

01 Apr '22

Hi, I’m currently working on a project porting drivers from U-Boot to seL4 and have run into an unexpected problem seemingly triggered by use of the memalign within the U-Boot drivers. What I am seeing is that calls to memalign from within my CAmkES component can return pointers to regions which overlap with those previously returned by malloc. Obviously this leads to the two allocated regions trampling over each other and resulting corruption of data. I’m at a complete loss to explain this behaviour and would be very grateful to receive any suggestions or pointers. Thanks for your help, Stephen This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

3 9

Re: How to switch virtual machines linux in vm_multi from camkes-vm-example?
by Peter Chubb 31 Mar '22

31 Mar '22

>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: yjy> `screen /dev/ttyUSB0 115200`. I have a shell terminal that can yjy> see the output from VM0. I input @1 to shell, which is useless. It only works at the start of a line. Peter C yjy> At 2022-03-31 14:12:16, peter(a)chubb.wattle.id.au wrote: >>>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: >> yjy> Hi, I have already run the camkes-vm-example vm_multi on my yjy> board, but i don't know how to switch linux vm shell from another yjy> linux vm, Can anyone help me solve this? >> >> If you're talking about controlling the serial console to talk to >> different VMs, the instructions are >> https://github.com/seL4/camkes-vm in the README.md under 'Serial' >> >> >> In brief, output from different VMs is colour coded. Switch >> between them for input with @0, @1, @2 etc. >> >> Peter C _______________________________________________ Devel >> mailing list -- devel(a)sel4.systems To unsubscribe send an email to >> devel-leave(a)sel4.systems yjy> [2 <text/html; GBK (base64)>] -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

How to switch virtual machines linux in vm_multi from camkes-vm-example?
by yjy 31 Mar '22

31 Mar '22

Hi, I have already run the camkes-vm-example vm_multi on my board, but i don't know how to switch linux vm shell from another linux vm, Can anyone help me solve this? Best, Comet

2 1

Question for student research
by Seth Nielson 31 Mar '22

31 Mar '22

Hi. I am mentoring a student group trying to do some work on SEL4. We are trying to setup basic TCP/IP networking and are really struggling to find documentation or up-to-date guides. We found a project that has networking (it even has some filesystem and a small webserver as part of the project). We thought we just about had the networking component working for QEMU but there seems to be issues with QEMU and networking, at least the way we did it. Does anyone have any how-to guides for getting basic networking up and running? If QEMU is not great for networking, please suggest a development board. Thanks much.

2 2

Information for Additional Virtio Driver Support of Sel4
by Tao Heng 陶恒-SW 28 Mar '22

28 Mar '22

Hi list， Is there any specific plan or some related development for supporting the Additional Virtio Driver (* e.g Virtio Blk, Virtio RNG, Virtio Balloon), as you mentioned in READ.md of libsel4vmmplatsupport, especially for the Virtio Blk? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 2

propagating initial thread's capabilities
by Sam Leffler 28 Mar '22

28 Mar '22

The rootserver gets various caps setup for it by the kernel (see Table 9.1 in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes that signal the rootserver should hand-off a cap by moving the rootserver's cap to the designated CNode just before it terminates. This involves modifications to CAmkES, capDL, and the rootserver. Is there a better way? Is there an existing example of doing this? Are any of these global objects accessible some other way than hand-off from the rootserver? -Sam

2 4

Questions about Kscurdomain variable.
by 603644559＠qq.com 25 Mar '22

25 Mar '22

In the case of multiple cores, is the scheduling of each core judged according to the kscurdomain, that is, the scheduling table of the domain is maintained by an operating system, rather than an independent kscurdomain in a core and a scheduling table of the domain in each core?

1 0

Hi,
by ezabujpz＠uuf.me 23 Mar '22

23 Mar '22

Hi, https://www.assortlist.com I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 22 Mar '22

22 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 2pm (There are too many time zones in the world to cite them all :-)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 21 Mar '22

21 Mar '22

Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

A question about capability derivation tree
by Chang Liu 18 Mar '22

18 Mar '22

Hi list, Here is a question about capability derivation trees, in particular when it comes to seL4_CNode_Copy and seL4_CNode_Mint. Suppose I have an untyped cap Untyped0, and I create a page cap by retyping Untyped0 into Frame0 (with seL4_AllRights). I then call CNode_Mint to mint Frame0 into Frame1 with restricted rights (say read-only). Finally, I call CNode_Copy to copy Frame1 into Frame2. What would the capability derivation tree look like at the end? Case 1: |--------| |Untyped0| |--------| / | \ / | \ / | \ |------| |------| |------| |Frame0| |Frame1| |Frame2| |------| |------| |------| Case 2: |--------| |Untyped0| |--------| | |------| |Frame0| |------| | |------| |Frame1| |------| | |------| |Frame2| |------| Case 3: |--------| |Untyped0| |--------| | |------| |Frame0| |------| / \ / \ |------| |------| |Frame1| |Frame2| |------| |------| Which one of the above is the correct answer? I suspect it's case 3, but I'm not sure. Best, Chang

1 0

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 11 Mar '22

11 Mar '22

Finally, I figured out the root cause of this issue. It happened when I changed the mac address of the virtio net probed for the vm guest. According to the issue, It seemed that the virtio_net driver of the libsel4vmmsupport did not support emulating the io control for changing the mac addess of the virtio net in the guest. 发件人: Tao Heng 陶恒-SW 发送时间: 2022年3月9日 14:49 收件人: 'devel(a)sel4.systems' <devel(a)sel4.systems> 主题: Sel4 VMM Virtio Net Related Porting on Other SOC Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 09 Mar '22

09 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

Does the CSpace needs to have a cap to the TCB
by Sid Agrawal 09 Mar '22

09 Mar '22

Hi, We roughly do the following steps when setting up a new process in seL4: - Allocate a new TCB - Allocate new CSpace - Make the TCB point to the CSpace - Construct the VSpace and add the relevant caps in the new CSpace - Update the VSpace cap in the TCB. - Add a copy of the TCB cap in the new CSpace. (I am looking at the process spawn function in libesel4utils at: https://github.com/seL4/seL4_libs/blob/master/libsel4utils/src/process.c#L4…) My question is about the last point i.e. copying of TCB to the new CSpace. If I want to restrict the new domain from changing its VSpace, suspend itself, and change its fault handlers, I would simply not do the last step. Will that work? Is there any fundamental need for the TCB cap to be in the cspace it points to? Thanks, Sidhartha Agrawal

2 1

vm_multi usage
by Michael Neises 08 Mar '22

08 Mar '22

Hi, I'm just beginning to use multiple VMs at once, and I have a simple question. When I simulate my image, two VMs are running, and I get a terminal interface to one of them. Can I also switch my terminal to interface with the second VM? Cheers, Michael Neises

2 1

Re: I Have some questions about the domain mechanism in the seL4
by Isaac Beckett 08 Mar '22

08 Mar '22

> Date: Sat, 5 Mar 2022 19:15:05 +1100 > From: Kent Mcleod <kent.mcleod72(a)gmail.com> > Subject: [seL4] Re: I Have some questions about the domain mechanism > in the seL4 > To: 603644559(a)qq.com > Cc: devel <devel(a)sel4.systems> > Message-ID: > <CA+-ozWdgMgBin34WBUoVL+uHSNfU=e852ekPgrNGZ5J7+nyN0g(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > >> On Sat, Mar 5, 2022 at 6:11 PM 603644559--- via Devel >> <devel(a)sel4.systems> wrote: >> >> For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… >> But i still do not know the purpose of adding the domain mechanism in seL4, >> Can anyone explain what kind of requirement led to the design of the domain mechanism? >> Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism. > > It was added in order to enable the completion of the info-flow proofs. > >> From the infoflow proof paper > (https://trustworthy.systems/publications/nicta_full_text/6464.pdf) > where it is called the partition scheduler: > "Similarly, the original seL4 scheduler, before partition > scheduling was implemented, was known not to enforce > isolation. We could not prove information flow security until > we had fully and correctly specified the partition scheduler > in the updated abstract specification. Proving information > flow security then required us to show that the scheduler’s > choice about which partition to schedule next can never be > affected by any other partition, as one would expect." Hello! It was my understanding that seL4 used to not have an in-kernel scheduler, and scheduling was up to the root task. How did that work? And why was the choice made to add the MCS features? Basically, why the change from having scheduling in the kernel vs. in userspace? It’s probably more convenient, especially since most operating systems are used to having scheduling in the kernel itself (so easier for people to think about). There are probably more technical reasons too. What are those?

2 3

I Have some questions about the domain mechanism in the seL4
by 603644559＠qq.com 07 Mar '22

07 Mar '22

For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… But i still do not know the purpose of adding the domain mechanism in seL4, Can anyone explain what kind of requirement led to the design of the domain mechanism? Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism.

2 2

Reminder: sel4 developer hangout
by Birgit Brecknell 07 Mar '22

07 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Questions about shared page tables and Intel's MPK
by Sid Agrawal 06 Mar '22

06 Mar '22

Hi, I have a couple of questions about the virtual memory subsystem in seL4. 1. Intel's Memory Protection keys let a process restrict the access to given virtual address ranges based on a key. This key is the bit 62:59 of the virtual address. It is stored in the PTE of the level 4/5 Page Table. I want to use this feature in my project. Does seL4 support the setting of Memory Protection keys for virtual addresses? I couldn't find any mention of it in the source. I understand that if I use the current API of "seL4_X86_PageTable_Map" with those higher bits of the vaddr set, the kernel will ignore them. Is my understanding correct? Furthermore, was a decision made not to support MPK at some point? 2. As per section 7.3 of the seL4 manual, seL4 doesn't allow sharing of page tables. I am trying to understand the reasoning behind this. Was this done to aid verification? Thanks, Sidhartha S Agrawal

3 4

libsel4muslcsys: Error attempting syscall 215
by skydivebcn＠gmail.com 05 Mar '22

05 Mar '22

Hi guys, I was trying to boot a custom Linux 4.9.302 Kernel and fot this horrible message: "libsel4muslcsys: Error attempting syscall 215" hugo@dev:~/seL4/sel4webserver_hugusmaximus_fork/build$ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off" [sudo] contraseña para hugo: ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61bf9000..631120af] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61d3a2b8. Loaded DTB from 61d3a2b8. paddr=[60243000..60244fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60242fff] vaddr=[ff8060000000..ff8060242fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' to 60245000 paddr=[60245000..617fdfff] vaddr=[400000..19b8fff] virt_entry=408f38 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf815400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices@main.c:655 module name: map_frame_hack install_linux_devices@main.c:655 module name: init_ram install_linux_devices@main.c:655 module name: cross_vm_connections libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x8020000 as this is purely an seL4 error message (musl libc seL4 code?) then I would appreciate any hint about what can be going on. P.S.: I have run my seL4 qemu aarch64 with several Linux kernel versions and never had this problem until now.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 04 Mar '22

04 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

seL4 Native Web-browser
by Daniel Douglas Dyrseth 04 Mar '22

04 Mar '22

Hi, everyone What parts are needed besides seL4 to get a fully functioning Chromium browser running in a Wayland server? (No virtual OS inside seL4). I'm talking native seL4 OS capable of running Chromium with all features. Hoping for some insightful answers, and at least a list from a Pro - of the minimum parts needed for this. Regards, Daniel Douglas Dyrseth

2 1

Call for support contract to the seL4 Foundation
by Birgit Brecknell 25 Feb '22

25 Feb '22

A friendly reminder that bids are due before March 4th, 2022 AOE: The seL4 foundation is seeking to contract support for the following duties: - address open github issues in the seL4 organisation repositories, with prioritisation directed by the TSC delegates; this includes: - documentation, tutorials - bugs - tests - docsite and possibly website in coordination with Foundation people - help keeping an eye on making sure questions on mailing lists, discourse and github issues are answered (by someone) Requirement for the person working on these tasks are: - multiple years of experience with seL4, both at kernel level and user-level code - good familiarity with the seL4 organisation repositories - active contributor to one or more seL4 repositories - fluent in written and spoken English The seL4 foundation would contract a service company, initially for 6 months. The service company should identify the person that will be performing the work, ideally on a full-time basis. To bid for the contract, send email to foundation(a)sel4.systems before March 4th, 2022 AOE, with the resume of the person that will be performing the work and a cover letter addressing the requirements. --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 24 Feb '22

24 Feb '22

Thank you both for the discussion on licensing. Seems that GPLv3 is a good choice for now. Wikipedia seems to claim that ReactOS is licensed under "GPLv2 or any later version" but I didn't find this on the reactos source code itself. If the ReactOS foundation has an objection later I can always change it to v2. Best, Chang On Wed, Feb 23, 2022 at 12:09 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Chamg, > > At 2022-02-22T23:29:21-0500, Chang Liu wrote: > > I just added a LICENSE file which is GPLv3. > > Good choice! > > > I'm honestly not sure what the difference between GPLv2 and GPLv3 > > There are modest differences, but the general thrust of both versions of > the license is the same: guaranteed access to source code under a "share > and share alike" principle. > > > is so I went with the latest version (I assume they are compatible?) > > Technically, no. But most GPLv2 software is licensed under terms that > allow promotion of the license to "any later version". One famous > example of an exception that is GPLv2-only is the Linux kernel. > So is seL4 itself[1]. Consider whether you expect to need to share code > with a GPLv2-only project. (Even if you do, I would only revisit your > decision once concrete code-sharing is imminent.) > > You're not stuck with a choice of a single license forever. The GPLv3 > is a good selection to start with (in my opinion) because most > organizations that would like to exploit a work for proprietary > advantage are allergic to that license. > > You can always relicense a work under more permissive terms later if > doing so would align better with your goals. Going from more permissive > terms (like a BSD-style license) to a copyleft (like any version of the > GPL) can be impractical, or result in unintended consequences, because > it is arguably impossible to rescind the permissive license on the older > versions of the code--unless you have an Apple- or Oracle-sized budget > for lawyers to intimidate rivals maintaining the old code base. > > There is probably a better forum for licensing discussions, but my view > is that you've made a perfectly reasonable choice, one that situates > your project squarely and clearly within the Free Software community, > while still leaving you the option to reconsider later. > > Regards, > Branden > > [1] https://microkerneldude.org/2019/12/09/what-does-sel4s-license-imply/ >

1 0