Devel

devel@sel4.systems

20 participants
1383 discussions

Build failure for sel4 on raspberry pi 5
by l4＠photiczone.com 13 Dec '23

13 Dec '23

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

2 3

Reminder seL4 developer hangout
by Birgit Brecknell 11 Dec '23

11 Dec '23

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

Question on TCB without SC in receiveSignal
by chenpingyuan＠xiaomi.com 05 Dec '23

05 Dec '23

Hello guys, I got confused on the implementation of receiveSignal in sel4 with MCS. When the notification status is NtfnState_Active, the kernel will try to donate the notification's schedule context to the thread by calling maybeDonateSchedContext. My confusion point is that: If the thread doesn't have a valid schedule context, the thread will not be able to execute, then how can this thread call receiveSignal to receive the signal? void receiveSignal(tcb_t *thread, cap_t cap, bool_t isBlocking) { notification_t *ntfnPtr; ntfnPtr = NTFN_PTR(cap_notification_cap_get_capNtfnPtr(cap)); switch (notification_ptr_get_state(ntfnPtr)) { .... case NtfnState_Active: setRegister( thread, badgeRegister, notification_ptr_get_ntfnMsgIdentifier(ntfnPtr)); notification_ptr_set_state(ntfnPtr, NtfnState_Idle); #ifdef CONFIG_KERNEL_MCS maybeDonateSchedContext(thread, ntfnPtr); // If the SC has been donated to the current thread (in a reply_recv, send_recv scenario) then // we may need to perform refill_unblock_check if the SC is becoming activated. if (thread->tcbSchedContext != NODE_STATE(ksCurSC) && sc_sporadic(thread->tcbSchedContext)) { refill_unblock_check(thread->tcbSchedContext); } #endif break; } }

2 9

seL4 summit 2024: survey about location
by Birgit Brecknell 29 Nov '23

29 Nov '23

Dear seL4 friends, With the great success of the seL4 summit 2023 behind us, we are now looking at the seL4 summit 2024! This should happen around Sep/Oct 2024. We have started investigating options for the location, and we would like your feedback. We would greatly appreciate it if you could fill in this very short survey to tell us your opinion between Abu Dhabi and Sydney: https://forms.gle/LQKSHVrqLGNqV2Ld8 Please do so by Nov 22nd 2023. Feel free to forward to anyone you believe may want to attend the summit next year. Many thanks! June & 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

2 3

How to avoid priority inversion in seL4
by chenpingyuan＠xiaomi.com 29 Nov '23

29 Nov '23

Hello experts, I'm reading the code of seL4 kernel, but I got confused how seL4 could help to avoid priority inversion. seL4 itself doesn't change the priority of TCB at the kernel level, does it mean that seL4 leaves the user level to handle priority inversion? Regards Neil.

2 2

A few questions regarding seL4
by Benjamin J. Kelly 29 Nov '23

29 Nov '23

To Whom It May Concern, My name is Ben Kelly. Myself and my partner James Briscoe - CC'd on this email - are in the beginning stages of starting a company that will host websites and web services for clients requiring high security on hardware that we control from the firmware up. We haven't decided which OS we want to use yet. Our initial goal is a customizable OS that contains only the minimum services to host a web server and nothing else. We will be evaluating the seL4 Microkernel. We're also intrigued by the possibilities of enhanced application performance and security that can be had from a unikernel approach. Is there anything that would forbid using the seL4 MicroKernel acting as a 'hypervisor/scheduler' for highly isolated and performant unikernel applications? If not, seL4 and Unikernel technology could potentially deliver the maximum amount of performance and security possible for hardware running seL4-compatible CPUs. In the following video Boyd Multerer, https://youtu.be/YG5BaoB24eA?si=TcxHq51Q5HLC0m1_ was asked the question if seL4 would "make sense on servers." Boyd replied that "I think it would but it's not something that we are targeting ... yet." He also said that "Yeah, I do think seL4 would be perfect at the bottom of the server once the multi-core thing gets figured out. But we don't need to solve that right away." Do you think seL4 is mature enough for our purpose? If we were to invest our time doing a deep dive into understanding seL4 do you know of any companies that are willing to pay for our acquired knowledge? Very Respectfully, Benjamin J. Kelly President Windsor Lake Computing LLC http://windsorlake.llc/ Sent with [Proton Mail](https://proton.me/) secure email.

3 5

Reminder seL4 developer hangout
by Birgit Brecknell 27 Nov '23

27 Nov '23

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

How to run seL4 on FVP?
by Hesham Almatary 23 Nov '23

23 Nov '23

Hello, I can build sel4test for FVP, how do I run it there? I couldn't find any documentation on that, would be great if someone could drop a command line and any required dependencies. Regards, Hesham

3 4

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

← Newer
1
2
3
4
5
6
7
8
...
139
Older →

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel