- Devel - lists.sel4.systems

General Question On Object Methods
by tunacici7＠gmail.com 25 Sep '24

25 Sep '24

I've recently started to learn seL4 by following the Tutorials, which have been great so far. I've been also reading the Manual & API reference to understand and gain insight into different mechanisms. However, I have one fundamental question: Are the object methods system calls? It is said that seL4 only has 3 logical system calls: Send, Recv and Yield. (In all the slides, videos and other documents I have seen) And the rest is just variations of those ones. But what about object methods? Are they system calls? Are they executed in kernel space? If they are system calls, then wouldn't all the resources out there be misleading? Since there are way more than just Send, Recv and Yield. If they are not, then how are they handled? Does 'libsel4' have anything to do with it? I can't imagine 'seL4_Untype_Retype' executing in user space. Unfortunately, I couldn't find any answers to this question online. So that's why I'm asking it here. Maybe there are others who wonders the same thing. NOTE The API Reference page confuses me even more. It lists Object Methods in its own category (instead of being under System Calls). Does this means Object Methods are NOT system calls? Or the term System Call is just not what I think it is(basically an endpoint to kernel)?. END NOTE Thanks for the answers in advance. -T

8 21

seL4 developer hangout reminder
by Birgit Brecknell 16 Sep '24

16 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 18 Sep, 8:00am UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Less than 1 week left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 09 Sep '24

09 Sep '24

Less than 1 week left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Virtual address ranges used in seL4 initial thread after boot?
by Ben McCart 06 Sep '24

06 Sep '24

I have read the manual in section 9.2 about userImageFrames and how to infer the virtual address range for the pages being used for the userland image, which I frankly do not concretely understand. For example, I can take the address of main() and that leads me to believe my first user image frame (page frame actually I suspect) is probably at 0x40000, but it feels like guessing. (Not good!) In addition, I like to know the address range used for the stack of the initial thread, as well as any other reserved regions (I read somewhere in the manual about reserved virtual address space for the kernel, but I can't remember where I read that and now I can't find it.) Are there any macros included in public header files that I can use in my project to get the starting addresses for any of these regions? Barring that, is there any straight-forward reliable way to find the starting address for these regions (or in the case of kernel reserved virtual address range is it documented anywhere?) I am on version 12.0 of seL4 for my project. Thank you! -Ben

2 2

Less than 2 weeks left to get the early-bird registration for the seL4 summit
by Birgit Brecknell 02 Sep '24

02 Sep '24

Less than 2 weeks left to get the early-bird registration for the seL4 summit The early bird cut-off date for the seL4 summit 2024 [0] is 15 September 2024. The summit will be held in Sydney, Australia, 15-17 October 2024. The seL4 summit will cover the complete seL4 ecosystem, consisting of the verified microkernel, as well as all seL4-related technology, tools, infrastructure, products, projects, and people. Tickets include: - Participation in the 3-day conference, including talks, keynotes, seL4 updates & discussions - Networking with other seL4 experts and enthusiasts - Reception and dinner Register here [1] A number of informal social activities [2] are being organised by local Sydney-siders. Check out the list [2] and contact the organiser to register your interest. [0] https://sel4.systems/Foundation/Summit/2024/ [1] https://events.linuxfoundation.org/sel4-summit/register/ [2] https://sel4.systems/Foundation/Summit/2024/social-activities Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 02 Sep '24

02 Sep '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Tue 3 Sep, 10:00pm UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

seL4 developer hangout reminder
by Birgit Brecknell 19 Aug '24

19 Aug '24

Hi all A friendly reminder that the seL4 developer hangout is on again this week. Wed 21 Aug, 8:00am UTC. For your local date and time please see https://sel4.systems/contact/. Zoom link: https://unsw.zoom.us/j/82640784431 Birgit Brecknell seL4 Foundation Project Coordinator Sydney, Australia Mon 9-5 Wed 2-5 Fri 9-5 birgit(a)sel4.systems <mailto:birgit@sel4.systems> bbrcknl(a)gmail.com <mailto:bbrcknl@gmail.com>

1 0

Gpu passthrough
by Hugo V.C. 15 Aug '24

15 Aug '24

Hi all, here a simple question: is there any example/tutorial off gpu passthrough to a Linux guest? Best,

4 6

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 14 Aug '24

14 Aug '24

Hi everyone, I am getting a link failure during the build of sel4test-tests: /usr/bin/ld: apps/sel4test-driver/musllibc/build-temp/stage/lib/libc.a(__stdio_exit.o): copy relocation against non-copyable protected symbol `__stdin_used' collect2: error: ld returned 1 exit status Searching t'interwebs seems to imply this is a gnarly problem caused by the nuances of various build tools - but one that should not apply to Arm. You can summarise everything I did before the build like this: sudo apt install ninja-build libxml2-utils repo pip3 install pyyaml typing hardware pyfdt jinja2 jsonschema six future ply python3-protobuf grpcio-tools cd && mkdir xxx && cd xxx Then to follow your build repo init -u https://github.com/seL4/sel4test-manifest.git repo sync mkdir build && cd build ../init-build.sh -DPLATFORM=bcm2711 ninja And yes I know it is not supported and the BCM2711 is for the Pi 4. I am evaluating ;) Any help greatly appreciated. Thanks, Smiley

3 4

I am interested in porting LionOS to X64 architecture
by Peter Relich 14 Aug '24

14 Aug '24

Hello, I am a researcher at Intellisense Systems, Inc. We are a small business that performs R&D for the U.S. Military. We have an active contractor to build a hypervisor for a microkernel. We recently selected Sel4 as the microkernel and I learned that the Army (our customer) used a camKes implementation of a VMM to host a fork of Ubuntu, but the limitations prompted them to try another approach. I think since that time, microkit has developed quite a bit and I saw the trustworthy systems has even been developing an operating system on the Sel4 microkernel. However, LionOS appears to be developed for ARM systems as the use case. For the Army use, we are using a Nuvo7000LP: https://www.neousys-tech.com/Resource/Product_Document/Nuvo-7000LP/Nuvo-700… Which is an X64 architecture. I just started learning microkit through your available tutorials and I am aware that building a comprehensive VMM is no easy task. However, I was wondering if you had some intuition or if you could provide me an estimate of the libraries in the LionOS that I would need to adjust/redesign to make an X64 architecture fork? Is this even a feasible approach? It looks like I just need to swap out the aarch64 libraries with compatible x64 libraries and do some testing. Before I commit, I just wanted to get some advice on the endeavor. Is forking LionOS to an X64 architecture feasible, or should I start at a lower level (i.e., redesigning the vmm?) Thanks so much for your time. Respectfully, Peter Relich Research Scientist Intellisense Systems, Inc. ________________________________ The information contained in this e-mail and any attachments from Intellisense Systems may contain confidential and/or proprietary information, and is intended only for the named recipient to whom it was originally addressed. If you are not the intended recipient, any disclosure, distribution, or copying of this e-mail or its attachments is strictly prohibited. If you have received this e-mail in error, please notify the sender immediately by return e-mail and permanently delete the e-mail and any attachments.

5 5