Stack Overflow
Stack Overflow

Questions tagged [sel4]

seL4 is the most advanced member of the L4 microkernel, notable for its comprehensive formal verification, which sets it apart from any other operating system.

11 questions
5
votes
1 answer

SEL4 User-space drivers Example

I am trying to write sample usb driver for sel4 in userspace. can anybody have an idea about sel4 user-space driver please share with me... If anyone have example code for sel4 user-space driver(sample drivers) please share with me...
Ashokkumar
  • 115
  • 1
  • 3
  • 8
4
votes
1 answer

What is a conceptual difference between seL4 and Fuchsia's kernel?

Originally I thought Fuchsia was the first kernel to extensively use capability-based security, but it looks like in seL4 they are also the main security primitive.
LOST
  • 2,956
  • 3
  • 25
  • 40
3
votes
1 answer

is there a simple way to port linux drivers to L4?

I want to build a system over seL4 and I do not want to write the drivers from scratch. I know that L4linux managaged to raise an entire linux kernel, drivers included, over fiasco.OC. Ideally I want a driver wrapper that would allow me to run linux…
user3848844
  • 509
  • 6
  • 20
2
votes
3 answers

Is there any application of L4 (microkernel)?

I Googled a lot about L4 microkernel and found that very less resources are there on L4. What are some good links I can refer ? Is there any application of L4 (i.e. where it is used) ?
Dinushan
  • 2,067
  • 6
  • 30
  • 47
2
votes
1 answer

sel4 Verify the environment setup

Now I am setting up sel4 verification environment, but I see the blogger said "link isabelle path to verification directory", I would like to ask what it means？ Do you want to download isabelle to the verification directory？
Xinyue Wang
  • 31
  • 1
1
vote
0 answers

sel4 Verify the script-l4v

When I built c-parser, I didn't find the specific steps to build the environment. Do you have a friend to share I want to implement automatic conversion of c code
Xinyue Wang
  • 31
  • 1
1
vote
1 answer

Building riscv-gnu-toolchain

I'm building the riscv-gnu-toolchain here: https://github.com/riscv-collab/riscv-gnu-toolchain like this: git clone https://github.com/riscv/riscv-gnu-toolchain.git cd riscv-gnu-toolchain git submodule update --init --recursive export…
FirmwareRootkits
  • 121
  • 1
  • 9
1
vote
1 answer

Understanding Page Tables in Linux/seL4

Why are entries in the Page Global Directory offset? What is the significance of the offset, if any? Page Global Directory Address Entry 1 Entry…
FirmwareRootkits
  • 121
  • 1
  • 9
0
votes
0 answers

Does CAmkES support non-Linux VMs?

I am working on a project that utilizes seL4 as the hypervisor, with both a Linux VM and a simple partitioned OS running on top. It is known that seL4 officially provides demos for Linux VMs with the CAmkES. The problem then lies with implement the…
colored-dye
  • 1
0
votes
0 answers

Correct procedure and memory addresses to setup a virtio-net ethernet device on a sel4 microkernel

In short: I am trying to run the sel4 microkernel inside a x86_64 virtual machine and can't get the ethernet interface working. What is the correct procedure to get internet connectivity (via a vitio-net ethernet device) on a sel4 microkernel? And…
M_E
  • 1
  • 1
  • 2
0
votes
1 answer

Micro-kernel architecture based operating system for desktop users?

Can we have Operating system with micro-kernel architecture targeted on desktop users? I have read here on this website that older micro-kernel can be 50% slower than Monolithic kernel, while later version like L4 were only 2% or 4% slower than the…
Faisal Aslam
  • 1
  • 1