- Devel - lists.sel4.systems

testing rust program in sel4webserver example project
by lfern70＠gmail.com 12 Feb '22

12 Feb '22

Hi, I am trying to compile a simple rust web server to be executed in the virtual machine (as lighthttpd works in this webserver project). This server works perfect (I am using qemu for testing -aarch64), but when I try to get some random bytes using the rand crate the program hangs: .... let mut key = vec![0u8; 32]; rand::thread_rng().fill_bytes(&mut key); ... Do anybody knows if this could be related to some missing settings (in qemu command line or in some device.camkes file) or some rust features that don't work in a sel4 VM?? Thanks

2 1

Call for support contract to the seL4 Foundation
by June Andronick (seL4 Foundation) 11 Feb '22

11 Feb '22

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.

1 0

picoserver and qemu
by lfern70＠gmail.com 08 Feb '22

08 Feb '22

Hi, I am trying to test picoserver app in qemu, but I am not able to connect to the echo component on port 1234. These are the steps I am following, please, let me know if I am doing something wrong. Thanks in advance: $ repo init -u https://github.com/seL4/camkes-manifest.git $ repo sync # use docker container to compile $ container @in-container:/host$ mkdir build @in-container:/host$ cd build @in-container:/host$ ../init_build.sh -DCAMKES_APP=picoserver -DPICOSERVER_IP_ADDR=127.0.0.1 -DSIMULATION=1 @in-container:/host$ ninja Everything seems to be ok, but when I tried to execute in qemu: $ sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="--enable-kvm -device intel-iommu,intremap=on,caching-mode=on -netdev user,id=network0,hostfwd=tcp::1234-:1234 -device e1000e,netdev=network0" It seems the echo component is listening on port 1234, but if I try to send data with "netcat 127.0.0.1 1234" I can't reach the echo component ...... IOMMU 0x0: enabling... enabled Booting all finished, dropped to user space Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). listener instance starting up, going to be listening on 192.168.0.21:4321 echo instance starting up, going to be listening on 192.168.0.21:1234

2 3

seL4 developer hangout/video call
by June Andronick (seL4 Foundation) 07 Feb '22

07 Feb '22

Friendly reminder that the seL4 developer hangout is on this week: - Sydney: Wed, Feb 9, 8am - Central Europe: Tue, Feb 8, 10pm - US Pacific Time: Tue, Feb 8, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, June

1 0

seL4 on TX1
by yjy 31 Jan '22

31 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 ------------------------------------------------------------------------------------------------------------------------------------------ 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? I'm sorry for sending this email again!

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