[seL4] Booting process

Hi all, I’m very new to seL4 development. I’m particularly interested in understanding seL4 kernel source code. Could someone points me out how the seL4 is booted and where should I start learning? Thanks -Dan ___ Devel mailing list Devel@sel4.system

[seL4] Questions about Kernel Memory Mapping

Hi all, I’m trying to understand the seL4 kernel source code. I think the memory mapping between physical memory and virtual memory is a key point since it is directly related to how kernel functions and manage badges. I noticed that the kernel turns on the paging very early. Can someone help m

[seL4] How to run seL4 as a hypervisor?

Hi all, Is there any document/tutorial about using seL4 as a hypervisor to running Linux on top? Appreciate for your help. Thanks -Dan ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

[seL4] Questions about Capability model

Hi all, I’m new to the capability concept of seL4. Please correct me if I’m wrong. My understand of the capability is that it is a reference to a chunk of memory that allocated for specific purpose. Say if I want to do IPC between two threads A and B, I will need to apply an chunk of memory as

[seL4] Questions about Memory Management in seL4

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode

Re: [seL4] Questions about Capability model

a61.csiro.au wrote: > >> On 21 Sep 2016, at 3:29 , Daniel Wang wrote: >> >> Hi all, >> >> I’m new to the capability concept of seL4. Please correct me if I’m wrong. >> My understand of the capability is that it is a reference to a chunk of >> memo

[seL4] Questions about Userspace memory allocation

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB

[seL4] Running Linux on top of seL4

Hi all, Is there any guide about how to run Linux on top of seL4? Or has anyone done that before that can give me some hints? Thanks -Dan ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Re: [seL4] Running Linux on top of seL4

Thank you for your response. I found out the two suggested board for Linux virtualization using seL4 are ODROID-XU and TK1-SOM Module. Is it still the case? The TK-1 SOM Module has been used by DARPA SCACCMPILOT project. Is it the recommended platform? For our experiment I need to have a Linux

Re: [seL4] Running Linux on top of seL4

on the XU3. I'm currently trying to get something up and running on > the XU4. This project: > > https://github.com/SEL4PROJ/camkes-arm-vm-manifest > <https://github.com/SEL4PROJ/camkes-arm-vm-manifest> > > has a VM that works for the TK1-SOM. > > - John

Re: [seL4] Running Linux on top of seL4

Sorry one more question: Can the Jetson TK1 (or other cheaper board) being used for running Linux Virtualization on top of seL4? I’m not familiar with TK1 board, it is kind of costly, and it has a NVIDIA Tegra K1 GPU. For using seL4 as a microvisor, I assume we only need a board to support ARM V

[seL4] seL4test with 4.0, 5.1 failed on Ubuntu

Hi all, I’m testing the new versions of seL4 (,4.0, 5.0, 5.1, etc.) using the sel4test-manifest. I tried both Ubuntu 16 and Ubuntu 14. For 3.2 version both I32 and KZM_simulation built just fine. However for the higher version (4.0. 5.1, 5.2) only I32 built properly. KZM_simulation keep failing

Re: [seL4] seL4test with 4.0, 5.1 failed on Ubuntu

at > configuration fix, does seem to build correctly for me. > > Adrian > > On Fri 16-Jun-2017 6:11 AM, Daniel Wang wrote >> Hi all, >> >> I’m testing the new versions of seL4 (,4.0, 5.0, 5.1, etc.) using the >> sel4test-manifest. I tried both Ubuntu 16 and Ubu

[seL4] Questions about TK1-SOM Memory Management

Hi all, I’m trying to get a better understand about the implementation details of seL4 for TK1-SOM. Most of the code are very clear, but I’m little confused on the available physical memory in TK1-SOM. I’m wondering why In the hardware.c file (/kernel/src/plat/tk1/machine/hardware.c), the ava

[seL4] Questions about TK1-SOM Memory Management

Hi Adrian, Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)? I can see the dev_p_regs[] (kernel/src/plat/tk1/machine/hardware.c)

Re: [seL4] Questions about TK1-SOM Memory Management

same for seL4. The reason I ask is that if seL4 maintains an armKSGlobalPD[], is that means it uses armKSGlobalPD[] for user land process context switch? Thanks -Dan > On Jun 21, 2017, at 3:32 PM, hesham.almat...@data61.csiro.au wrote: > > Hi Daniel, > > > On 21/06/17 08:26,

Re: [seL4] seL4 as TEE OS in TrustZone

support? How about QEMU, it will be easier to simulate first. Best Regards -Daniel Wang > On Jan 27, 2018, at 3:51 AM, Stefan Wallentowitz > wrote: > > Hi Dan, > > I have mentored a proof of concept project with the lowRISC project > during Google Summ

Re: [seL4] seL4 as TEE OS in TrustZone

Hi Gernot, We are thinking about exploring TZ mainly because lots of legacy software stacks are written for Linux. It would be very costly to port all code directly into seL4. Best Regards -Daniel Wang > On Jan 29, 2018, at 4:17 PM, > wrote: > > On 30 Jan 2018, at 05:22,

Re: [seL4] seL4 as TEE OS in TrustZone

business to switch hardware and some their chosen boards already support TZ. Although I’ m not 100% sure the difference between those two solutions regards of system security and performance. I would love to hear your opinion. Thank you very much for your response. Best Regards -Daniel Wang >

[seL4] seL4 VMM Hangs during loading time

started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[9000..913a7fff] ELF-loading image 'kernel' paddr=[6000..6003cfff] vaddr=[e000..e003cfff] virt_entry=e000 --- Best Regards -D

Re: [seL4] seL4 VMM Hangs during loading time

did those two things before that can give me some advice? I implemented the the second scenario before using L4re with a paravirtualized L4Linux. But I’m exactly sure how to do it with seL4 yet. Best Regards -Daniel Wang > On Mar 1, 2018, at 8:00 PM, > wrote: > > Hi Dani

[seL4] ARM-VM with Linux Distribution

Hi all, I was able to compile the camkes-arm-vm and run it on a TK1-SOM board. I wonder if it is possible to run a Linux distribution as the guest OS, such as Ubuntu, Fedora, etc.? If so how can we do that? Best Regards -Daniel Wang ___ Devel

[seL4] Questions about Allocman

{ seL4_Word cookie; cspacepath_t slot; }; I didn’t find struct that hold the paddr, also after we create a frame where is that paddr stored? It is stored in slot.capPtr? Also What does the field cookie for? Best Regards -Daniel Wang ___ Devel

[seL4] CapDL spec for Camkes-ARM-VM

the VMM and guest Linux. I assume I need to modify the CapDL. I’m not exactly the work flow with CapDL can you give me a hint? Thanks. Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Re: [seL4] CapDL spec for Camkes-ARM-VM

Hi Adrian, Thank you for your response. Yeah I mixed the relationship between CamkES and CapDL. Best Regards -Daniel Wang > On Mar 7, 2018, at 5:36 PM, > wrote: > > Hi Daniel, > > The camkes-arm-vm project is built on CAmkES, which has a high level system > assemb

Re: [seL4] Compilation Error with version

I saw something similar with Camkes-arm-vm-manifest repository after I sync. Will do more test make sure it is not a issue with configuration. Best Regards -Daniel Wang > On Mar 7, 2018, at 5:37 PM, > wrote: > > Hi Thad, > > Can you please provide steps to reproduce

Re: [seL4] Compilation Error with version

Wang > On Mar 7, 2018, at 5:43 PM, Daniel Wang wrote: > > I saw something similar with Camkes-arm-vm-manifest repository after I sync. > Will do more test make sure it is not a issue with configuration. > > Best Regards > -Daniel Wang > > >

Re: [seL4] Compilation Error with version

kes-arm-vmm/stage/arm/tk1/accelerator/camkes-accelerator' failed make: *** [/home/daniel/Documents/camkes-arm-vmm/stage/arm/tk1/accelerator/camkes-accelerator] Error 1 Best Regards -Daniel Wang > On Mar 7, 2018, at 9:53 PM, Daniel Wang wrote: > > I’m afraid that the new update i

Re: [seL4] Compilation Error with version

Thank you so much Kent! It took me a while. I was trying to use -b 15844a5 but it does work. Best Regards -Daniel Wang > On Mar 7, 2018, at 10:11 PM, > wrote: > > Hi Daniel, > > To check out a particular version of default.xml you can pin it when you > checkout

Re: [seL4] Compilation Error with version

I see. I thought it might be due to my old configuration. Thank you for pointing it out for me. I will update my cmake. Best Regards -Daniel Wang > On Mar 7, 2018, at 10:24 PM, > wrote: > > Hi Daniel, > > The accelerator was changed in a way that requires some ne

[seL4] Share UART with Guest Linux

data FAULT HANDLER: +-- 0x0001 -- CPIO: 2 files found. 0) linux 0x00059c70, 16302080 bytes 1) linux-dtb 0x00fe5ce8,29415 bytes Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4

Re: [seL4] Share UART with Guest Linux

Sorry for the confusion. printf works fine. syscall 162 is actual SYS_nanosleep. I guess it is not implemented by sel4’s libmuslc yet. Best Regards -Daniel Wang > On Mar 8, 2018, at 11:53 PM, Daniel Wang wrote: > > Hi all, > > For experiment, I created a simple app along wit

[seL4] Questions about Vchan

But the compile shows error due to the VM.h file (camkes-arm-vm/projects/vm/components/VM/src/cmks_vchan_vm.c:23) cannot be found. How can I generate the VM.h file? Thanks a lot! Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.system

Re: [seL4] Questions about Vchan

manage ioctl() syscall? Best Regards -Daniel Wang > On Mar 13, 2018, at 8:44 PM, > wrote: > > We haven’t touched the vchan code in a while, and have pretty much stopped > using vchan. We developed cross-vm dataports and events for x86[1], and will > be starting work

Re: [seL4] Questions about Vchan

configured (I assume that is done by capdl). I’m not exactly sure what is need in the hardware-assisted virtualization environment. Best Regards -Daniel Wang > On Mar 13, 2018, at 9:06 PM, kent.mcl...@data61.csiro.au wrote: > > As far as I am aware, the arm support for Vchans

[seL4] VM and VMM Communication for ARM

. Does it triggers vevent? I’m not sure the control flow. Thank you in advance! Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

[seL4] ARM Vchan Error

modified call_into_hypervisor() or by event_thread_run()->eventfd_signal(). Any help would be appreciated! Thanks in advance. Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

[seL4] Questions on U-boot Verified Boot with CAmkES-ARM-VM

different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much! Best Regards -Daniel Wang

[seL4] Booting BIN abort after elfloader

age 'capdl-loader-experimental' paddr=[8003d000..81f3efff] vaddr=[1..1f11fff] virt_entry=184f8 Enabling MMU and paging Jumping to kernel-image entry point... abort() called. Best Regards -Daniel Wang ___ Devel mailing list Deve

[seL4] OPENSSL for seL4

available for now I wonder has anyone used other crypto library before, such as wolfssl, bearssl, etc.? Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

[seL4] Passing Network Resource to Linux VM in TK1-SOM

, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

[seL4] Questions on CAMKES-ARM-VM Build and Components

and kernel modules work for ARM architecture, TK1 or TK1-SOM specifically? Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Re: [seL4] Questions on CAMKES-ARM-VM Build and Components

Regards -Daniel Wang > On Oct 4, 2018, at 2:36 PM, Mike Clark wrote: > > I've been doing > > # ../init-build.sh -DAARCH32=TRUE -DTk1Insecure=TRUE -DCAMKES_VM_APP=tk1_vm > # ninja > > If that doesn't work can you post logs? > > On Thu, Oct 4, 2018 at

Re: [seL4] Questions on CAMKES-ARM-VM Build and Components

Thank you so much for your response! Is there any way for now that allows VM and native process communicate? Best Regards -Daniel Wang > On Oct 4, 2018, at 3:16 PM, Kent Mcleod wrote: > > Hi, > > The x86 connectors don't currently work in the arm vmm unfortunately. Th

[seL4] Reverse back to Original TK1-SOM U-boot

ot the original on board Linux? Thank you! Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

Re: [seL4] Reverse back to Original TK1-SOM U-boot

kernel ... Best Regards -Daniel Wang > On Oct 10, 2018, at 11:30 PM, > wrote: > > Hi Daniel, > You shouldn't have to reflash to boot the original Linux. If you > want to, use Nvidia's L4T tool. But try to reset the secure mode > booting by doing &g

Re: [seL4] Reverse back to Original TK1-SOM U-boot

gra124 stderr=serial stdin=serial stdout=serial usb_boot=usb start; if usb dev ${devnum}; then setenv devtype usb; run scan_dev_for_boot_part; fi vendor=cei Best Regards -Daniel Wang > On Oct 10, 2018, at 11:35 PM, Daniel Wang wrote: > > Hi Dr. Chubb, > > Thank you for you

Re: [seL4] Reverse back to Original TK1-SOM U-boot

Thank you very much Dr. Chubb! Yes I think you are right. I got access to their FTP and did the same thing now I can boot original Linux. Will flash the U-boot so I can boot seL4. Thank you for confirming it, and thank you for testing out for me. Best Regards -Daniel Wang > On Oct 11, 2

[seL4] camkes-arm-vmm run multiple VMs at once

Hi all, I’m wondering can the camkes-arm-vmm run multiple VMs at once? I know it is possible for X86 but I’m not sure about the ARM version. Thanks Best Regards -Daniel Wang ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists

Re: [seL4] Passing Network Resource to Linux VM in TK1-SOM

Yeah it helps a lot. Thank you! Best Regards -Daniel Wang > On Nov 5, 2018, at 8:03 PM, > wrote: > > Hi Daniel, > > I don't know if this is still an issue for you, but if it is, do these > instructions help? > https://sel4.systems/pipermail/devel/2017-January