October 2019 - Devel - lists.sel4.systems

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

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

Is there a "modern" seL4 manifest/configuration that is known to run on CMA34CR?
by Nogin, Aleksey 24 Nov '19

24 Nov '19

Unless I am looking in the wrong place, all the CMA34CR support was removed in https://github.com/seL4/camkes-vm/commit/aab3478acc4705a3161f5bf59625f7c96a…. Is there something that remains? If not, what would be the best starting point to try to port a demo running on CMA34CR board from an old (early 2017) version of the sel4/camkes/etc to a recent stable release (e.g, 10.1.1)? Thanks. Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.

2 4

Fwd: port sel4 to RK3308(quad cortex-a35)
by Yun Zhou 22 Nov '19

22 Nov '19

---------- Forwarded message --------- 发件人： Yun Zhou <shiny725829(a)gmail.com> Date: 2019年10月25日周五下午9:52 Subject: port sel4 to RK3308(quad cortex-a35) To: <devel-owner(a)sel4.systems> Dear sel4 Experts How are you I found some information about sel4, and sel4 is great microkernel OS, i want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal processing. Form the Tutorials I found sel4 just support cortex-a53, I would like to ask does sel4 support cortex-a35 SMP mode. and because our application is real time audio processing so system delay must lower than 3ms and hard real-time determinism. Will sel4 support real-time signal processing? Looking forward to your reply Thanks &Kind regards Yun

2 1

releasing confidentiality
by Michael Neises 15 Nov '19

15 Nov '19

Hi, I know that seL4 provides confidentiality, which is described as a property that "means that data cannot be read without permission." Given this wording, I wonder if it is not possible to revoke those permissions in certain cases. In particular, I would like for one camkes component to be able to perform runtime measurements, such as heap analysis, on another component. Or even better, I would like for a component to be able to perform runtime measurements on a program running within the camkes linux vm. Is such a feat possible? Best, Michael Neises

3 2

Fwd: camkes vm question
by Michael Neises 15 Nov '19

15 Nov '19

Hello, In my system, sel4 is loaded by u-boot from an sd card that contains only an ELF image. I would like to store some sensitive data in plaintext for use in a non-vm component, but I worry that it can be read from the ELF image. Can this sd card data be accessed from within a linux vm instance? Or otherwise, is it certain that the vm cannot access this data? Best, Michael Neises

2 2

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

Re: [seL4] Devel Digest, Vol 65, Issue 24
by abdi mahmud haji 31 Oct '19

31 Oct '19

i am working on sel4-tutorials for the first time .i setup my machine accordingly and then when i trying to generate the tutorials like this "./init --tut hello-world" i keep getting an error message and dont know what to do or how to fix it . the error was like bellowing =================================================== abdi@abdi-HP-P-PC:~/sel4-tutorials-manifest$ ./init --tut hello-world loading initial cache file ../settings.cmake CMake Error: Error: generator : Ninja Does not match the generator used previously: Unix Makefiles Either remove the CMakeCache.txt file and CMakeFiles directory or choose a different binary directory. Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/abdi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 774, in __init__ self.wait() File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/abdi/.local/lib/python3.6/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /home/abdi/.local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-world82varrcf -C ../settings.cmake .. STDOUT: STDERR: ====================================================================== is there someone who suggests what i should do please. thanks On Sun, Oct 27, 2019 at 4:00 AM <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: releasing confidentiality > (Heiser, Gernot (Data61, Kensington NSW)) > 2. Fwd: port sel4 to RK3308(quad cortex-a35) (Yun Zhou) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sat, 26 Oct 2019 03:07:23 +0000 > From: "Heiser, Gernot (Data61, Kensington NSW)" > <Gernot.Heiser(a)data61.csiro.au> > To: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] releasing confidentiality > Message-ID: <5FEA58C5-9011-49B7-9790-28B4B54849EF(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > On 26 Oct 2019, at 08:00, Michael Neises <neisesmichael(a)gmail.com> wrote: > > > > Hi, > > > > I know that seL4 provides confidentiality, which is described as a > property that "means that data cannot be read without permission." Given > this wording, I wonder if it is not possible to revoke those permissions in > certain cases. In particular, I would like for one camkes component to be > able to perform runtime measurements, such as heap analysis, on another > component. Or even better, I would like for a component to be able to > perform runtime measurements on a program running within the camkes linux > vm. Is such a feat possible? > > Hi Michael > > seL4’s confidentiality (and other security) enforcement means that the > kernel guarantees that you can only access objects to which you have been > given explicit permission (in the form of a capability). How those > permissions are allocated is a matter of policy, the kernel doesn’t care, > it only enforces. > > In particular, it is totally possible in seL4 to give one component access > to another component’s address space, that’s for the user-level policy > framework to decide. > > Whether the present CAmkES framework supports this is a different > question, which I’ll leave to someone who’s more up to date with CAmkES > details. > > Gernot > > > ------------------------------ > > Message: 2 > Date: Sat, 26 Oct 2019 10:35:50 +0800 > From: Yun Zhou <shiny725829(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Fwd: port sel4 to RK3308(quad cortex-a35) > Message-ID: > <CAHNKqcxb7ws3MD=- > nwJka6HKEcA4hXZipJv0vdsStetJjxP-yg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > ---------- Forwarded message --------- > 发件人： Yun Zhou <shiny725829(a)gmail.com> > Date: 2019年10月25日周五下午9:52 > Subject: port sel4 to RK3308(quad cortex-a35) > To: <devel-owner(a)sel4.systems> > > > Dear sel4 Experts > How are you > I found some information about sel4, and sel4 is great microkernel OS, i > want port sel4 to RK3308(quad cortex-a35, GICv2) for real time audio signal > processing. Form the Tutorials I found sel4 just support cortex-a53, I > would like to ask does sel4 support cortex-a35 SMP mode. and because our > application is real time audio processing so system delay must lower than > 3ms and hard real-time determinism. > Will sel4 support real-time signal processing? > Looking forward to your reply > > Thanks &Kind regards > Yun >

1 0

The seL4 Foundation is coming!
by Heiser, Gernot (Data61, Kensington NSW) 25 Oct '19

25 Oct '19

Re-post from announce(a)sel4.systems<mailto:announce@sel4.systems> regarding the seL4 Foundation. We’ll start recruiting members soon. Gernot Begin forwarded message: From: Announcements about seL4 -- low volume list <announce(a)sel4.systems<mailto:announce@sel4.systems>> Subject: [seL4 Announce] The seL4 Foundation is coming! Date: 25 October 2019 at 17:09:30 AEDT To: "announce(a)sel4.systems<mailto:announce@sel4.systems>" <announce(a)sel4.systems<mailto:announce@sel4.systems>> Reply-To: <announce(a)sel4.systems<mailto:announce@sel4.systems>> Dear seL4 community, With great excitement we announce that we are in the process of setting up an seL4 Foundation, similar to foundations for other open-source projects, such as Linux and RISC-V. This will form an open, transparent and neutral organisation tasked with growing the seL4 ecosystem. It will bring together developers of the seL4 kernel, developers of seL4-based components and frameworks, and those deploying seL4-based systems. Its focus will be on coordinating, directing and standardising development of the seL4 ecosystem in order to reduce barriers to adoption, raising funds for accelerating development, and ensuring clarity of verification claims. This was originally announced at the seL4 Summit in the US last month. I apologise for the delay in this posting (side-tracked with various issues). Gernot on behalf of the Trustworthy Systems team _______________________________________________ Announce mailing list Announce(a)sel4.systems<mailto:Announce@sel4.systems> https://sel4.systems/lists/listinfo/announce

1 0

Upcoming release planned
by Mcleod, Kent (Data61, Kensington NSW) 23 Oct '19

23 Oct '19

Hi all, I'm announcing that we are planning a new versioned release of seL4, capDL and CAmkES in about 3 weeks - around 11 November. We want to provide an opportunity for people to report issues or provide patches that can be fixed/incorporated for the versioned release. The last versioned release occurred almost 12 months ago and we plan on returning to a shorter release cycle of several weeks per cycle. Feel free to raise new issues across our GitHub repositories and we will also try to address any currently outstanding issues that have been neglected. Here is a highlight list of what changes are going to be in the upcoming versioned release: ## seL4 - Add GrantReply access right for endpoint capabilities. `seL4_Call` is permitted on endpoints with either the Grant or the GrantReply access rights. Capabilities can only be transferred in a reply message if receiver's endpoint capability has the Grant right. The GrantReply access right allows endpoints to be configured for two-way communication without also providing the right to transfer authority via capability transfer. - Merging of the mixed-criticality scheduling (MCS) branch into master. Previously the MCS branch only received versioned releases. Merging it into master under a build configuration (KernelIsMCS) makes it easier to keep up to date with changes to master and other tooling/libraries in-between versioned releases. Verification work is still on-going. - Continued development of the newly added RISC-V platform to support in-progress verification. - Auto-generation of Arm and RISC-V kernel platform definitions from a provided devicetree as well as support for passing a devicetree to the root task via the seL4_BootInfo structure. Interrupt controllers, timers and other devices required by the kernel can also be selected in the devicetree provided that the kernel already has a compatible driver. - Support for AArch64 hypervisors is in active development with initial support for Cortex-A53 and Cortex-A57 cores - De-duplicating kernel platform configurations and code in order to reduce the effort required to support additional platforms. - New platforms added: BeagleBone Blue, Hardkernel ODROID-C2, Freescale i.MX8M, i.MX8M Mini, Arm FVP (based on foundation-v8-gicv3.dts), QEMU ARM virt platform (with 3 CPUs: cortex-A15, cortex-A53 and cortex-A57) and possibly PINE64 ROCKPro64. - Implement RFC-3: Cross-platform thread-local storage (TLS) support. https://sel4.atlassian.net/browse/RFC-3. This provides a way for a thread to access or modify a thread-specific pointer without requiring a capability to itself. On architectures that don't provide unprivileged write access to this pointer a new syscall `seL4_SetTLSBase` is added that performs this operation. The kernel no longer reserves a register for holding a thread's IPC buffer and it is the thread's responsibility for managing this. `libsel4` declares a pointer to a thread's IPC buffer using a `__thread` keyword and a new user-level library `sel4runtime` can be used to provide a minimal supporting runtime. Additionally, the IPC buffer's userData field is no longer used for holding a pointer to the IPC buffer. - Better SMP Arm IRQ handling: Support is added for creating IRQ handler capabilities for core-local interrupts (PPIs) for each core and for also specifying a target core for global interrupts (SPIs) via the new invocation `IRQControl_GetTriggerCore`. - Merge ARCH_Page_Remap functionality into ARCH_Page_Map. Remap was used for updating the mapping attributes of a page without changing its virtual address. Now ARCH_Page_Map can be performed on an existing mapping to achieve the same result. The ARCH_Page_Remap invocation has been removed from all configurations. - Support for compiling the kernel with Clang. For a more complete list see the CHANGES file in the seL4 repository. ## CAmkES - Support for the new seL4 Endpoint GrantReply access right for CAmkES connector types. This allows multi-sender/single-receiver connectors such as `seL4RPCCall` that don't also provide the ability for arbitrary capability transfer from sender to receiver. Previously the `seL4RPC` connector was used instead of `seL4RPCCall` to create an Endpoint without a Grant right. This used a combination of `seL4_Send` and `seL4_Wait` to communicate without the ability for capability transfer, however this only supports a single sender and single receiver. - Better support for configuring components with a provided devicetree. This support includes adding a seL4DTBHardware connector that can be used instead of seL4HardwareMMIO and seL4HardwareInterrupt and can be used to extract IRQs and MMIO register information out of the devicetree node rather than specifying the info directly. This connector can also be used to access a devicetree within a component at for querying further device information. There is also a connector seL4VMDTBPassthrough that can be used for specifying devices to pass through to a `camkes-arm-vm` VM component. - CapDL Refinement framework. These are generated Isabelle proof scripts to prove that the generated capDL respects the isolation properties expected from its CAmkES system specification. Only the AARCH32 platform is supported. The generated capDL is a specification of seL4 objects and capabilities that will implement the CAmkES system specification. This specification is then given to a system initialiser to create the objects and capabilities and load the system. - Support for RISC-V systems. ## capDL capDL refers to the capability distribution language and tools contained in https://github.com/seL4/capdl. CAmkES uses these tools for generating a capDL specification and then uses the `capdl-loader-app` as it's seL4 root task for initialising the system. As we are in the process of developing additional loaders we are going to start providing versioned releases of the capDL set of tools. Changes since the last seL4 release: - Support for the new seL4 Endpoint GrantReply access rights in the CapDL spec. Endpoint capabilities in the capDL spec can now have Read, Write, Grant and GrantReply rights. - Static Untyped allocation of spec objects. This is support for performing offline pre-allocation of spec objects to the Untyped objects that are expected to be provided in the seL4_BootInfo by the kernel. Having a static allocation of spec objects to Untypeds allows for more simple loaders that do not have to perform resource allocation during initialisation. This feature is optional and a spec is still valid if objects aren't allocated from Untyped objects. - Support for loading RISC-V systems.

1 0