- Devel - lists.sel4.systems

Camkes-vm-linux tutorial
by felicianidaniele＠gmail.com 26 Oct '23

26 Oct '23

Hi, I modified the vm_tutorial.camkes file to obtain two VMs. It works but I would like to see the two virtual machines on two different consoles. Is it possible? Thanks Daniele

1 0

vm-minimal on raspberry pi4
by felicianidaniele＠gmail.com 19 Oct '23

19 Oct '23

Hi everyone, I would like to run vm-minimal and vm-multi (camkes-vm-manifest repo) on raspberry pi 4 4gb RAM. Can someone help me? Thanks Daniele

1 0

Running Sel4 on Rasberry pi 4 4 gb RAM
by felicianidaniele＠gmail.com 18 Oct '23

18 Oct '23

Hello, i'm trying to upload seL4 ( seL4test-driver-image-bcm2711 image) on raspberry pi 4 but i'm encountering two different errors: 1. If I follow the website procedure and upload the sel4test image into the address 0x10000000 the error is : “Reading file would overwrite reserved memory” 2. If I try to upload the image into 0x1000000 I read the following error: “sel4 failed assertion ‘isSchedulable(candidate)’ at /kernel/thread.c can someone help me? Thanks Daniele

2 2

Help with navigating the l4v repository
by Typaldos, Athanasios 18 Oct '23

18 Oct '23

Hello, I am from Lin Zhong’s group at Yale University and I am currently looking at the seL4 specifications and proofs. I am interested in finding the invariants at the abstract level regarding the capability management (CNode and CSpace). I would need some help with navigating the repository, because I am relatively new to interactive theorem proving in general. - I think what I am looking for is in the `l4v/proof/invariant-abstract` directory inside the `{CNode, CSpace}*_AI.thy` files. Is this correct ? - How can I distinguish between helper lemmas and the invariants that you state for example in your paper: SeL4: formal verification of an OS kernel<https://dl.acm.org/doi/10.1145/1629575.1629596> ? - Is there any textual artifact that lists the invariants in prose that could help me ? - Can you clarify me the relationship between the specifications in `l4v/spec/abstract` and the proofs in `l4v/proof/invariant-abstract` ? According to my understanding, the abstract specification defines the system in the abstract level, whereas the proofs use these definitions from the specifications to prove properties and invariants about them. So, the invariants are the statements that the proofs prove. Am I on the right track ? Thank you for your help, Thanasis Typaldos

2 1

Reminder seL4 developer hangout
by Birgit Brecknell 16 Oct '23

16 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 18, 5pm For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0

Incorrect dtb in the Microkit tutorial
by Luke Hart 09 Oct '23

09 Oct '23

Hello, It seems that the linux.dtb file supplied with the tutorial code is not correct and does not allocate enough memory for the initrd. The symptoms this issue caused when attempting to run part4 was that the libresolv.so.2 could not be opened and the vmm panic'ed. The linux.dtb supplied in the 'solution' folder in the git repository has 'initrd-end' set to a larger value and this version does work. Thanks, Luke

2 1

Re: The seL4 Microkit tutorial is now available
by Isaac Beckett 05 Oct '23

05 Oct '23

> Date: Wed, 4 Oct 2023 06:36:02 +0000 > From: Ivan Velickovic <i.velickovic(a)unsw.edu.au> > Subject: [seL4] The seL4 Microkit tutorial is now available > To: devel <devel(a)sel4.systems> > > Hello everyone, > > For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. > > The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. > > Thanks, > Ivan Hello, I was going to ask what Microkit was and how it differs from seL4 Core Platform, but I see it’s just a new name. That’s good to know. I’ll definitely be checking out that tutorial Also, where can I find information on comparison between CAMmkES and Microkit/seL4cp? I only have a vague idea of the difference between the two. Thanks, Isaac

2 1

The seL4 Microkit tutorial is now available
by Ivan Velickovic 04 Oct '23

04 Oct '23

Hello everyone, For those who are new to seL4 or want to learn about the seL4 Microkit, the Microkit tutorial is now available to everyone on the Trustworthy Systems website: https://trustworthy.systems/projects/microkit/tutorial/welcome.html. This is the same tutorial that ran at this year’s seL4 Summit. The tutorial code and infrastructure is also open-source, available here https://github.com/au-ts/microkit_tutorial. Feel free to provide feedback or ask questions there. Thanks, Ivan

1 0

Re: [oss-security] Xen Security Advisory 439 v1 (CVE-2023-20588) - x86/AMD: Divide speculative information leak
by Solar Designer 04 Oct '23

04 Oct '23

On Tue, Sep 26, 2023 at 09:59:19PM -0400, Demi Marie Obenour wrote: > These detailed security advisories are one of the things I love about > Xen. It's hard to trust a hypervisor (KVM) that will not issue them, > for then one has no way to know if a particular problem got fixed. I concur. I'd appreciate security advisories from the KVM project. > I'm CCing KVM here to make sure they have a fix. From their Git commit > history, I am almost certain that seL4 does not. I'm CCing the seL4 > developers to alert them of this and suggest that the x86 port be > removed or at least have a big warning. I strongly oppose removal of a port/support for a certain architecture just because some implementations of it are/were problematic. Adding a warning is fine. Alexander P.S. Demi Marie, please note that oss-security list content guidelines explicitly discourage CC'ing other lists(*), and Xen advisories are already stretching this. In this reply, I am still CC'ing many of what you had CC'ed as I am following up on your specific points relevant to those lists, but in general let's be more careful about this. (*) Because we may then get off-topic follow-ups from there, especially if CC'ing project user lists or high-volume lists like LKML. In this specific case, we're lucky so far.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 02 Oct '23

02 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Oct 4, 8am For your time zone, please see the calendar: https://sel4.systems/contact/ Zoom link: https://unsw.zoom.us/j/82640784431 cheers Birg --- Birgit Brecknell Project Coordinator, seL4 Foundation birgit(a)sel4.systems<mailto:birgit@sel4.systems> birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> Mon 9am-5pm Wed 2pm-5pm Fri 9am-5pm

1 0