Devel January 2022

devel@sel4.systems

13 participants
13 discussions

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

seL4 on TX1
by yjy 31 Jan '22

31 Jan '22

2 3

Re: seL4 on TX1
by 杨竣轶 30 Jan '22

30 Jan '22

I did’t get any difference about my error except the address. Is my Uboot precedure errored? 从 Windows 版邮件发送

1 0

seL4test on Nvidia TX1
by yjy7894＠126.com 28 Jan '22

28 Jan '22

Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ Help me! I am running sel4test on my TX1 according to the official tutorial, but I get a problem again and again. For the newly purchased TX1, I directly connected my Ubuntu host with UART serial port. At the same time, I follow this instruction ( https://docs.sel4.systems/Hardware/jetsontx1.html ), pulled the latest sel4test project code, successfully ran ninja command and built images "sel4test-driver-image-arm-tx1". Everything seemed to be going very smoothly. I use the newly purchased SanDisk 64GB SD card to boot my image, which has been formatted in ext4 format. Then I use command `sudo screen / dev / ttyusb0 115200` to open the UART serial port. After pressing and holding the power key for 1 second, and TX1 starts. Then I hit the Enter key to make TX1 cancel the auto boot default image and enter the u-boot interactive command line. Then, according to the instruction, under uboot, I typed the following command to load the image and start from the address 0x82000000: ``` ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 go 0x82000000 ``` Finally, I failed to start sel4test as I wanted. After many repetitions, I got the same error. This is my output： ------------------------------------------------------------------------------------------------------------------------------------------ Tegra210 (P2371-2180) # ext4load mmc 1 0x82000000 sel4test-driver-image-arm-tx1 5247256 bytes read in 260 ms (19.2 MiB/s) Tegra210 (P2371-2180) # go 0x82000000 ## Starting application at 0x82000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p1 paddr=[80a57000..80f58117] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 80b825e0. Loaded DTB from 80b825e0. paddr=[8023d000..8024afff] ELF-loading image 'kernel' to 80000000 paddr=[80000000..8023cfff] vaddr=[ffffff8080000000..ffffff808023cfff] virt_entry=ffffff8080000000 ELF-loading image 'sel4test-driver' to 8024b000 paddr=[8024b000..80661fff] vaddr=[400000..816fff] virt_entry=40f0b8 Enabling MMU and paging Jumping to kernel-image entry point... Warning: gpt_cntfrq 19200000, expected 12000000 Bootstrapping kernel available phys memory regions: 2 [80000000..ff000000] [100000000..180000000] reserved virt address space regions: 3 [ffffff8080000000..ffffff808023d000] [ffffff808023d000..ffffff808024b000] [ffffff808024b000..ffffff8080662000] seL4 failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap' at /home/yjy/Desktop/sel4-rpi/sel4test_newv2/kernel/src/object/cnode.c:426 in function cteInsert halting... Kernel entry via Interrupt, irq 0 ------------------------------------------------------------------------------------------------------------------------------------------ I'm about to collapse. I really need your help. How can I solve this problem? 1. Why did I get this warning？ "Warning: gpt_cntfrq 19200000, expected 12000000" , It exists in this file "/sel4test/kernel/src/drivers/timer/generic_timer.c:21" 2. About reporting errors "failed assertion 'cap_get_capType(destSlot->cap) == cap_null_cap'". I found that the variable "(slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] " is equals to 0xffffffffffffffff, so that the cap_get_capType(destSlot->cap) <=> (slot_ptr_t) (rootserver.tcb) ) -> cap.words[0] & 0x1full != 0 . I guess it caused the mistake, but i don't know why. I'm about to collapse. I really need your help. How can I solve this problem?

1 0

Re: seL4 developer hangout/video call
by Isaac Beckett 27 Jan '22

27 Jan '22

Hello all! If you’re reading this at the time it was sent, then the developer hangout is in roughly an hour. See you there! > > On Jan 25, 2022, at 8:02 PM, devel-request(a)sel4.systems wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe 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: seL4 developer hangout/video call (Gerwin Klein) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 25 Jan 2022 06:52:21 +0000 > From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] Re: seL4 developer hangout/video call > To: devel <devel(a)sel4.systems> > Message-ID: <7F36F76C-E596-4A51-9419-785AB723CC03(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > Just a reminder that seL4 dev hangout is not tomorrow, but shifted by one day. > > Cheers, > Gerwin > >> On 23 Jan 2022, at 18:13, Gerwin Klein <kleing(a)unsw.edu.au> wrote: >> >> An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia. >> >> This means, we're meeting on Wed for Europe/US and on Thu for Australia: >> >> - Sydney: Thu, Jan 27, 8am >> - Central Europe: Wed, Jan 26, 10pm >> - US West Coast: Wed, Jan 26, 1pm >> >> Zoom link: https://unsw.zoom.us/j/82640784431 >> >> Cheers, >> Gerwin >> > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > ------------------------------ > > End of Devel Digest, Vol 135, Issue 2 > *************************************

3 2

📣 2022 SUMMIT - Trusted Computing Center of Excellence
by Griffiss Institute 27 Jan '22

27 Jan '22

NEXT WEEK! Register TODAY! NEXT WEEK! | SUMMIT 2022 View email in browser https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… REGISTER NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) NEXT WEEK! 2022 SUMMIT BEGINS JAN 31! The Trusted Computing Center of Excellence (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) (TCCoE) is excited to announce that our annual Summit (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) will be held virtually on January 31 - February 3, 2022! The TCCoE has been established with support from DARPA (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) , AFRL (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) , and the Griffiss Institute (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) . Many of you may be familiar with the annual seL4® Summit, which we’ve successfully hosted for the past three years in coordination with the seL4 Foundation. Planning for the next annual seL4 Summit has begun under the leadership of seL4 Foundation, tentatively scheduled for October 2022 at a site in Europe. Beginning in January 2022, the TCCoE will host an annual Summit in the US, a complementary multi-day event focused on trusted computing technologies with a current emphasis on the secure embedded L4 (seL4) microkernel. seL4 is the world’s first open source operating system kernel with an end-to-end proof of implementation correctness and security enforcement. The main theme of this year’s TCCoE Summit is to provide a forum to discuss measurable security, resilience and assurance, via organic integration of hardware and software security features, for current and future platforms and systems. Specifically, the Summit scope includes, (but is not limited to), discussions on hardware security features, kernel, hypervisor and Virtual Machine Managers (VMMs), operating systems, containers, software security, etc. The TCCoE Summit will provide attendees the opportunity to attend presentations by government, industry, and academia experts; interact with discussion panels; and obtain tutorial training related to the seL4 microkernel. Come join us for 4 days packed with thought provoking keynotes, insightful presentations, lively panel discussions, and educational tutorials - an event that anyone interested in embedded systems and trust-based computing cannot miss! We look forward to your attendance! REGISTRATION IS LIVE! Registration | 13 January 2022 - 3 Feb 2022 | $250 (US) REGISTER NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) REMINDER #1: Some levels of TCCoE Membership include discounted and free attendance at the Summit, so check with your organization about membership status! REMINDER #2: Tutorials will take place on Monday, January 31, starting at 8:00 am EST. These tutorials are included with your 2022 TCCoE Summit registration. You can join these one day tutorials for free just by registering below. TUTORIAL REGISTRATION (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) MEMBERSHIP Have you and/or your company considered Trusted Computing Center of Excellence membership? Through membership, you gain an opportunity to influence the CoE’s priorities and technical direction, share ideas and network among peers in our community, and gain leverage from the latest trusted computing (e.g. seL4®) based innovations. The specific member benefits vary by membership class, but in general, membership benefits include: * Complimentary (or discounted) registration fee for CoE workshops and events * Advertising on the CoE’s website, in CoE publications, and at CoE sponsored events * Voting privileges for the election of the CoE Board of Directors, and other matters * Representation on CoE Committees * Tutorials for developers of trusted systems * Connect and collaborate securely and privately with other CoE members (chat, etc.) * Curated Software Distributions * Access to the CoE Private Code Repository (ITAR restrictions may apply) JOIN NOW! (https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498…) https://griffissinstitute.us6.list-manage.com/track/click?u=f0470275265f498… seL4 is a trademark of LF Projects, LLC. ============================================================ Copyright © 2022 Griffiss Institute, All rights reserved. You are receiving this email because of your interest in the Trusted Computing Center of Excellence.. Our mailing address is: Griffiss Institute 592 Hangar Rd Rome, NY 13441-4506 USA Want to change how you receive these emails? You can ** update your preferences (https://griffissinstitute.us6.list-manage.com/profile?u=f0470275265f4981c83…) or ** unsubscribe from this list (https://griffissinstitute.us6.list-manage.com/unsubscribe?u=f0470275265f498…)

1 0

seL4 developer hangout/video call
by Gerwin Klein 25 Jan '22

25 Jan '22

Hi seL4 devs, a few of us thought it might be nice to talk more directly from time to time rather than only via pull requests, so we're trialling a seL4 developer hangout/video chat. The idea for this is to be: - informal, about 1h - for technical discussions about seL4 and related repositories - anyone can join - every two weeks, initially for 3 times, then we can decide how we like it At least one or two technical steering committee (TSC) members will try to be at every one of these, but these are not TSC meetings where formal decisions are made, just technical discussions about whatever people have on their minds. To provide a starting topic, one thing we'd be interested in is: seL4 boot code There have been quite a few pull requests in that area, and it'd be nice to know what people's plans are and how we can keep this part of seL4 high assurance while making it more flexible. Other topics for future meetings could be better support for other language bindings (e.g. Rust), any RFCs that are open or people are thinking about opening, or just discussions about current pull requests or issues. The first hangout is on - Sydney: Wed, Nov 3, 8am - Central Europe: Tue, Nov 2, 10pm - US East Coast: Tue, Nov 2, 2pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

2 9

Re: seL4 developer hangout/video call
by Isaac Beckett 25 Jan '22

25 Jan '22

Other US time zones: PST (West Coast): 1pm MST (Mountain Time): 2pm CST (Central Time): 3pm EST (East Coast): 4pm We have a lot of time zones here, it’s a bit of a pain sometimes. > > On Jan 23, 2022, at 8:01 PM, devel-request(a)sel4.systems wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe 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: seL4 developer hangout/video call (Gerwin Klein) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 23 Jan 2022 07:13:27 +0000 > From: Gerwin Klein <kleing(a)unsw.edu.au> > Subject: [seL4] Re: seL4 developer hangout/video call > To: devel <devel(a)sel4.systems> > Message-ID: <678C2D4C-EEE5-4D79-82BD-256BC78B3BFC(a)unsw.edu.au> > Content-Type: text/plain; charset="us-ascii" > > An earlier-than-usual heads-up that the seL4 developer hangout this week will be shifted by one day, because of the public holiday in Australia. > > This means, we're meeting on Wed for Europe/US and on Thu for Australia: > > - Sydney: Thu, Jan 27, 8am > - Central Europe: Wed, Jan 26, 10pm > - US West Coast: Wed, Jan 26, 1pm > > Zoom link: https://unsw.zoom.us/j/82640784431 > > Cheers, > Gerwin > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > ------------------------------ > > End of Devel Digest, Vol 134, Issue 1 > *************************************

2 1

Sel4 Vmm Project Supporting on memory resources configure
by Tao Heng 陶恒-SW 19 Jan '22

19 Jan '22

Hi Sel4: While portinging Android Guest based on Sel4 Vmm project, I met some problems .In my porting steps, I increased the reserved memory for Android Guest to 2G on my platform. Then there were some parts of Sel4 Vmm project that confused me. 1. the principle to determin the static pool size for bootstrap with allocman n In bootstrap.h, I found your explanation for the value that it is based on the work with trial and error.Is that still the case? n If I incease this size, the frame_vm0_group_bin showed in vm_minimal.cdl file will obviously increase together.What’s the relationship of the two value? 2. How is the staic memory pool created? Is this memory pool created from untyped memory, so as treated untyped object? 3. the principle to determin the vm.simple_untyped24_pool size and nums n What’s the usage of the untyped_pool memory? n How can I make sure a reasonable size and nums of this value ? Much apprecitated, if you can give some feedbacks. Tao Heng | Taoer * +8618800230581 * taoheng(a)saicmotor.com<mailto:taoheng@saicmotor.com> Basic Software Platform SAIC Motor Z-ONE Software Company Auto Innovation Park | 201 Anyan Road, Jiading, Shanghai 邮件免责申明 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

Virtual Machine and scheduling query
by Sidhartha 12 Jan '22

12 Jan '22

Hi, I am a 2nd-year grad student at the Systopia Lab in UBC. I am using seL4 for the OS research project at I have a few independent questions: 1. Virtual Machines can be implemented with different levels of support from the hardware. If we talk about x86_64, in the most basic terms, you could have VMs without or without VT-X extensions. Looking at the resources available on the seL4 site, I think the given VMM libraries assume VT-X. Is there an example that does not use VT-X? 2. The scheduler inside seL4 is relatively simple. I have heard(Thanks Nick!) that if a complicated scheduling policy is desired, it can be done in userspace. A user-level component that has the capabilities to all the TCB's can play with the priority, resume/pause, and achieve any arbitrary scheduling. Is there an example available which I could look at? 3. I would like to implement a new functionality of memory quota, where different user-apps can be assigned memory quota and not just the physical pages. Does such a functionality belong in the kernel or the userspace component(say memory quota manager)? In the latter case, it would be just an endPoint capability to the quota manager service, so how does one split it - say split a quota of 100MB into two separate 50MB quotas. This is more a generic micro-kernel query rather than seL4 specific, but any insights would help. Thanks, Sid sid-agrawal.ca

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel January 2022