- Devel - lists.sel4.systems

vm_multi usage
by Michael Neises 07 Mar '22

07 Mar '22

Hi, I'm just beginning to use multiple VMs at once, and I have a simple question. When I simulate my image, two VMs are running, and I get a terminal interface to one of them. Can I also switch my terminal to interface with the second VM? Cheers, Michael Neises

2 1

Re: I Have some questions about the domain mechanism in the seL4
by Isaac Beckett 07 Mar '22

07 Mar '22

> Date: Sat, 5 Mar 2022 19:15:05 +1100 > From: Kent Mcleod <kent.mcleod72(a)gmail.com> > Subject: [seL4] Re: I Have some questions about the domain mechanism > in the seL4 > To: 603644559(a)qq.com > Cc: devel <devel(a)sel4.systems> > Message-ID: > <CA+-ozWdgMgBin34WBUoVL+uHSNfU=e852ekPgrNGZ5J7+nyN0g(a)mail.gmail.com> > Content-Type: text/plain; charset="UTF-8" > >> On Sat, Mar 5, 2022 at 6:11 PM 603644559--- via Devel >> <devel(a)sel4.systems> wrote: >> >> For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… >> But i still do not know the purpose of adding the domain mechanism in seL4, >> Can anyone explain what kind of requirement led to the design of the domain mechanism? >> Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism. > > It was added in order to enable the completion of the info-flow proofs. > >> From the infoflow proof paper > (https://trustworthy.systems/publications/nicta_full_text/6464.pdf) > where it is called the partition scheduler: > "Similarly, the original seL4 scheduler, before partition > scheduling was implemented, was known not to enforce > isolation. We could not prove information flow security until > we had fully and correctly specified the partition scheduler > in the updated abstract specification. Proving information > flow security then required us to show that the scheduler’s > choice about which partition to schedule next can never be > affected by any other partition, as one would expect." Hello! It was my understanding that seL4 used to not have an in-kernel scheduler, and scheduling was up to the root task. How did that work? And why was the choice made to add the MCS features? Basically, why the change from having scheduling in the kernel vs. in userspace? It’s probably more convenient, especially since most operating systems are used to having scheduling in the kernel itself (so easier for people to think about). There are probably more technical reasons too. What are those?

2 3

I Have some questions about the domain mechanism in the seL4
by 603644559＠qq.com 07 Mar '22

07 Mar '22

For some reason, i m learning the scheduling module in seL4. I have read the manual and the source code, and i have already read the answer in the link https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/VYRTG3… But i still do not know the purpose of adding the domain mechanism in seL4, Can anyone explain what kind of requirement led to the design of the domain mechanism? Please explain it more specifically, and it would be best if there were relevant documents and papers on the domain mechanism.

2 2

Reminder: sel4 developer hangout
by Birgit Brecknell 07 Mar '22

07 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 1pm (There are too many time zones in the world to cite them all :)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Questions about shared page tables and Intel's MPK
by Sid Agrawal 05 Mar '22

05 Mar '22

Hi, I have a couple of questions about the virtual memory subsystem in seL4. 1. Intel's Memory Protection keys let a process restrict the access to given virtual address ranges based on a key. This key is the bit 62:59 of the virtual address. It is stored in the PTE of the level 4/5 Page Table. I want to use this feature in my project. Does seL4 support the setting of Memory Protection keys for virtual addresses? I couldn't find any mention of it in the source. I understand that if I use the current API of "seL4_X86_PageTable_Map" with those higher bits of the vaddr set, the kernel will ignore them. Is my understanding correct? Furthermore, was a decision made not to support MPK at some point? 2. As per section 7.3 of the seL4 manual, seL4 doesn't allow sharing of page tables. I am trying to understand the reasoning behind this. Was this done to aid verification? Thanks, Sidhartha S Agrawal

3 4

libsel4muslcsys: Error attempting syscall 215
by skydivebcn＠gmail.com 05 Mar '22

05 Mar '22

Hi guys, I was trying to boot a custom Linux 4.9.302 Kernel and fot this horrible message: "libsel4muslcsys: Error attempting syscall 215" hugo@dev:~/seL4/sel4webserver_hugusmaximus_fork/build$ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off" [sudo] contraseña para hugo: ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=2048 -netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -kernel images/capdl-loader-image-arm-qemu-arm-virt ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[61bf9000..631120af] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 61d3a2b8. Loaded DTB from 61d3a2b8. paddr=[60243000..60244fff] ELF-loading image 'kernel' to 60000000 paddr=[60000000..60242fff] vaddr=[ff8060000000..ff8060242fff] virt_entry=ff8060000000 ELF-loading image 'capdl-loader' to 60245000 paddr=[60245000..617fdfff] vaddr=[400000..19b8fff] virt_entry=408f38 Enabling hypervisor MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/205 T0xff80bf815400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>> Loading Linux: 'linux' dtb: 'linux-dtb' install_linux_devices@main.c:655 module name: map_frame_hack install_linux_devices@main.c:655 module name: init_ram install_linux_devices@main.c:655 module name: cross_vm_connections libsel4muslcsys: Error attempting syscall 215 libsel4muslcsys: Error attempting syscall 215 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x8020000 as this is purely an seL4 error message (musl libc seL4 code?) then I would appreciate any hint about what can be going on. P.S.: I have run my seL4 qemu aarch64 with several Linux kernel versions and never had this problem until now.

2 1

Sel4 VMM Virtio Net Related Porting on Other SOC
by Tao Heng 陶恒-SW 04 Mar '22

04 Mar '22

Hi everyone , Background: I was porting vm_virtio_net project on other platforms with Cortex-A55. I met a run error with : ----------------------------------------- Unhandled offset of 0x14 of size 1, writing 0x2 Assertion failed: !"panic" (/home/kuang/workspace/penoy/system/core/seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109) --------------------------------------------------- While it ran well on qemu with linux kernel version 4.9.189, my linux kernel version for the SOC is 4.14.61. If I replaced the qemu linux kernel with my kernel, the vm_virtio_net project also ran well on the qemu platform. To my analyzation, your virtio_net driver should be able to support for my platform. Is this related to my dts configuration for PCI node? 邮件免责申明 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

seL4 Native Web-browser
by Daniel Douglas Dyrseth 04 Mar '22

04 Mar '22

Hi, everyone What parts are needed besides seL4 to get a fully functioning Chromium browser running in a Wayland server? (No virtual OS inside seL4). I'm talking native seL4 OS capable of running Chromium with all features. Hoping for some insightful answers, and at least a list from a Pro - of the minimum parts needed for this. Regards, Daniel Douglas Dyrseth

2 1

Call for support contract to the seL4 Foundation
by Birgit Brecknell 25 Feb '22

25 Feb '22

A friendly reminder that bids are due before March 4th, 2022 AOE: 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. --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au seL4 Foundation, birgit(a)sel4.systems 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

Re: Announcing Neptune OS release v0.1.1: A Windows NT personality for seL4
by Chang Liu 23 Feb '22

23 Feb '22

Thank you both for the discussion on licensing. Seems that GPLv3 is a good choice for now. Wikipedia seems to claim that ReactOS is licensed under "GPLv2 or any later version" but I didn't find this on the reactos source code itself. If the ReactOS foundation has an objection later I can always change it to v2. Best, Chang On Wed, Feb 23, 2022 at 12:09 AM G. Branden Robinson < g.branden.robinson(a)gmail.com> wrote: > Hi Chamg, > > At 2022-02-22T23:29:21-0500, Chang Liu wrote: > > I just added a LICENSE file which is GPLv3. > > Good choice! > > > I'm honestly not sure what the difference between GPLv2 and GPLv3 > > There are modest differences, but the general thrust of both versions of > the license is the same: guaranteed access to source code under a "share > and share alike" principle. > > > is so I went with the latest version (I assume they are compatible?) > > Technically, no. But most GPLv2 software is licensed under terms that > allow promotion of the license to "any later version". One famous > example of an exception that is GPLv2-only is the Linux kernel. > So is seL4 itself[1]. Consider whether you expect to need to share code > with a GPLv2-only project. (Even if you do, I would only revisit your > decision once concrete code-sharing is imminent.) > > You're not stuck with a choice of a single license forever. The GPLv3 > is a good selection to start with (in my opinion) because most > organizations that would like to exploit a work for proprietary > advantage are allergic to that license. > > You can always relicense a work under more permissive terms later if > doing so would align better with your goals. Going from more permissive > terms (like a BSD-style license) to a copyleft (like any version of the > GPL) can be impractical, or result in unintended consequences, because > it is arguably impossible to rescind the permissive license on the older > versions of the code--unless you have an Apple- or Oracle-sized budget > for lawyers to intimidate rivals maintaining the old code base. > > There is probably a better forum for licensing discussions, but my view > is that you've made a perfectly reasonable choice, one that situates > your project squarely and clearly within the Free Software community, > while still leaving you the option to reconsider later. > > Regards, > Branden > > [1] https://microkerneldude.org/2019/12/09/what-does-sel4s-license-imply/ >

1 0