- Devel - lists.sel4.systems

Information for Smmuv3 support of Sel4
by Tao Heng 陶恒-SW 06 May '22

06 May '22

Hi, list We are trying to porting Sel4 Vmm project on our platform.But we found there was no information about smmuv3 support of Sel4. Do you have some related development work for supporting this? Or can you give us some advice for supporting Smmuv3 on Sel4? 邮件免责申明 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

One week left to propose a talk at the seL4 summit 2022!
by June Andronick (seL4 Foundation) 06 May '22

06 May '22

A reminder that you have until Monday 9th of May 2022 to propose a talk for the seL4 Summit 2022 :) http://sel4.systems/news/2022 <http://sel4.systems/news/2022> http://sel4.systems/Foundation/Summit/ <http://sel4.systems/Foundation/Summit/> http://sel4.systems/Foundation/Summit/cfp <http://sel4.systems/Foundation/Summit/cfp>

1 1

Reminder seL4 developer hangout
by Birgit Brecknell 02 May '22

02 May '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 4, 7am (UTC), Topics: (open) * Sydney: Wed, May 4, 5pm * Central Europe: Wed, May 4, 9am * US Pacific Time: Wed, May 4, 12 midnight Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

1 0

The seL4 Summit 2022 will be in Munich, Germany, on 10-12 Oct 2022
by June Andronick (seL4 Foundation) 29 Apr '22

29 Apr '22

It is our pleasure to confirm that the seL4 Summit 2022 will be in: Munich, Germany in the week of Oct 10th, 2022 It will be hosted by seL4 Foundation member Hensoldt Cyber. It will be a hybrid in-person/online event (if you'd like to propose a talk to be delivered remotely, please notify it in the submission). Remember that you have until Monday 9th of May 2022 to propose a talk. https://sel4.systems/news/2022 https://sel4.systems/Foundation/Summit/ https://sel4.systems/Foundation/Summit/cfp

1 0

Sending extraCaps over IPC | Unable to send 2 caps
by Sid Agrawal 28 Apr '22

28 Apr '22

Hello seL4 devs and users, I am trying to send two capabilities from one process to another via the extraCaps mechanism in the IPC. I can get it working when I send just 1 cap, but when I am sending 2 caps, the 2nd one never makes it. The extraCaps field on the receiver side is somehow always 1. Looking at the seL4 manual, I understood that I could send more than 1 capability via an IPC. But since on the receiver side, I can only specify one receive slot, I assumed that if more than 1 capability is received, it will be put in the consecutive slots. Not sure if this is a valid assumption. Looking at kerne/libsel4/include/sel4/constants.h <https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/constants.h#L…>, I see that seL4_MsgMaxExtraCaps is set to 2, so I think I should be able to send 2 caps. I have spent about 3 days trying to make this work and thought that at this stage, it would be best to ask :) My C code on the sender side looks something like this: seL4_CPtr cap1 = <alloc some capability> seL4_CPtr cap2 = <alloc some capability> seL4_SetMR(0, 0xabcd); seL4_SetCap(0, cap1); seL4_SetCap(1, cap2); seL4_MessageInfo_t tag = seL4_MessageInfo_new(0, 0, 2, 1); tag = seL4_Call(receivers_ep_cap, tag); On the receive side, the code looks something like this: /* Allocate one csapce slot */ cspacepath_t received_cap_path_1; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_1); <- slot = 2786 assert(error == 0); /* Allocate another csapce slot */ cspacepath_t received_cap_path_2; error = vka_cspace_alloc_path(simple-vka, &received_cap_path_2); <- slot = 2785(somehow decreasing) assert(error == 0); /* Since the allocated slots are decreasing in count, I pick the lesser one as my first slot * assuming that if more than 1 cap is received it will be put in the next slot */ seL4_CPtr min_cptr = MIN(received_cap_path_1.capPtr, received_cap_path_2.capPtr); seL4_SetCapReceivePath( /* _service */ received_cap_path.root, /* index */ min_cptr, /* depth */ received_cap_path.capDepth); tag = recv(&sender_badge); assert(seL4_MessageInfo_get_extraCaps(tag) == 2); <--- This asser fails. Thanks again!! Sid Graduate Student @ UBC

2 2

RTReply and cap xfer
by Sam Leffler 21 Apr '22

21 Apr '22

The kernel supports attaching a capability to an RTReply xfer. sel4test even checks this WAI. But capdl doesn't seem to support it as I see no way to express the set of rights associated with a capability to an RTReply object. I added capdl support so I can mark the Grant right and verified cap xfer works. TWas this intentional? -Sam

1 0

Running vm_multi app on qemu-arm-virt platform, udhcpc can not return
by ybbekele＠aggies.ncat.edu 21 Apr '22

21 Apr '22

Hi, I tried to build vm_multi for qemu-arm-virt using the procedures in this link https://docs.sel4.systems/projects/camkes-vm/. After building, I used the generated simulation file to do ./simulate in my build directory. After displaying 'welcome to buildroot', the console always prints the log "udhcpc: sending discover",which indicates udhcpc can not return. The related log was shown below: Starting syslogd: OK Starting syslogd: OK Starting syslogd: OK Starting klogd: OK Starting klogd: OK Starting klogd: OK Running sysctl: OK Running sysctl: OK Running sysctl: OK Initializing random number generator... [ 7.195263] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.315113] random: dd: uninitialized urandom read (512 bytes read) done. Initializing random number generator... [ 7.300770] random: dd: uninitialized urandom read (512 bytes read) done. Starting network: OK Starting network: OK Starting network: OK udhcpc: started, v1.31.0 udhcpc: started, v1.31.0 ifconfig: SIOCGIFFLAGS: No such device [ 9.077855] random: mktemp: uninitialized urandom read (6 bytes read) [ 9.177878] random: mktemp: uninitialized urandom read (6 bytes read) Welcome to Buildroot udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover udhcpc: sending discover As the simulation process progresses there was an error: _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0x10080000 alloc_vm_device_cap@main.c:938 Grabbing the entire cap for device memory alloc_vm_device_cap@main.c:941 Failed to grab the entire cap My question is: 1. Is the two things have dependencies (The error and the hang at booting the system up)? 2. How can this issue be solved? 3. Is this issue related to the TimeServer component being imported to Qemu (as this is indicated as a requirement to run multi_vm on qemu-arm-virt)? Thank you for your time

1 0

Why vppi is sent from kernel to vmm by fault endpoint but not by notification ?
by wtliang785 21 Apr '22

21 Apr '22

hello devel, Why vppi , such as vtimer interrupt to guest, is sent from kernel to vmm by fault endpoint but not by notification? I see that spi to guest is sent from kernel to vmm by notification. thank you.

1 0

Reminder seL4 developer hangout/video call
by Gerwin Klein 19 Apr '22

19 Apr '22

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, Apr 19, 10pm (UTC) * Sydney: Wed, Apr 20, 8am * Central Europe: Wed, Apr 20, 12 midnight * US Pacific Time: Tue, Apr 19, 3pm Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Gerwin

1 0

Re: Combatting spam on this list
by Isaac Beckett 13 Apr '22

13 Apr '22

Thanks Peter! In my experience posts like that, linking to pornographic websites, are not made by humans anyway, but rather by bots. I don’t think this will effect humans too much except at the very beginning. It may make sense to implement a different captcha, as often the developers of those bots can outsource solving common captcha providers to underpaid humans. Using an uncommon or home-grown captcha solution will make it less likely that bots will be able to get around them using that method. And attacks like these aren’t targeted, usually, so I doubt the bot writers will adapt for one specific mailing list. That will stop bots from signing up in the first place, hopefully. We could also maybe report abuse of free email services like Gmail or Hotmail or similar in a semi-automated fashion. Would not surprise me if there is some sort of API for that. But on the other hand with the way those companies work it could be a waste of time and effort, since they might not do anything. And it may also make sense to keep track of which domains non-malicious users are sending email from. That way we can ban entire domains without worrying about getting rid of legitimate users unintentionally. For example, a small webmail service that we may not realize is a public email service at first, could be used by both a malicious user and a legitimate one. That way we’re only banning domains controlled by spammers exclusively. There’s lots of resources for this stuff thankfully, you can go on a whole tangent reading about email spam prevention on Wikipedia. I wish you luck with figuring out how to stop this annoying nonsense.

3 2