Devel October 2023

devel@sel4.systems

9 participants
12 discussions

Use C-parser on seL4 based application
by r2ji＠uwaterloo.ca 20 Nov '23

20 Nov '23

Hi, I have been trying to reuse the seL4 verification framework to verify a toy example I built on seL4, and I am currently stuck on the c-parser step. I am trying to use c-parser to parse the example I built, then conduct refinement verification. The toy example is a normal c project, which includes `sel4.h`. From this thread: https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/3QYNFY… I learned that I am supposed to do $ ./isabelle/bin/isabelle jedit -d . -l CParser toy.thy And the toy.thy file is supposed to begin with `install_C_file("toy.c")`. However, since toy.c includes sel4.h, I am not sure how to preprocess it before I put it into toy.thy. I know the standalone c-parser can have a -I flag to include in all the dependency directories, but it cannot open an interactive window. (From my understanding, the standalone c-parser seems to be only a checking tool) I also know that when sel4 is parsed into HOL, it is preprocessed into a single c file `kernel_all.c_pp`, which is later parsed. I am not sure if the preprocessor tool can be reused for other applications as well. My question is summarized as: 1. Is there a way to add an include directory in interactive CParser? 2. If not, can I reuse the preprocessing approach for sel4 to preprocess my application to a singleton file that can be parsed by c-parser? Any help will be appreciated! Thanks, Ru

2 2

Reminder seL4 developer hangout
by Birgit Brecknell 30 Oct '23

30 Oct '23

Hi all A friendly reminder that the seL4 developer hangout is on again this week: * Sydney: Wed, Nov 1, 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

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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel October 2023