- Devel - lists.sel4.systems

Sel4 for quadcore riscv64imafd
by Sreenadh S 03 Oct '19

03 Oct '19

I want to build sel4 for quadcore riscv64imafd and run the test programs, how to do that? Regards, Sreenadh S, CDAC, Trivandrum, India

2 1

seL4_FailedLookup in vmware
by KAP Benjamin 03 Oct '19

03 Oct '19

Hello I set up VMware according to this guide https://docs.sel4.systems/Hardware/VMware/ (using serial output to file) and compiled the picoserver CAmkES application (for x86_64) to run inside the VMware machine. However, I do encounter a seL4_FailedLookup error. I understand the error message but cannot figure out why it occurs nor how to fix it (probably my pci configuration is wrong). Attached you find the serial_output file. For the ethernet configuration I used linux in the same VM to figure out the details: 1) ip addr: 2: ens32: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc fq_codel state UNKNOWN group default qlen 1000 link/ether 00:0c:29:90:a7:4a brd ff:ff:ff:ff:ff:ff 2) lspci -vvv: 02:00.0 Ethernet controller: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] (rev 10) Subsystem: Advanced Micro Devices, Inc. [AMD] PCnet - Fast 79C971 Physical Slot: 32 Control: I/O+ Mem+ BusMaster+ SpecCycle- MemWINV- VGASnoop- ParErr- Stepping- SERR- FastB2B- DisINTx- Status: Cap- 66MHz- UDF- FastB2B+ ParErr- DEVSEL=medium >TAbort- <TAbort- <MAbort- >SERR- <PERR- INTx- Latency: 64 (1500ns min, 63750ns max) Interrupt: pin A routed to IRQ 18 Region 0: I/O ports at 2000 [size=128] [virtual] Expansion ROM at fd500000 [disabled] [size=64K] Kernel driver in use: pcnet32 Kernel modules: pcnet32 3) dmesg | grep "02:00.0": ... [ 0.378516] pci 0000:02:00.0: BAR 6: assigned [mem 0xfd500000-0xfd50ffff pref] ... 4) lspci -nn: 02:00.0 Ethernet controller [0200]: Advanced Micro Devices, Inc. [AMD] 79c970 [PCnet32 LANCE] [1022:2000] (rev 10) And here the configuration part inside picoserver.camkes (anything else NOT pasted here is unmodified): picoserver.ethdriver_mac = [0x00, 0x0c, 0x29, 0x90, 0xa7, 0x4a]; .... hwethdriver.mmio_paddr = 0xfd500000 hwethdriver.mmio_size = 0x10000 hwethdriver.irq_irq_type = "pci"; hwethdriver.irq_irq_ioapic = 0; hwethdriver.irq_irq_ioapic_pin = 18; hwethdriver.irq_irq_vector = 18; ethdriver.iospaces = "0x0:0x02:0x00:0"; ethdriver.iospace_id = 0x0200; ethdriver.pci_bdf = "0x02:0x00.0"; I am sorry to bother you with this; I am fairly new to low level stuff. Any help would be very much appreciated. Best regards, Benjamin

2 1

Adding an Extra Component in Camkes
by Amit Goyal 03 Oct '19

03 Oct '19

Hi, I was trying to add an extra component in hello-camkes-1 example. Here are the small tweaks that I did. a) hello-camkes-1-camkes.template import <std_connector.camkes>; import "components/Client1/Client1.camkes"; import "components/Client2/Client2.camkes"; import "components/Echo/Echo.camkes"; assembly { composition { component Client1 client1; component Client2 client2; component Echo echo; connection seL4RPC hello_con(from client1.hello1, to echo.hello2); } } -------------------------------------------------------------------------------------------------------------------------- b) CMakeLists.text cmake_minimum_required(VERSION 3.7.2) project(hello-camkes-1 C) DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES components/Client1/src/client1.c) DeclareTutorialsCAmkESComponent(Client TEMPLATE_SOURCES components/Client2/src/client2.c) DeclareTutorialsCAmkESComponent(Echo TEMPLATE_SOURCES components/Echo/src/echo.c) DeclareCAmkESComponent(EmptyComponent) DeclareTutorialsCAmkESRootserver(hello-camkes-1.camkes ADL_IS_TEMPLATE TEMPLATE_SOURCES interfaces/HelloSimple.camkes TUTORIAL_SOURCES components/Client1/Client1.camkes components/Client2/Client2.camkes components/Echo/Echo.camkes ) ------------------------------------------------------------------------------------------------------------------------ I am getting the following error: STDERR: CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:16 (include) CMakeLists.txt:21 (include) CMake Error at build/projects/sel4-tutorials/camkes-gen.cmake:192 (target_link_libraries): Error evaluating generator expression: $<TARGET_PROPERTY:CAmkESComponent_Client1,COMPONENT_LIBS> Target "CAmkESComponent_Client1" not found. Call Stack (most recent call first): tools/camkes/camkes.cmake:591 (include) projects/sel4-tutorials/CMakeLists.txt:257 (GenerateCAmkESRootserver) CMake Error at build/projects/sel4-tutorials/cam... (2531 more, please see e.stderr) ----------------------------------------------------------------------------------------------------------------- Can you please suggest a possible solution. -- Thanks and Regards, Amit Goyal

2 1

Questions about building Raspberry Pi image on SEL4
by Zhonghao Liao 03 Oct '19

03 Oct '19

Hi, I am Zhonghao Liao, a graduate student from Iowa State University. We are doing a security related project and would like to deploy the code to the SEL 4. The hardware we use is Raspberry Pi 3 B+. We follow the tutorial here <https://docs.sel4.systems/Hardware/Rpi3.html> and have successfully loaded the SEL4 test image. We think the next step should be building the image for the application and run it on the Raspberry Pi. We followed the CAmKES tutorial <https://docs.sel4.systems/CAmkES/> and tried to use the command: ../init-build.sh -DPLATFORM=sabre -DAARCH32=1 -DCAMKES_APP=adder -DSIMULATION=1 to build the image for the Raspberry Pi but we failed. In fact, we change the settings.cmake file in the camkes-project folder and add "rpi3" at line 36: set(valid_arm_platform "am335x;sabre;kzm;exynos5410;exynos5422;tx1;tx2;zynq7000;rpi3") and the command we used is: ../init-build.sh -DPLATFORM=rpi3-DAARCH32=1 -DCAMKES_APP=adder -DSIMULATION=1 We did get an image but we cannot simulate using QEMU: ninja: Image Name: Created: Tue Sep 17 09:30:30 2019 Image Type: ARM Linux Kernel Image (uncompressed) Data Size: 2110464 Bytes = 2061.00 KiB = 2.01 MiB Load Address: 0157c000 Entry Point: 0157c000 ./simulate: Unsupported platform or architecture for simulation Also we tried to load the image into the RPi3 but we are also defeated: bootelf {loadaddr} ## No elf image at address {loadaddr} I think our problem is that we don't provide enough dependencies to support building the RPi image. But we have no idea where to start. Could you please give us any advice? Otherwise, If the CAmkES can not be used, how do I build an application on SEL4 and run it on the Raspberry Pi? Thanks for your patient and looking forward to your reply. Thank you! Best, Zhonghao

2 1

Enable benchmarking tools on SEL4
by Zhonghao Liao 20 Sep '19

20 Sep '19

Hi, I am going to measure the resource consumption of process on SEL4 and I found the tutorial here: https://docs.sel4.systems/BenchmarkingGuide.html One thing I am confused about is how to enable the benchmark feature shown below: "This feature can be enabled from the menuconfig list (seL4 Kernel > Enable benchmarks > Track threads and kernel CPU utilisation time)." It seems like there should be a file "menuconfig" or some other similar object I can modify. But I cannot find such an object. I would appreciate if you could give me any suggestions. Thank you! Best, Zhonghao

2 1

Using RPC in two different container
by Shahnewaz Sakib 19 Sep '19

19 Sep '19

Hi, I just used hello-camkes-1 tutorial to send and receive a message between a client and an echo. My understanding is that both client and echo are in the same machine but different address. What changes do I need to make so that client and echo are in different machine? I have used docker for using seL4 environment. I was thinking about using container1 for client and container2 for echo and communicate between them. Is there any way I can do it by modifying the hello-camkes-1tutorial? If not, can anyone suggest a way to do it? Thanks! -- Regards' Shahnewaz Karim Sakib

2 1

Issues with broadcasting a message in seL4
by Shahnewaz Sakib 13 Sep '19

13 Sep '19

Hi, I was trying to generate a simple broadcasting message in sel4. I have used a c code I found in the internet. #include <stdio.h> #include <sys/socket.h> #include <arpa/inet.h> #include <stdlib.h> #include <string.h> #include <unistd.h> void DieWithError(char *errorMessage) { perror(errorMessage); exit(1); } int main(int argc, char *argv[]) { int sock; struct sockaddr_in broadcastAddr; char *broadcastIP; unsigned short broadcastPort; char *sendString; int broadcastPermission; unsigned int sendStringLen; broadcastIP = "0.0.0.0"; broadcastPort = 6741; sendString = "Hello World!"; printf("start\n"); printf("Socket is about to be created!\n"); if ( (sock = socket(AF_INET, SOCK_DGRAM, 0)) < 0 ) { perror("socket creation failed"); exit(EXIT_FAILURE); } printf("Socket is created! \n"); broadcastPermission = 1; if (setsockopt(sock, SOL_SOCKET, SO_BROADCAST, (void *) &broadcastPermission, sizeof(broadcastPermission)) < 0) DieWithError("setsockopt() failed"); memset(&broadcastAddr, 0, sizeof(broadcastAddr)); broadcastAddr.sin_family = AF_INET; broadcastAddr.sin_addr.s_addr = inet_addr(broadcastIP); broadcastAddr.sin_port = htons(broadcastPort); sendStringLen = strlen(sendString); for (;;) { if (sendto(sock, sendString, sendStringLen, 0, (struct sockaddr *) &broadcastAddr, sizeof(broadcastAddr)) != sendStringLen) DieWithError("sendto() sent a different number of bytes than expected"); sleep(3); } return 0; } However, I get the error in syscall 41. What I understood is that for some reason the socket is not created successfully and can't find an endpoint. What can be the reason for that? libsel4muslcsys: Error attempting syscall 41 Caught cap fault in send phase at address (nil) while trying to handle: vm fault on data at address 0x28 with status 0x4 in thread 0xffffff801fe09400 "rootserver" at address 0x40e3af With stack: 0x41ce28: 0x40c0fe 0x41ce30: 0x418720 0x41ce38: 0x0 0x41ce40: 0x41ceb0 0x41ce48: 0x0 0x41ce50: 0x0 0x41ce58: 0x4011bd 0x41ce60: 0x41cf10 0x41ce68: 0x200402323 0x41ce70: 0x3 0x41ce78: 0x3 0x41ce80: 0x41ceb0 0x41ce88: 0x401ce2 0x41ce90: 0xffffffff00000000 0x41ce98: 0x412008 0x41cea0: 0x1a5500000041cf20 Thanks! -- Regards' Shahnewaz Karim Sakib

2 1

CAmkES 3.7.0 bug?
by Zippy Maniac 11 Sep '19

11 Sep '19

Hi, I am porting an old application from CAmkES 2.x to CAmkES 3.7.0. But I am having an issue with a very large dataport. The data structure mapped between components needs to be about 25 MiB. I have defined the size of the connection to be 64 MiB. But compilation fails. Looking at the generated code for the shared data I see this struct { char content[ROUND_UP_UNSAFE(sizeof(ui_config_t), PAGE_SIZE_4K)]; } to_0_ui_configbuf_data ALIGN(16777216) SECTION("align_24bit") USED; extern typeof(to_0_ui_configbuf_data) to_0_ui_configbuf_data ALIGN(67108864) VISIBLE; static_assert(sizeof(to_0_ui_configbuf_data) <= 67108864, "typeof(to_0_ui_configbuf_data) size greater than dataport size."); static_assert(sizeof(to_0_ui_configbuf_data) % 16777216 == 0, "to_0_ui_configbuf_data not page-sized. Template bug in its declaration? Suggested formulation: `char to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`"); But compilation fails with projects/musllibc/build-temp/stage/include/assert.h:12:23: error: static assertion failed: "to_0_ui_configbuf_data not page-sized. Template bug in its declaration? Suggested formulation: `char to_0_ui_configbuf_data[ROUND_UP_UNSAFE(sizeof(...), PAGE_SIZE_4K)];`" The assert is looking for the buffer to be a multiple of 16MiB but the ROUND_UP_UNSAFE is only doing working to a multiple of 4KiB. PAGE_SIZE_4K is hard coded in the template but the alignment has changed from 12bit to 24bit so CAmkES is aware of the large data structure. I guess I could pad and align my data structure to a multiple of 16MiB. Also, having hard coded numbers in my top level CAmkES configuration for the dataport size is a bit of a maintenance nightmare. Being able to use a #define from the code base would be ideal but this doesn't work. It does work for paddr and irq_number specifications! Cheers, Zippy

2 2

Error with the file handling in camkes tutorial
by Akshat Garg 11 Sep '19

11 Sep '19

Hi all, I am trying to understand how the camkes system works. I get stuck up on a problem where I tried to change the code of camkes 1 tutorial ( https://docs.sel4.systems/Tutorials/hello-camkes-1.html) a bit. In a simple sender receiver code, I tried to write the contents, received by the receiver, in a file. But, while doing it I got the following error message. The error message was not letting me to create a file in any mode. When using read mode with FILE *fptr = fopen("xxxyyyzzz", "r"); I encountered the following message: sys_open_impl@sys_io.c:205 Failed to open file xxxyyyzzz FAULT HANDLER: data fault from client1.control (ID 0x1) on address 0, pc = 0x411754, fsr = 0x4 FAULT HANDLER: rip = 0x411754 FAULT HANDLER: rsp = 0x528ae8 When using write mode with FILE *fptr = fopen("xxxyyyzzz", "w"); I encountered the following message: sys_open_impl@sys_io.c:191 Open only supports O_RDONLY, not 0x241 on xxxyyyzzz Assertion failed: flags == O_RDONLY (../projects/seL4_libs/libsel4muslcsys/src/sys_io.c: sys_open_impl: 192) Kindly, suggest me a way out or let me know the reason if not possible. -Akshat

2 1

Compiling Error for Hello World
by Shahnewaz Sakib 11 Sep '19

11 Sep '19

Hi, I was trying to compile hello world using the tutorial here <https://docs.sel4.systems/Tutorials/#get-the-code>. I was able to compile sel4test before and I built the dependencies using docker. For running hello world, I used the command "../init --plat pc99 --tut hello-world". Then I got the following error message: Traceback (most recent call last): File "../init", line 16, in <module> import common File "/home/bikas/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' I have looked into my machine and I do have sh in "/usr/bin/sh". I am not sure what is the source of the error. Please let me know. Thanks! -- Shahnewaz Karim Sakib

2 1

Muen
by Gergely Buday 07 Sep '19

07 Sep '19

Hi, how does Muen relate to seL4? https://muen.codelabs.ch/ e.g. it claims to be the first verified microkernel. - Gergely

2 1

Issues about compile C program
by Zhonghao Liao 03 Sep '19

03 Sep '19

Hi, I am a graduate student and I am doing ainformation security related research project using SEL4. I installed the SEL4 kernel on a raspberry pie 3. The problem is that I can't compile C programs on this Raspberry Pi. Any suggestions for solving this problem? Thank you! Best, Zhonghao Liao

2 1

seL4 UART input (on RISC-V)?
by Ortiz, Baltazar 21 Aug '19

21 Aug '19

Hi all, I've been looking through the seL4 libraries and examples, and it seems to me that serial input should in some way be possible - the refos example appears to have a terminal, and I would imagine that debugging via GDB requires input in addition to output. However, the code to do this is unclear to me. Calling getchar() or similar leads to the unimplemented readv syscall, and calling __arch_getchar or similar causes a cap error even after running platsupport_serial_setup_simple(). Is there a step I'm missing? I'm specifically trying to get this working on RISC-V. Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

2 4

CapDL output to isabelle file
by Norrathep Rattanavipanon 20 Aug '19

20 Aug '19

Hello, I have been trying to generate Isabelle file from CapDL specification. But I run into an error when I'm running the command: ./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml example-arm.cdl warning: specifying untyped child multiple times is deprecated: ut = a, child = name warning: specifying untyped child multiple times is deprecated: ut = b, child = name warning: specifying untyped child multiple times is deprecated: ut = something, child = rm_ut parse-capDL: CapDL/PrintIsabelle.hs:180:15-71: Irrefutable pattern failed for pattern ut@(Untyped {maybePaddr = Just utPaddr}) where example-arm.cdl is the example I got from CapDL repo ( https://github.com/seL4/capdl/blob/master/capDL-tool/example-arm.cdl) And object_sizes.yaml contains: seL4_TCBObject: 10 seL4_EndpointObject: 4 seL4_NotificationObject: 4 seL4_SmallPageObject: 12 seL4_LargePageObject: 16 seL4_ASID_Pool: 12 seL4_ASID_Table: 10 seL4_Slot: 4 seL4_Value_MinUntypedBits: 4 seL4_Value_MaxUntypedBits: 29 seL4_PageTableObject: 10 seL4_PageDirectoryObject: 14 seL4_ARM_SectionObject: 20 seL4_ARM_SuperSectionObject: 24 seL4_IOPageTableObject: 12 seL4_IOPorts: 0 seL4_IODevice: 0 seL4_ARMIODevice: 0 seL4_IRQ: 0 seL4_IOAPICIRQ: 0 seL4_MSIIRQ: 0 The same error also occurs when I used parse-capdL executable generated by Camkes repo. Is there any step I'm missing? Or does the tool not support the conversion to Isabelle? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 0

Shared memory in CapDL
by Norrathep Rattanavipanon 12 Aug '19

12 Aug '19

Hi, I have been reading Andrew Boyton's thesis about CapDL and realized that CapDL does not support a shared memory page. Is it still a limitation in CapDL/Camkes? Or has it somehow been addressed? Does this limitation include the case where a page is mapped/shared with different access rights? e.g., a page is mapped writable to one process and the same page is mapped only readable to another process? Best, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

How to use sel4runtime
by Ortiz, Baltazar 09 Aug '19

09 Aug '19

Hi all, Another (less exclusively RISC-V related, though I am targeting RISC-V still) question - I've been trying to figure out the sel4runtime repo, but I'm a bit confused on how to set it up. Specifically: * How much of a "minimal seL4 environment" do I need to initialize first? * Do does my program with main() also need to specify a root task, or is that part of the minimal environment? * Is there a specific recommended location for the sel4runtime repo? Thanks! Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

1 0

SeL4 on 32 bit RISC-V
by Ortiz, Baltazar 09 Aug '19

09 Aug '19

Hi all, I'm looking into getting seL4 booting on 32 bit RISC-V. Currently working with seL4test 10.1.1, QEMU 4.0.0, and an upstream copy of riscv-gnu-toolchain (is there a specific release I should try?). I'm able to get seL4 to build after deleting a few CONST labels that the compiler was complaining about, but when I try to run the simulation script, I get the following output: > ./simulate -b /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 > /home/baltazar/qemu/build/riscv32-softmmu/qemu-system-riscv32 -machine spike_v1.10 -nographic -s -serial mon:stdio -m size=2000M -kernel images/sel4test-driver-image-riscv-spike > bbl loader > /host/sel4test-upstream-riscv/tools/riscv-pk/machine/minit.c:74: assertion failed: !(read_csr(misa) & fd_mask) > Power off Are there any tricks for getting this working right now? Thanks, Baltazar ________________________________ Notice: This email and any attachments may contain proprietary (Draper non-public) and/or export-controlled information of Draper. If you are not the intended recipient of this email, please immediately notify the sender by replying to this email and immediately destroy all copies of this email. ________________________________

3 5

CAmkES Tutorial Generation Issues
by Austin Owens 23 Jul '19

23 Jul '19

Hello, I am able to generate, build, and execute the majority of tutorials using init, ninja, qemu, etc. within sel4-tutorials-manifest. However, I am having issues generating the tutorials specifically for the CamkES tutorials. I have installed all of the system requirements and I am running on Ubuntu 18. The output I get is the following: # ./init --tut hello-camkes-0 loading initial cache file ../settings.cmake -- The C compiler identification is GNU 7.4.0 -- Check for working C compiler: /usr/bin/gcc -- Check for working C compiler: /usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- The CXX compiler identification is GNU 7.4.0 -- Check for working CXX compiler: /usr/bin/g++ -- Check for working CXX compiler: /usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc -- CPIO test cpio_reproducible_flag FAILED -- Performing Test compiler_arch_test -- Performing Test compiler_arch_test - Success -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/ast.pickle is out of date. Regenerating... -- /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake is out of date. Regenerating... CAmkES uses UTF-8 encoding, but your locale's preferred encoding is ansi_x3.4-1968. You can override your locale with the LANG environment variable. CMake Error at tools/seL4/cmake-tool/helpers/make.cmake:19 (file): file failed to open for reading (No such file or directory): /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes_gen/deps_1 Call Stack (most recent call first): tools/seL4/cmake-tool/helpers/make.cmake:77 (MakefileDepsToList) tools/camkes/camkes.cmake:460 (execute_process_with_stale_check) hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) CMake Error at tools/camkes/camkes.cmake:480 (message): Failed to generate /root/sel4-tutorials-manifest/hello-camkes-0_build/hello-camkes-0/camkes-gen.cmake Call Stack (most recent call first): hello-camkes-0/CMakeLists.txt:13 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/root/sel4-tutorials-manifest/hello-camkes-0_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 96, in <module> File "./init", line 85, in main File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/root/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 75, in _init_build_directory return sh.cmake(args + ['..'], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python3.6/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.6/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-0 -C ../settings.cmake .. STDOUT: STDERR: I am not sure if ast.pickle and camkes-gen.cmake being out of date has anything to do with deps_1 file not being present. It's not possible to copy the deps_0 file to deps_1 since calling the './init --tut hello-camkes-0' command again creates a new project directory. Is there something obvious that I am missing? Thanks, Austin

3 4

Autocorres tutorial for Isabelle/HOL beginner
by Norrathep Rattanavipanon 22 Jul '19

22 Jul '19

Hello, I have been trying to study how seL4's C code is formally verified. So I looked into Autocorres tool and had a bit of hard time understanding how to use the tool to generate Isabelle definitions from C code. I tried to follow Autocorres' quickstart but I was confused since I do not know much about Isabelle/HOL. I simply ran ``make AutoCorresTest" in l4v/tools/autocorres folder and it gave me this output: ``` Session Pure/Pure Session FOL/FOL Session HOL/HOL (main) Session HOL/HOL-Eisbach Session HOL/HOL-Library (main timing) Session HOL/HOL-Computational_Algebra (main timing) Session HOL/HOL-Algebra (main timing) Session HOL/HOL-Number_Theory (main timing) Session HOL/HOL-Statespace Session HOL/HOL-Word (main timing) Session Lib/Word_Lib (lib) Session Lib/Lib (lib) Session C-Parser/Simpl-VCG Session C-Parser/CParser Session Lib/CLib (lib) Session Unsorted/AutoCorres Session Unsorted/AutoCorresTest Building AutoCorresTest ... AutoCorresTest: theory AutoCorresTest.CustomWordAbs AutoCorresTest: theory AutoCorresTest.Test_Spec_Translation ... Finished AutoCorresTest (0:02:33 elapsed time, 0:08:14 cpu time, factor 3.23) ``` But I couldnt find any Isabelle definitions as output except "thy" files that contain: ``` theory somefile imports "AutoCorres.AutoCorres" begin external_file "somefile.c" install_C_file "somefile.c" autocorres "somefile.c" end ``` I suppose I need to invoke this file somehow using Isabelle in order to generate the definition but I'm not sure how to do that. Any help would be very appreciated. Best Regards, Norrathep -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 on the Xilinx Zynq US+ ZCU104 Evaluation Kit
by derek65 22 Jul '19

22 Jul '19

Hi, I'm interested in running sel4 on a Xilinx Zynq UltraScale+ MPSoC evaluation board. I read the great blog post about the port from DornerWorks [1] and checked the sel4 hardware support page here [2]. Since the Zynq ZCU102 Evaluation Kit listed is quite expensive, I wanted to ask if anyone tried the procedure described in the blog post on the much cheaper Xilinx US+ ZCU104 Evaluation Kit. Might this work as well? Thanks! Kind regards, - derek [1] - https://dornerworks.com/blog/hardware-security-growing-concern-sel4-ecosyst… [2] - https://docs.sel4.systems/Hardware/

4 3

CamkES support for waiting on multiple signals
by yogidk . 22 Jul '19

22 Jul '19

Hello , I would like to know if the CamkES has support for wait on multiple signal events ? I need to wait for 3 different events (say write, read and timer), I need to wait until one of these events occur. As soon as I get an event, I need to call a common function. I cannot use emitter/consumer signal events concept of CamKES here as it allows only one to one connection and not many to one connection. So in other words a single consumer_wait() for 3 different emitter events is not possible in CamkES. Any suggestions how can this be achieved using CamkES? Regards yk

3 3

Re: [seL4] Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 16 Jul '19

16 Jul '19

Hi Kent, Thank you for your detailed reply. I agree that write only accesses are stored as read write mappings and reading on a write only access dataport does not give any error. I am still not very clear about the following: a) As suggested by you, I looked through the generated spec in .cdl file. I did not find the expected configuration of the dataport. Please find attached my .cdl file along with the template file. I cannot find dataport "delta" in that. Can you please help me to figure out the same. b) As far as I understood the .cdl configuration is setup by the camkes/kernel and corresponding page table mapping entries are made for each component. Later, whenever a component is scheduled by the kernel, MMU hardware will check whether it has the read or write access, based on the page table entries provided by the kernel. Please correct me if I have misunderstood it. My query is that in seL4 for communicating using endpoints a thread mints endpoint capabilities into other threads cspace and gives it the required access. I am not very clear with why the similar mechanism was not used here. I mean why a thread does not mint a frame's capability into other thread cspace with the required access. I am referring to section 7.4 of seL4 manual (http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf) i) I feel if that would have been used, then we could take better advantage of the seL4 capability based access control guarantees and lift it to camkes. This way frame capability bits in frame capability could have been used to store/check the access rights. This way checks might have been software based rather than hardware based. ii) In case we are minting the frame in the similar way as mentioned above, can you point me towards that piece of code. iii) I hope minting is actually being used in Event connection and RPC connection. -- Thanks and Regards, Amit Goyal > On 2019-07-03 07:24, Mcleod, Kent (Data61, Kensington NSW) wrote: >> Camkes dataports on seL4 (seL4SharedData connector) are implemented as a >> shared memory mapping between the two components both pages are mapped to >> the >> same underlying frame of physical memory. The access rights are >> implemented >> via mapping attributes supported by the architecture. Your reads and writes >> through your dataport pointers are acting on this shared memory directly. >> The >> fault is generated by a hardware exception that seL4 handles by creating a >> fault and sending it to a registered fault handler (sendFaultIPC is the >> function in the kernel). There is a setting (that is enabled by default) >> that >> causes each Camkes component to set up a fault handler for all of its >> threads. >> If any of these threads cause a fault, such as by writing to read only >> memory, the fault handler will receive a message from the kernel. >> >> These mapping attributes are set when the kernel creates the page >> mapping for each component using the relevant Map invocation [1]. The >> result >> of building a Camkes system for seL4 is a system spec that contains all of >> the >> seL4 kernel objects and capabilities described by the system. Within this >> spec, dataports are described as a capability to physical memory where each >> capability has the specified access rights. When the system initialiser >> (capdl-loader-app in our case) is started by seL4 as the root task, it >> constructs the system following the spec and starts each Camkes component. >> By >> this point, the seL4 invocations for setting up the shared data page >> mappings >> have been performed. >> You can look through the generated spec in the build directory by finding >> the >> file with the .cdl extension. If you search for the name of the dataport >> you >> can find the capabilities and objects to validate that the rights are as >> you >> would expect. >> >> Hope this answers your questions. >> >> @Matthew: Write only mappings are still coerced by the capdl-loader to read >> write mappings before calling the mapping invocation. >> >> [1] https://docs.sel4.systems/ApiDoc.html#map-4

3 2

Understanding Camkes Dataport Interface Access Rights
by Amit Goyal 03 Jul '19

03 Jul '19

Hi All, I was looking at hello-camkes-2 tutorial. I understand the concept of dataports and the access rights given on dataport interfaces. I changed the configuration in hello-camkes-2.camkes.template file by adding echo.d = "R"; client.d = "W";. I did some changes in the client.c.template file to read on the dataport interface d by trying to access its contents through str/n/d pointers. Although, it only has write access on "d" in the new configuration. This leads to the fault handler being called when I simulate the build. I was just curious to find out where are such checks being done at the backend in camkes/seL4. I could find the code of fault handler in component.template.c but I could not find anywhere the code which checks that the client only has write access on dataport d and thus calling the fault handler. Can someone point me towards that piece of code or explain what is exactly happening at the backend in camkes/seL4? -- Thanks and Regards, Amit Goyal

4 4

Beaglebone Black: failed to find device frame
by KAP Benjamin 29 Jun '19

29 Jun '19

Hello I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file: projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h. Current contents of this file (I am creating it step by step, thus it might be incomplete): #pragma once #define HARDWARE_ETHERNET_COMPONENT #define HARDWARE_ETHERNET_INTERFACES \ consumes Dummy EthDriver; \ emits Dummy dummy_source; #define HARDWARE_ETHERNET_COMPOSITION \ connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver); #define HARDWARE_ETHERNET_CONFIG \ EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" }); \ EthDriver.generate_interrupts = 1; I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error: ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..8262e037] No DTB found! Looking for DTB in CPIO archive... Found dtb at 820c1b84 Loaded dtb from 820c1b84 paddr=[80034000..8003cfff] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'capdl-loader' paddr=[8003d000..8059afff] vaddr=[10000..56dfff] virt_entry=1e4dc ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space create_object@main.c:726 device frame/untyped, paddr = 0x48040000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x48042000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x4a100000, size = 12 bits create_object@main.c:726 device frame/untyped, paddr = 0x4a101200, size = 12 bits create_object@main.c:730 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x4a101200 seL4 root server abort()ed Debug halt syscall from user thread 0xffefd600 "rootserver" halting... Kernel entry via Unknown syscall, word: 65 The am335x.dtb contains the following line in ethernet@4a100000: reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>; I did find related posts (http://sel4.systems/pipermail/devel/2016-June/000850.html, http://sel4.systems/pipermail/devel/2018-July/002031.html and http://sel4.systems/pipermail/devel/2015-October/000530.html) but didn't help me that much.<http://sel4.systems/pipermail/devel/2018-July/002031.html)> If I am correct the hardware block isn't enabled but I don't know exactly how to do this. Could anyone help me out here or give me some hints? Best Regards, Kap Benjamin

3 7

seL4 devs
by James Rolevink 25 Jun '19

25 Jun '19

Hey, guys. After getting it up and running a while back, just wondering: are there any (good) seL4 app devs for hire? Engineer partner-in-crime is looking to develop apps for a smart device. Physically based in Adelaide. Cheers, James Rolevink –––––––––––––––––––––––––––––––––––––––– M: 04123 62 432 E: cybercitadel(a)icloud.com <mailto:james@cybercitadel.co> W: www.cybercitadel.co <https://www.cybercitadel.co/> L: james-r-53986189 <https://www.linkedin.com/in/james-r-53986189/> Cyber Citadel Pty Ltd ACN: 622 880 657

1 0

CMake Error
by Amit Goyal 25 Jun '19

25 Jun '19

Hi, Camkes had been working fine till now. Suddenly, it stopped working. I am running it on x86 system (i7 processor), ubuntu 16.04 on qemu. I am running the following commands: mkdir build cd build ../init --plat pc99 --tut hello-camkes-2 --solution Following error is generated: --------------------------------------------------------------------------------------------------------------------------------- Traceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/goyal/sel4/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 59, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/uTraceback (most recent call last): File "../init", line 76, in <module> sys.exit(main()) File "../init", line 62, in main result = common.init_build_directory(args.plat, args.tut, args.solution, os.getcwd()) File "/home/goyal/sel4/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 59, in init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 774, in __init__ self.wait() File "/usr/local/lib/python2.7/dist-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python2.7/dist-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/local/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL=hello-camkes-2 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- Configuring incomplete, errors occurred! STDERR: CMake Error at /opt/cmake-3.11.0-Linux-x86_64/share/cmake-3.11/Modules/CMakeDetermineSystem.cmake:100 (message): Could not find toolchain file: ../kernel/gcc.cmake Call Stack (most recent call first): CMakeLists.txt CMake Error: CMake was unable to find a build program corresponding to "Ninja". CMAKE_MAKE_PROGRAM is not set. You probably need to select a different build tool. CMake Error: CMAKE_C_COMPILER not set, after EnableLanguage CMake Error: CMAKE_CXX_COMPILER not set, after EnableLanguage --------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a possible way out? -- Thanks and Regards, Amit Goyal

5 8

Checking if an endpoint is a badged version of another
by Demi Obenour 15 Jun '19

15 Jun '19

I have a server process SB that issues badged endpoints to users. Clients can invoke the endpoints to access memory and possibly other resources. Essentially, it is a version of Robigalia’s space bank. Other programs pass endpoints issued by SB to provide servers the resources needed to do their tasks, and the servers invoke the endpoints to obtain memory that they know cannot be revoked or modified by other programs. SB is part of the TCB, and is trusted by all of its clients. Clients, however, do not trust each other, and may pass forged endpoints to servers to cause servers to misbehave. Therefore, servers need to be able to ask SB if a given capability was actually issued by SB. SB can make that check by checking that the endpoint is a badged version of its master endpoint, which it never gives anyone else access to. What is the correct API function for doing this? Sincerely, Demi M. Obenour

2 1

Re: [seL4] Checking if an endpoint is a badged version of another
by Millar, Curtis (Data61, Kensington NSW) 15 Jun '19

15 Jun '19

Hi Demi, Any time you perform an seL4_Call operation on an endpoint and block waiting for a reply you are trusting that endpoint in a variety of ways. You trust that the messages will eventually get a reply and allow you to resume. You also trust that the message will eventually be received. If you want to perform an seL4_Call on an untrusted endpoint you will require a monitor thread that can handle a timeout and reset the calling thread if it is still blocked. In general, you want to avoid using endpoints where you can't trust that the message will be received and replied to in a timely manner. Asynchronous notifications do not suffer from this trust requirement so it is recommended that communication between mutually distrusting servers use shared memory and notifications. The client should seL4_Signal the server to notify a message has been sent via the shared memory and the server should signal in response to notify the client the message has been handled and the reply is in the shared memory. The problem of setting up a connection, sending the reply badged notification object to the server, acquiring a send notification object from the server, and mapping the shared memory would require either the connection being statically configured at process creation or dynamically configured by some mutually trusted shared component. Cheers, Curtis

1 0

Re: [seL4] camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

sorry, previous email sent by mistake. #include "sys/socket.h" actually solved the problem instead of only "socket.h" many thanks. Regards yk On Fri, Jun 14, 2019 at 10:30 AM yogidk . <yogidk(a)gmail.com> wrote: > thanks Kent and Peter, > > however if I remove > > > On Fri, Jun 14, 2019 at 2:14 AM Mcleod, Kent (Data61, Kensington NSW) < > Kent.Mcleod(a)data61.csiro.au> wrote: > >> > "../muslibc/include/sys"* // necessary for compilation as >> test_2.c has "socket.h"* >> This line shouldn't be here, and instead socket.h should be included via >> <sys/socket.h>. Otherwise many other include directives are going to match >> on the incorrect files. >> >> Kent. >> ------------------------------ >> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Chubb, Peter >> (Data61, Kensington NSW) <Peter.Chubb(a)data61.csiro.au> >> *Sent:* Friday, 14 June 2019 8:03 AM >> *To:* yogidk . >> *Cc:* devel(a)sel4.systems >> *Subject:* Re: [seL4] camkes error.h include problem >> >> >>>>> "yogidk" == yogidk <yogidk(a)gmail.com> writes: >> >> yogidk> and another file >> >> yogidk> test_2.c which includes "socket.h" >> >> yogidk> DeclareCAmkESComponent(test >> yogidk> INCLUDES "../muslibc/include/sys"* // necessary for >> yogidk> compilation as test_2.c has "socket.h"* >> >> This line means that "#include <errno.h>" picks up sys/errno.h instead >> of errno.h. >> >> Get rid of it. Instead, do '#include <sys/socket.h> instead of >> '#include <socket.h>' >> >> Peter C >> -- >> Dr Peter Chubb Tel: +61 2 9490 5852 >> http://ts.data61.csiro.au/ >> Trustworthy Systems Group Data61, CSIRO (formerly >> NICTA) >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> >

1 0

camkes error.h include problem
by yogidk . 14 Jun '19

14 Jun '19

Hi , I have a test_1.c file which includes <camkes.h> camkes.h which is automatically generated has following includes #include <camkes/dataport.h> #include <camkes/error.h> #include <stdint.h> #include <stdlib.h> #include <utils/util.h> #include <platsupport/io.h> and another file test_2.c which includes "socket.h" In CMakeLists.txt, where I compile my test_1.c and test_2.c looks like this DeclareCAmkESComponent(test INCLUDES "../muslibc/include/sys"* // necessary for compilation as test_2.c has "socket.h"* SOURCES "test_1.c" "test_2.c" C_FLAGS -Wall -Werror LIBS seos_libs ) However when I compile , I start getting these errors: In file included from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20:0, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] *#warning redirecting incorrect #include <sys/errno.h> to <errno.h>* ^~~~~~~ In file included from ../projects/musllibc/include/sys/errno.h:2:0, from ../projects/util_libs/libplatsupport/include/platsupport/io.h:20, from projects/test/include/camkes.h:20, from ../projects/src/test_1.c:8: ../projects/musllibc/include/sys/errno.h:1:2: error: #warning redirecting incorrect #include <sys/errno.h> to <errno.h> [-Werror=cpp] #warning redirecting incorrect #include <sys/errno.h> to <errno.h> How could this be solved ? thanks --yk

3 2

Roadmap - Status
by Rutherford, Luke 08 Jun '19

08 Jun '19

I see these on your development road map. Any updates on the status of them? Development Roadmap Microkernel in progress 64-bit ARM virtualisation support branch Low-level Userland Status Date Feature Location planned SMP-capable virtual-machine monitor (VMM) master

3 2

Re: [seL4] xilinx ultrascale+: Spurious interrupt
by Shen, Yanyan (Data61, Kensington NSW) 05 Jun '19

05 Jun '19

Hi Leonid, One possible cause I can think of is the trigger type (level vs edge) of an interrupt is incorrect. The Linux device tree should have interrupt type for each interrupt source, so you can change the GIC init code to configure the interrupt types (GICD_ICFGR, assuming GICv2) accordingly and see if the messages disappear. Regards, Yanyan From: Devel <devel-bounces(a)sel4.systems> on behalf of Leonid Meyerovich <lmeyerovich(a)i-a-i.com> Date: Wednesday, 5 June 2019 at 4:28 am To: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: [seL4] xilinx ultrascale+: Spurious interrupt Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

1 0

xilinx ultrascale+: Spurious interrupt
by Leonid Meyerovich 04 Jun '19

04 Jun '19

Hello Everybody, Petalinux is running on VM on the one of the core of Xilinx Ultrascale+ (A53) >From time to time I see Spurious Interrupt message from seL4 kernel (handleInterruptEntry) <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80080fa414]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff80083e64bc]: Spurious interrupt!>> <<seL4(CPU 1) [handleInterruptEntry/54 T0xff805da00400 "vm core" @ffffff800894cc98]: Spurious interrupt!>> Could somebody explain why it may happen? How to debug it? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

1 0

回复: Devel Digest, Vol 60, Issue 18
by KIM MK 03 Jun '19

03 Jun '19

Hello Sel4 developer, Thanks for your support. Aditya and me are debugging physical memory sel4. Is there visual tool or analysis module or anything to debugging that physical memory to virtual mapping table. If you have any question, please let me know. BR, MK

2 2

Multicore for 64-bit ARM
by Rutherford, Luke 24 May '19

24 May '19

I see this on your roadmap: https://sel4.systems/Info/Roadmap/ planned Multicore for 64-bit ARM and x64 master Do you have any updates on when this will be implemented?

2 1

How to add conditional compilation in .Camkes files
by yogidk 21 May '19

21 May '19

Hi, I try to add support for UART on one platform and disable this UART for another platform. As my application is Camkes based, I need to define the UART connections (Dataport, Interface functions etc) between the 2 Camkes components. However I need to use the same application on another platform without UART support. How can this be got in .Camkes files ? I already tried including a .h file where I define something like this In main.h #ifdef PLATFORM_X #define UART 1 #else #define UART 0 #endif Then include main.h file in Camkes files using a .idl4 file . However it did not work. .Camkes file is not able to see these defines to use it further for conditional compilation in .camkes files to enable or disable UART between the two components. Is there any way to get it done ? Regards yk

2 4

Compiling seL4
by Yousif Kako 21 May '19

21 May '19

Hello, I am a student researcher, I am trying to compile seL4 using the Configuring and building an seL4 project guidelines on your website ( https://docs.sel4.systems/Developing/Building/Using) And on the site, it says that after the command "ninja", I will be given binaries in the folder "images". But, I do not get such folder nor any images. I tried re-configuring some settings using cmake-gui but still nothing. I am want to write a user-level application but I am not sure if I am going about this the right way. If you have any suggestions or if you can point me in the right direction, that would be great. Thank You

2 1

Compilation Errors for the MCS tutorial
by Zeyu Mi 20 May '19

20 May '19

Hi, I was trying the MCS tutorial but encountered a few compilation errors which I cannot resolve. And the previous tutorials can be compiled normally. The building environment is based on Docker, as recommended by the tutorials. Steps: 1. cd kernel 2. git fetch seL4 mcs-tutorials 3. git checkout mcs-tutorials 4. cd .. && ./init --tut mcs 5. cd mcs && ninja Compilation output about the errors: [79/161] Building C object projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/elf.c.obj FAILED: projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/elf.c.obj ccache /usr/bin/gcc --sysroot=/host/mcs_build -DHAVE_AUTOCONF -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utic ../projects/seL4_libs/libsel4utils/src/elf.c: In function ‘rights_from_elf’: ../projects/seL4_libs/libsel4utils/src/elf.c:35:12: error: too many arguments to function ‘seL4_CapRights_new’ return seL4_CapRights_new(false, false, canRead, canWrite); In file included from ../kernel/libsel4/include/sel4/types.h:30:0, from ../kernel/libsel4/include/sel4/sel4.h:16, from ../projects/seL4_libs/libsel4utils/src/elf.c:15: libsel4/include/sel4/shared_types_gen.h:317:1: note: declared here seL4_CapRights_new(seL4_Uint64 capAllowGrant, seL4_Uint64 capAllowRead, seL4_Uint64 capAllowWrite) [82/161] Building C object projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/vspace/bootstrap.c.obj FAILED: projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/vspace/bootstrap.c.obj ccache /usr/bin/gcc --sysroot=/host/mcs_build -DHAVE_AUTOCONF -I../projects/seL4_libs/libsel4utils/include -I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64 -I../projects/seL4_libs/libsel4utic In file included from ../projects/seL4_libs/libsel4utils/src/vspace/bootstrap.c:20:0: ../projects/seL4_libs/libsel4utils/src/vspace/bootstrap.c: In function ‘common_init_post_bootstrap’: ../projects/seL4_libs/libsel4utils/include/sel4utils/vspace.h:43:43: error: ‘seL4_UserTop’ undeclared (first use in this function) #define KERNEL_RESERVED_START (ALIGN_DOWN(seL4_UserTop, PAGE_SIZE_4K)) Thanks in advance. Zeyu

2 5

Changing initial thread cnode guard
by Clifford, Alexandra - 0553 - MITLL 16 May '19

16 May '19

I am attempting to prototype an seL4 based system that ideally will have multiple threads, each with their own CSpaces which are each a tree e.g. not rooted in the initial cnode. My strategy here is to 1. chain new cnodes off of the initial cnode in the initial thread, and 2. Create a new thread TCB etc., revoke the initial cnode caps and set the new cnode cap as it’s own cnode root in that new thread. I have run into some issues at step 1 and am writing to ask if this is a viable strategy. Perhaps I am misunderstanding something but chaining in this way does not seem possible if all 32 bits are to be resolved in searching the initial cnode, so I am not certain if this strategy will work. Is it possible to configure the initial cnode guard to be something other than 32 bits? I have searched through the config of the kernel and cannot find some easily changed parameter for compile time, and for runtime I have tried to use the TCB_SetSpace and TCB_Configure on the initial thread to change the guard but this has lead to other problems. If I set it to something like 16, does this mean that all of the slot indices in the bootinfo struct are no longer valid as being set at 0x0, 0x1, etc and now will be at half word indices? It is very unclear to me from the documentation how this works but perhaps I am missing something. Setting it to something like 4 leads to an explicit TCB illegal operation and something larger like 19 returns seL4_Error 3 illegal op when I try to create new cnodes via untyped_retype from the init cnode. Is there something obvious that I am missing? I wonder if this is even possible—having cnodes not rooted in the initial cnode. Or if it is possible, is there some other mechanism to create a new cnode that is not rooted in the initial cnode? It is also probably important to note that due to constraints I am not able to use any of the nice sel4_libs provided to help with this. Thanks very much in advance for any help. Alexandra Clifford, MS 05-53 Secure Resilient Systems and Technology MIT Lincoln Laboratory 244 Wood st., Lexington MA 02421 Email: Alexandra.Clifford(a)ll.mit.edu

2 1

Possible newbie question: What are ".bf"-files belonging to the seL4 code base?
by Mike Epoch 15 May '19

15 May '19

Hi! I am new to this list so please forgive me if this question has been asked before. The seL4 code base contains a slew of files with a file type of "bf". These files seem to define packed structs that are to fit into words or d-words. An example of that would be file kernel/libsel4/mode_include/64/sel4/shared_types.bf which can be obtained (as part of an entire source tree, of course) via repo init -u https://github.com/seL4/sel4test-manifest.git followed by repo sync. What I find curious is that these files do not adhere to (common) C syntax yet they are fed into GCC and GCC swallows them. This file format appears to be an extension to GCC. I could not find any documentation on any such extension. I would be grateful if anyone could point me to some kind of documentation pertaining to it. Regards Mike

3 5

Using ARM GIC Virtualization Extensions with seL4
by dan pittman 10 May '19

10 May '19

Hi all! I'm currently trying to understand something about the use of the virtualization extensions available in the PL-400 interrupt controller in seL4. It all starts with this sentence: > The hypervisor supports virtualization also by using address translation tables to trap accesses that the virtual machines make to the virtual distributor. The hypervisor determines the effect of these accesses and might typically update the virtual interface control registers as a result. Source: http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0471b/CHDIHI… My interpretation of this is that by using the IPA which is available with arm hyp, the hardware can trap accesses to the GIC from the guest and "redirect" those accesses to the physical GIC. From this, I draw the conclusion that the need for a completely virtualized GIC when using these extensions is not necessary. However, in seL4—due to the way in which it manages interrupts by handling the hardware interactions itself and instead invoking an endpoint—the use of these extensions in this way is not possible. I'm curious if this understanding is correct, and if not, I welcome any clarity y'all can provide! cheers, dan

2 1

BeagleBone and CAmkES app picoserver
by KAP Benjamin 06 May '19

06 May '19

Hello I am trying to compile the CAmkES app picoserver for the BeagleBone Black but I do encounter some errors which I cannot manage to solve. Steps: - I repo synced the latest camkes-manifest which was added support for the BeagleBone - added am335x implementations to the Ethdriver global-component - created subfolder and issued ../init-build.sh -DPLATFORM=am335x -DSIMULATION=0 -DAARCH32=1 -DCAMKES_APP=picoserver - ninja Errors: [1/48] Building C object projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj FAILED: projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj ccache /usr/bin/arm-linux-gnueabi-gcc --sysroot=/host/PICO -DHAVE_AUTOCONF -I../projects/util_libs/libethdrivers/src/plat/am335x/cpsw -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/am335x -I../projects/util_libs/libethdrivers/arch_include/arm -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes-tool/libsel4camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/projects_libs/libusbdrivers/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/seL4_projects_libs/libsel4arm-vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/musllibc/build-temp/stage/include -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/am335x -I../projects/util_libs/libplatsupport/arch_include/arm -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/arm -Iprojects/util_libs/libpicotcp/picotcp_external/picotcp/build/include -march=armv7-a -marm -D__KERNEL_32__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mfloat-abi=softfp -std=gnu11 -MD -MT projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj -MF projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj.d -o projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/cpsw/cpswif.c.obj -c ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/cpswif.c In file included from ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/cpswif.c:47:0: ../projects/util_libs/libethdrivers/src/plat/am335x/cpsw/../lwiplib.h:46:22: fatal error: lwip/opt.h: No such file or directory #include <lwip/opt.h> ^ compilation terminated. [2/48] Performing build step for 'parse_capdl_tool' make: Nothing to be done for 'all'. [3/48] Building C object projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj FAILED: projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj ccache /usr/bin/arm-linux-gnueabi-gcc --sysroot=/host/PICO -DHAVE_AUTOCONF -I../projects/util_libs/libethdrivers/src/plat/am335x/cpsw -I../projects/util_libs/libethdrivers/include -I../projects/util_libs/libethdrivers/plat_include/am335x -I../projects/util_libs/libethdrivers/arch_include/arm -Iautoconf -Ikernel/gen_config -Ielfloader-tool/gen_config -Ilibsel4/gen_config -Iprojects/camkes-tool/libsel4camkes/gen_config -Iprojects/capdl/capdl-loader-app/gen_config -Iprojects/projects_libs/libusbdrivers/gen_config -Iprojects/rumprun/gen_config -Iprojects/seL4_libs/libsel4vka/gen_config -Iprojects/seL4_libs/libsel4utils/gen_config -Iprojects/seL4_libs/libsel4platsupport/gen_config -Iprojects/seL4_libs/libsel4serialserver/gen_config -Iprojects/seL4_libs/libsel4debug/gen_config -Iprojects/seL4_libs/libsel4test/gen_config -Iprojects/seL4_libs/libsel4muslcsys/gen_config -Iprojects/seL4_libs/libsel4vmm/gen_config -Iprojects/seL4_projects_libs/libsel4arm-vmm/gen_config -Iprojects/util_libs/libutils/gen_config -Iprojects/util_libs/libplatsupport/gen_config -Iprojects/util_libs/libethdrivers/gen_config -Iprojects/util_libs/libpicotcp/gen_config -Iprojects/musllibc/build-temp/stage/include -I../projects/util_libs/libplatsupport/include -I../projects/util_libs/libplatsupport/plat_include/am335x -I../projects/util_libs/libplatsupport/arch_include/arm -I../projects/util_libs/libutils/include -I../projects/util_libs/libutils/arch_include/arm -Iprojects/util_libs/libpicotcp/picotcp_external/picotcp/build/include -march=armv7-a -marm -D__KERNEL_32__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mfloat-abi=softfp -std=gnu11 -MD -MT projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj -MF projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj.d -o projects/util_libs/libethdrivers/CMakeFiles/ethdrivers.dir/src/plat/am335x/beaglebone.c.obj -c ../projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c ../projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c:17:24: fatal error: lwip/netif.h: No such file or directory #include <lwip/netif.h> ^ compilation terminated. ninja: build stopped: subcommand failed. Any help is very much appreciated. Best regards, Benjamin P.S. The file projects/util_libs/libplatsupport/plat_include/am335x/platsupport/plat/timer.h contains the static UNUSED timer_properties_t dmt_properties which caused errors on compilation too. (I deleted the lines since they arent used anyways)

2 1

Undefined Reference iommu dma
by KAP Benjamin 26 Apr '19

26 Apr '19

Hello I have a linking problem in the picoserver CAmkES-application which was added 2 days ago. Steps I did: 1) repo init -u https://github.com/seL4/camkes-manifest.git 2) repo sync 3) start docker container 4) (in new subfolder) ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=1 -DCAMKES_APP=picoserver (side note: aborts because picotcp folder is missing in projects folder, but that's easy fixed) 5) ninja Error: [5/16] Linking C executable projects/camkes/ethdriver.instance.bin FAILED: projects/camkes/ethdriver.instance.bin : && ccache /usr/bin/gcc --sysroot=/host/test -m64 -march=nehalem -D__KERNEL_64__ -g -march=nehalem -D__KERNEL_64__ -Wl,-m -Wl,elf_x86_64 -static -nostdlib -z max-page-size=0x1000 -static -nostdlib -u _camkes_start -e _camkes_start -Wl,--script=/host/test/projects/camkes/ethdriver/linker.lds /host/test/lib/crt1.o /host/test/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/6/crtbegin.o projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/ethdriver.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/82574.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.simple.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.environment.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/EthDriver_seL4HardwareMMIO_0.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/irq_seL4HardwareInterrupt_0.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/client_seL4Ethdriver_0.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/camkes-tool/libsel4camkes/libsel4camkes.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/util_libs/libutils/libutils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libethdrivers/libethdrivers.a projects/projects_libs/libvirtqueue/libvirtqueue.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4debug/libsel4debug.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a projects/util_libs/libplatsupport/libplatsupport.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a projects/util_libs/libpicotcp/picotcp_external/picotcp/build//lib/libpicotcp.a -lgcc -lgcc_eh libsel4/libsel4.a projects/camkes-tool/libsel4camkes/libsel4camkes.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/util_libs/libutils/libutils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libethdrivers/libethdrivers.a projects/projects_libs/libvirtqueue/libvirtqueue.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4debug/libsel4debug.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a projects/util_libs/libplatsupport/libplatsupport.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a projects/util_libs/libpicotcp/picotcp_external/picotcp/build//lib/libpicotcp.a /usr/lib/gcc/x86_64-linux-gnu/6/crtend.o /host/test/lib/crtn.o -o projects/camkes/ethdriver.instance.bin && : /usr/bin/ld: projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj: in function `camkes_iommu_dma_alloc': /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:48: undefined reference to `sel4utils_iommu_dma_alloc_iospace' /usr/bin/ld: projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj: in function `pc99_eth_setup': /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:71: undefined reference to `simple_get_iospace' /usr/bin/ld: /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:88: undefined reference to `sel4utils_make_iommu_dma_alloc' I checked all the files in the Ethdriver component and for me it seems that all should be fine, thus I cannot find/see the error (or the missing configuration). (The only file I edited was picoserver.camkes but that is irrelevant.) Any help/hint would be very appreciated. Best regards, Benjamin

1 1

seL4 process memory utilization
by Leonid Meyerovich 25 Apr '19

25 Apr '19

Hello, Is there any way in seL4 (library function?) to check free heap memory? Thank you, Leonid ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

4 5

Interested in Contributing to SeL4
by Aditya Upadhyay 26 Mar '19

26 Mar '19

Hi Developers, This is Aditya Upadhyay, would like to contribute in SeL4 microkernel. I am trying to figure out any open projects on wiki page of SeL4 Systems. One project that is related to POSIX Compliance. I can see here: https://docs.sel4.systems/SuggestedProjects.html but I am still figuring out the stuff to contribute. Any Valuable suggestions would be appreciated. Would you like to point any blogs related to SeL4? I have some experience of contributing the code in Open Source Organisation Newlib-Cygwin. I was working on POSIX Compliance for RTEMS as a part of Google Summer of Code 2017 Students internship. To stick to Open Source, I am mentoring RTEMS Google Summer of Code Project this year also. I have always learned from mentoring and contributing to open source. I have deep understanding of Linux Operating System Internals and Monolithic Kernels as well. I am also looking for Research Internship in Distributed Systems especially in Microkernel and Microhypervisor field. I am open for any research oriented projects in this field. Regards, Aditya Upadhyay

3 2

Re: [seL4] Devel Digest, Vol 58, Issue 5
by KIM MK 26 Mar '19

26 Mar '19

Okay! Aditya, Let’s research together :) BR, MK Sent from my iPhone > On 26 Mar 2019, at 6:43 AM, "devel-request(a)sel4.systems" <devel-request(a)sel4.systems> wrote: > > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Re: some questions about camkes-manifest > (Anna.Lyons(a)data61.csiro.au) > 2. Interested in Contributing to SeL4 (Aditya Upadhyay) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Mon, 25 Mar 2019 02:23:22 +0000 > From: <Anna.Lyons(a)data61.csiro.au> > To: <yadong.li(a)horizon.ai>, <devel(a)sel4.systems> > Subject: Re: [seL4] some questions about camkes-manifest > Message-ID: <1553480602203.73891(a)data61.csiro.au> > Content-Type: text/plain; charset="iso-8859-1" > > Hi, > > > 1. You can find the library in https://github.com/SEL4PROJ/projects_libs? > > 2. Sorry, we do not have any public demos that use this library. It has mainly been used in experimental contexts. > > > Cheers > > Anna. > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://sel4.systems/pipermail/devel/attachments/20190325/580f5330/attachmen…> > > ------------------------------ > > Message: 2 > Date: Mon, 25 Mar 2019 22:01:09 +0530 > From: Aditya Upadhyay <aditya.sidd.upadhyay(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Interested in Contributing to SeL4 > Message-ID: > <CAP7bF08qCr2dxd=WwbRwKuJP8ZqNc1RswNJbsfnyZ5Dxg1rjCg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Hi Developers, > > This is Aditya Upadhyay, would like to contribute in SeL4 microkernel. > > I am trying to figure out any open projects on wiki page of SeL4 Systems. > One project that is related to POSIX Compliance. I can see here: > https://docs.sel4.systems/SuggestedProjects.html > but I am still figuring out the stuff to contribute. Any Valuable > suggestions would be appreciated. Would you like to point any blogs related > to SeL4? > > I have some experience of contributing the code in Open Source Organisation > Newlib-Cygwin. I was working on POSIX Compliance for RTEMS as a part of > Google Summer of Code 2017 Students internship. > > To stick to Open Source, I am mentoring RTEMS Google Summer of Code Project > this year also. I have always learned from mentoring and contributing to > open source. > > I have deep understanding of Linux Operating System Internals and > Monolithic Kernels as well. I am also looking for Research Internship in > Distributed Systems especially in Microkernel and Microhypervisor field. I > am open for any research oriented projects in this field. > > Regards, > Aditya Upadhyay > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: <http://sel4.systems/pipermail/devel/attachments/20190325/3cbbe26b/attachmen…> > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 58, Issue 5 > ************************************

1 0

speed up sel4
by Sreenadh S 26 Mar '19

26 Mar '19

When running sel4 in my processor it is taking too long to get this line "vka_alloc_object_at_maybe_dev@object.h:65 Failed to allocate object of size 268435456, error 1" Is there any options to reduce allocation object size? Or any other methods to speed up Regards, Sreenadh S CDAC, Trivandrum, India

2 1

some questions about camkes-manifest
by yadong.li 25 Mar '19

25 Mar '19

hi, I have some questions about camkes-manifest 1、I find the libsdhcdrivers in /projects/projects_libs of the project. But where can I find the superset of these libs by git? I can't find the maintenance branch about libsdhcdrivers (like 'seL4_libs' ) in https://github.com/seL4 2、I can't find who use the function of libsdhcdrivers, what is the plan of the lib ? Is there some demo using sdhc ? Thank you very much

2 1

Hello. Nice to meet you. I’m MK
by KIM MK 11 Mar '19

11 Mar '19

Hello Micro kernel develper I’m MK. Nice to meet u. I’ll research and commit ARMv8 and virtualization in Sel4 你好。谢谢。 반갑습니다 Thank you BR， MK Sent from my iPhone

1 0

How to (and how not to) use seL4 IPC
by Gernot.Heiser＠data61.csiro.au 11 Mar '19

11 Mar '19

Folks might be interested in this blog: https://microkerneldude.wordpress.com/2019/03/07/how-to-and-how-not-to-use-… Gernot

2 3

ENTROPY 2019: Second Call for Papers
by Toby.Murray＠data61.csiro.au 20 Feb '19

20 Feb '19

NEW: two more invited speakers ********************************************************************** Second Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface https://protect-au.mimecast.com/s/h5JtCjZroMFQkjkKFW-1Th?domain=entropy2019… Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ********************************************************************** INVITED SPEAKERS Dominique Bolignano, Prove & Run Gernot Heiser, University of New South Wales Frank Piessens, KU Leuven Peter Sewell, University of Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (10 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://protect-au.mimecast.com/s/h5JtCjZroMFQkjkKFW-1Th?domain=entropy2019…. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers

1 0

Re: [seL4] port SeL4 to renesas rcar-H3 development board
by Diego Alejandro Parra Guzman 19 Feb '19

19 Feb '19

Hi guys !!! Thank you for your quick replay. I'm try to port Sel4 kernel to the* renesas H3 ULCB* board with two clusters (ARM57),(ARM53) each one with 4 cores I just have couple of questions regarding with the elf loader in sel4-tools: there is some files in* elfloader-tool/plat/** those are intended to initialize the CPU and the UART on the platform. In there, there is a function written in assembly called *core_entry_head* and a function *init_cpus*implemented in smp.c file. *Could you please explain me a little bit what is the purpose of these functions ? * In the case of *init_cpus* where is suppose to be that information? I means, I should reference the ARM57 or ARM53 cpu manual or maybe to the boot section in the SoC manual. from the other hand the *renesas H3 ULCB* doesn't have a physical UART port. Instead, it has an Serial Communication Interface with FIFO (SCIF) that can be configure properly to be compatible with *UART* interfaces. The point is that I'm using this interface in order to implement the * __fputc()* function following the one implemented in sys_fput.c file. Unfortunately, I don't understand why in your implementation there is not an initialization for the *UART. could you tell me why not?* Thank you. best regards On Sat, 16 Feb 2019 at 06:57, Diego Alejandro Parra Guzman < daparrag(a)correo.udistrital.edu.co> wrote: > Hi guys !!! > > Thank you for your quick replay. > > I'm try to port Sel4 kernel to the* renesas H3 ULCB* board with two > clusters (ARM57),(ARM53) each one with 4 cores > > I just have couple of questions regarding with the elf loader in > sel4-tools: > > there is some files in* elfloader-tool/plat/** those are intended to > initialize the CPU and the UART on the platform. In there, there is a > function written in assembly called *core_entry_head* and a function > *init_cpus*implemented in smp.c file. > *Could you please explain me a little bit what is the purpose of these > functions ? * > > In the case of *init_cpus* where is suppose to be that information? I > means, I should reference the ARM57 or ARM53 cpu manual or maybe to the > boot section in the SoC manual. > > > from the other hand the *renesas H3 ULCB* doesn't have a physical UART > port. Instead, it has an Serial Communication Interface with FIFO (SCIF) > that can be configure properly to be compatible with *UART* interfaces. > The point is that I'm using this interface in order to implement the > * __fputc()* function following the one implemented in sys_fput.c file. > Unfortunately, I don't understand why in your implementation there is > not an initialization for the *UART. could you tell me why not?* > > Thank you. > > best regards > > On Wed, 13 Feb 2019 at 15:21, Diego Alejandro Parra Guzman < > daparrag(a)correo.udistrital.edu.co> wrote: > >> >> Hi, >> >> I'm new with seL4 kernel and I would like to port it to the ARM-based >> renesas rcar-H3 board >> >> I would like to ask of you have a development manual that i can follow >> with some basics about how to do it? >> >> I followed the tutorials and so one. But I will appreciate if you have >> something guidelines to start. >> >> Thank you >> >> BR >> Diego. >> -- >> Diego Alejandro Parra Guzmán >> Estudiante de ingeniería electrónica >> Universidad distrital FJC >> > > > -- > Diego Alejandro Parra Guzmán > Estudiante de ingeniería electrónica > Universidad distrital FJC > -- Diego Alejandro Parra Guzmán Estudiante de ingeniería electrónica Universidad distrital FJC

2 3

sel4 at Developers Conference 2019
by Jheengut Pritvi 14 Feb '19

14 Feb '19

Hi, I have been following and keeping track of the development of sel4 for more than 3 years. Unfortunately, I have not been able to install sel4 on my odroid U3 and it also has been a long time that I have built and run sel4. I am also part of the organising team of the Developers Conference since 2015 and this year is the fifth edition held in the Voila hotel and Flying Dodo in Bagatelle in the Republic of Mauritius. This year, I have a session about sel4. https://sessionize.com/s/jheengut/an_introduction_to_the_sel4_microke/21360 I would be highly pleased to have a piece of your opinion on this matter. Cheers Pritvi Jheengut

1 0

port SeL4 to renesas rcar-H3 development board
by Diego Alejandro Parra Guzman 14 Feb '19

14 Feb '19

Hi, I'm new with seL4 kernel and I would like to port it to the ARM-based renesas rcar-H3 board I would like to ask of you have a development manual that i can follow with some basics about how to do it? I followed the tutorials and so one. But I will appreciate if you have something guidelines to start. Thank you BR Diego. -- Diego Alejandro Parra Guzmán Estudiante de ingeniería electrónica Universidad distrital FJC

4 3

Poll for Separation Kernel (microkernel) CC Protection Profile
by Holger Blasum 20 Jan '19

20 Jan '19

Hello seL4 devel, microkernel-based systems can be used as separation kernels[*] for security. At the moment there is a poll on input for a Common Criteria for Information Technology Security (CC) separation kernel protection profile draft, organized by a certMILS.eu colleague from Rostock Univ, at https://evasys.uni-rostock.de/evasys/online.php?p=ccuf-sk-wg The idea is to have a base protection profile (PP) that all players can agree with and to specify additional functionality as add-ons to the PP (e.g., in the form of PP modules). The questionnaire is an opportunity to provide early feedback. Note that there are no mandatory questions, i.e. you can freely move around / you can leave any question unanswered - the only condition for your feedback be submitted to the collection system is that you go to the last page and use the submit button there. We invite feedback via that poll by end of this week. If, beyond the questionnaire, you want to join the Common Criteria User's Forum separation kernel working group, or anyone would like to have more time, just let me know by answering to this email. [*] https://en.wikipedia.org/wiki/Multiple_Independent_Levels_of_Security Best, -- Holger Blasum, SYSGO

1 1

seL4 Training and ARMv8 virtualization release
by Robert VanVossen 18 Jan '19

18 Jan '19

All, We at DornerWorks wanted to let the seL4 community know about some seL4 training opportunities that we will be providing on behalf of the seL4 Center of Excellence (CoE). First, we will be providing an introductory webinar that provides an overview and explains the basics of seL4. Webinar: Intro to seL4 Thursday, February 7 11 a.m. EST Register Now: https://dornerworks.clickmeeting.com/intro-to-sel4/register Second, a more advanced two day training will take place on March 7th. This is a paid training that will provide information on seL4, libraries, CAmkES, the proof, and supported platforms. The training will also have hands-on labs that will include configuring CAmkES applications, debugging seL4 applications with GDB, and writing an HTTP server application to serve as a real life example. You can see more information and sign up here: https://www.sae.org/learn/content/c1874/ Finally, we wanted to let people know about our release of our ARMv8 virtualization feature. We recently received approval to release these features to the public. We have a press release providing additional details, a link to the code, and user instructions: https://dornerworks.com/news/new-commits-to-open-source-sel4. Currently, the release is on the DornerWorks github and based on an earlier version of seL4 and its libraries. We are working with Data61 to update to the latest versions and then mainline into the Data61 repositories. This may take some time as we integrate our ARMv8 virtualization code with Data61's ARMv8 virtualization code. Cheers, Robbie VanVossen DornerWorks, Ltd.

1 0

ENTROPY 2019: Call for Papers
by Toby Murray 13 Jan '19

13 Jan '19

************************************************************************** Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ************************************************************************** AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. INVITED SPEAKERS (to be extended) Frank Piessens, KU Leuven Peter Sewell, Univ. Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (8 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions: (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://entropy2019.sciencesconf.org. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers -- Toby Murray, DPhil (University of Oxford) Senior Lecturer, School of Computing and Information Systems University of Melbourne http://people.eng.unimelb.edu.au/tobym/ toby.murray(a)unimelb.edu.au

1 0

Running 2 VM Linux on Camkes
by Amit Goyal 08 Jan '19

08 Jan '19

Hi, I am using Ubuntu 16.04 on 64 Bit, i7 machine and following CAmkES x86 VM instructions available at: https://docs.sel4.systems/CAmkESVM I am able to successfully run single guest vm. I am now trying to run 2 guest vms at the same time. For this, I changed a) minimal.camkes as follows: -------------------------------------------------------------------------------------------------------------------------------- #ifdef HAVE_AUTOCONF #include <autoconf.h> #endif import <VM/vm.camkes>; #include <configurations/vm.h> #define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \ i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem" component Init0 { VM_INIT_DEF() } component Init1 { VM_INIT_DEF() } assembly { composition { VM_COMPOSITION_DEF() VM_PER_VM_COMP_DEF(0) VM_PER_VM_COMP_DEF(1) } configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) VM_PER_VM_CONFIG_DEF(1) vm0.simple_untyped23_pool = 20; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 128; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm1.simple_untyped23_pool = 20; vm1.heap_size = 0x2000000; vm1.guest_ram_mb = 128; vm1.kernel_cmdline = VM_GUEST_CMDLINE; vm1.kernel_image = "bzimage"; vm1.kernel_relocs = "bzimage"; vm1.initrd_image = "rootfs.cpio"; vm1.iospace_domain = 0x0f; } } --------------------------------------------------------------------------------------------------------------------------------- b) CMakeLists.txt as follows: --------------------------------------------------------------------------------------------------------------------------------- cmake_minimum_required(VERSION 3.8.2) project(minimal) # Include CAmkES VM helper functions include("../../vm/camkes_vm_helpers.cmake") include("../../vm-linux/vm-linux-helpers.cmake") # Declare VM component: Init0 DeclareCAmkESVM(Init0) DeclareCAmkESVM(Init1) # Get Default Linux VM files GetDefaultLinuxKernelFile(kernel_file) GetDefaultLinuxRootfsFile(rootfs_file) # Decompress Linux Kernel image and add to file server DecompressLinuxKernel(extract_linux_kernel decompressed_kernel ${kernel_file}) AddToFileServer("bzimage" ${decompressed_kernel} DEPENDS extract_linux_kernel) # Add rootfs images into file server AddToFileServer("rootfs.cpio" ${rootfs_file}) # Initialise CAmkES Root Server with addition CPP includes DeclareCAmkESVMRootServer(minimal.camkes) --------------------------------------------------------------------------------------------------------------------------------- I can successfully build the system and 2 vm images are being created namely: vm0_group.bin, vm1_group.bin On running the system using: sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=true --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0" I get the following error: --------------------------------------------------------------------------------------------------------------------------------- <<seL4(CPU 0) [decodeUntypedInvocation/209 T0xffbfec00 "rootserver" @804853d]: Untyped Retype: Insufficient memory (1 * 4194304 bytes needed, 2048 bytes available).>> <<seL4(CPU 0) [decodeInvocation/542 T0xffbfec00 "rootserver" @804853d]: Attempted to invoke a null cap #0.>> create_objects@main.c:767 [Err seL4_InvalidCapability]: Untyped retype failed with unexpected error seL4 root server abort()ed Debug halt syscall from user thread 0xffbfec00 "rootserver" halting... Kernel entry via Unknown syscall, word: 523QEMU: Terminated --------------------------------------------------------------------------------------------------------------------------------- I have 2 doubts: a) Can someone suggest a possible way to get this running. b) Is it possible to see the 2 VMs running on separate terminals at the same time. -- Thanks and Regards, Amit Goyal

2 2

An RFC process for seL4
by Curtis.Millar＠data61.csiro.au 02 Jan '19

02 Jan '19

Hi Everyone, We are currently in the process of setting up and moving to a public Jira instance to manage many of our development issues. The first part of this move involves setting up a request for comments (RFC) process which will be implemented using a Jira project. You can find out more about the RFC process in the first RFC: https://sel4kernel.atlassian.net/browse/RFC-1 You are encouraged to leave feedback on the issue, but doing so requires that you are logged in with an Atlassian Cloud account. The introduction of a public issue tracker will allow us to better engage with our community, accept more contribution from outside the seL4 development team, and better communicate the ways in which we are changing and improving the seL4 ecosystem. In the long term, we hope to use this to track all of the major issues currently under development across the ecosystem, accept issues submitted by the public, and open issues up for members of the greater community to work on. The issue tracker will initially be used as the basis of the RFC process, which will allow for the community to get involved with larger changes to the ecosystem. Many of the details of the process can only be clearly resolved as it becomes used more regularly as part of ongoing development, so much of how it works is still to be determined. We are hoping to finalise this process at the beginning of the new year before we use it to present a number of other changes we have been planning so we can get your feedback before their design and implementation is finalised. This new issue tracker and RFC process are just part of greater ongoing changes on which we are working to grow the community and to increase its involvement. We wish you all a happy holiday season and look forward to the start of a new year with seL4. Cheers, Curtis

2 2

seL4 at 35C3 in Leipzig (Chaos Communication Congress)
by Daniel Schäfer 26 Dec '18

26 Dec '18

Hey there, are some of you going to the 35C3 congress in Leipzig, Germany? I'm trying to understand seL4 and get into developing for it. I'd love to talk to someone if anyone's around. Best regards and merry Christmas, Daniel P.S. My "home" is the Selfnet assembly

1 0

Fwd: CAmkES tutorial build system
by Wei Xiang Leow 18 Dec '18

18 Dec '18

Hello Kent, Thanks for the reply :) The moving/copying was to demonstrate the differences between the tutorial and the solution. Creating and completing a new copy of the tutorial doesn't give the expected results either. My understanding is, when we run "./init --tut hello-camkes-1", the build directory is immediately built off the incomplete tutorial, hence it's missing client.instance.bin.dir etc. This isn't fixed when we complete the tutorial and ninja. Hence when someone goes through the tutorial, it doesn't give the expected "Starting the client". If this is the case, could you point me to where I can rectify this? On an separate note, I'm experiencing the same issues as https://sel4.systems/pipermail/devel/2018-October/002221.html. The simulate script exists, but qemu (at least 2.5.0+) seems to only allow "kernel-irqchip=on|off", not split. May I know which version of qemu we should be using? Regards, Leow Wei Xiang On Tue, Dec 18, 2018 at 2:10 PM <Kent.Mcleod(a)data61.csiro.au> wrote: > Hi, > > > Renaming the source directory and the build directories aren't supported > as CMake and Ninja rely on the absolute and relative paths remaining > consistent. You are still able to copy the contents of the source > directory from the solution into the source directory of the non solution > and use the same build directory. The reason why you only see ...Booting all > finished is because when the tutorial starts, there are no components > defined in the camkes assembly, so no components will be loaded by the > initial task. This is why you don't see any output. > > > I don't believe there is an issue, but let me know if I have misunderstood > what you meant. > > > Kind regards, > > Kent. > > > > ------------------------------ > *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Wei Xiang Leow < > leowweixiang1991(a)gmail.com> > *Sent:* Tuesday, December 18, 2018 4:42 PM > *To:* devel(a)sel4.systems > *Subject:* [seL4] CAmkES tutorial build system > > Hello, there seem to be issues with the tutorial build system, at least > for CAmkES tutorial 1. After adding the necessary details and running, I > get "...Booting all finished", no further messages. The solution runs fine, > I get "Starting the client" etc. > > Made fresh copies of the tutorial and solution, and overwrote the > tutorial's files with the solution's. Diff shows that only .tute_config > (--solution) and the .md files differ. Diff on the "_build" folders shows > multiple differences. I assume there is an issue there? > > mkdir tutorial; mkdir solution > ./init --tut hello-camkes-1 > mv hello-camkes-1 tutorial > mv hello-camkes-1_build tutorial > ./init --tut hello-camkes-1 --solution > mv hello-camkes-1 solution > mv hello-camkes-1_build solution > cp solution/hello-camkes-1/hello-1.camkes > tutorial/hello-camkes-1/hello-1.camkes > diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1 > ############################ > Files tutorial/hello-camkes-1/hello-camkes-1.md and > solution/hello-camkes-1/hello-camkes-1.md differ > Files tutorial/hello-camkes-1/.tute_config and > solution/hello-camkes-1/.tute_config differ > ############################ > > diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build > ############################ > Files tutorial/hello-camkes-1_build/build.ninja and > solution/hello-camkes-1_build/build.ninja differ > Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and > solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ > Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and > solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ > Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and > solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ > Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and > solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ > Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: > client.instance.bin.dir > Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: > echo.instance.bin.dir > Files > tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes > and > solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes > differ > Files > tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md > and > solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md > differ > Files tutorial/hello-camkes-1_build/rules.ninja and > solution/hello-camkes-1_build/rules.ninja differ > ############################ > > cp -r tutorial/hello-camkes-1 hello-camkes-1 > cp -r tutorial/hello-camkes-1_build hello-camkes-1_build > cd hello-camkes-1_build > ninja > ./simulate > ############################ > ... > Booting all finished, dropped to user space > ############################ > > <another terminal> > rm -r hello-camkes-1 > rm -r hello-camkes-1_build > cp -r solution/hello-camkes-1 hello-camkes-1 > cp -r solution/hello-camkes-1_build hello-camkes-1_build > cd hello-camkes-1_build > ninja > ./simulate > ############################ > ... > Booting all finished, dropped to user space > Starting the client > ------------------- > Component echo saying: hello world > After the client > ############################ > > Regards, > Leow Wei Xiang >

1 0

CAmkES tutorial build system
by Wei Xiang Leow 18 Dec '18

18 Dec '18

Hello, there seem to be issues with the tutorial build system, at least for CAmkES tutorial 1. After adding the necessary details and running, I get "...Booting all finished", no further messages. The solution runs fine, I get "Starting the client" etc. Made fresh copies of the tutorial and solution, and overwrote the tutorial's files with the solution's. Diff shows that only .tute_config (--solution) and the .md files differ. Diff on the "_build" folders shows multiple differences. I assume there is an issue there? mkdir tutorial; mkdir solution ./init --tut hello-camkes-1 mv hello-camkes-1 tutorial mv hello-camkes-1_build tutorial ./init --tut hello-camkes-1 --solution mv hello-camkes-1 solution mv hello-camkes-1_build solution cp solution/hello-camkes-1/hello-1.camkes tutorial/hello-camkes-1/hello-1.camkes diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1 ############################ Files tutorial/hello-camkes-1/hello-camkes-1.md and solution/hello-camkes-1/hello-camkes-1.md differ Files tutorial/hello-camkes-1/.tute_config and solution/hello-camkes-1/.tute_config differ ############################ diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build ############################ Files tutorial/hello-camkes-1_build/build.ninja and solution/hello-camkes-1_build/build.ninja differ Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: client.instance.bin.dir Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles: echo.instance.bin.dir Files tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes and solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes differ Files tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md and solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md differ Files tutorial/hello-camkes-1_build/rules.ninja and solution/hello-camkes-1_build/rules.ninja differ ############################ cp -r tutorial/hello-camkes-1 hello-camkes-1 cp -r tutorial/hello-camkes-1_build hello-camkes-1_build cd hello-camkes-1_build ninja ./simulate ############################ ... Booting all finished, dropped to user space ############################ <another terminal> rm -r hello-camkes-1 rm -r hello-camkes-1_build cp -r solution/hello-camkes-1 hello-camkes-1 cp -r solution/hello-camkes-1_build hello-camkes-1_build cd hello-camkes-1_build ninja ./simulate ############################ ... Booting all finished, dropped to user space Starting the client ------------------- Component echo saying: hello world After the client ############################ Regards, Leow Wei Xiang

2 1

Multiboot and extra modules
by Dave Richards 18 Dec '18

18 Dec '18

Is it (or would it be) possible to specify more than the single root server module and have seL4 create virtual addresses, cap. Spaces, threads (leaving them suspended) and pass the information about these modules to the root server? In this way it would be possible to have GRUB load a multi-server seL4 environment. Thanks, Dave

6 11

(no subject)
by Виктор Фадеев 14 Dec '18

14 Dec '18

Good day everyone! I want to try to port sel4 to mips. I will be grateful if you give me the literature that will help me understand the structure of sel4 and its logical interaction with arm/riscv.

1 0

Camkes Cross-VM Communication
by Amit Goyal 14 Dec '18

14 Dec '18

Hi All, I am using Ubuntu 16.04 on 64 Bit, i7 machine and running Camkes Cross-VM communication tutorial available at: https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html I am able to build the system properly but when I run the system, I get the following error: --------------------------------------------------------------------------------------------------------------------------------- Creating dataport node /dev/camkes_reverse_src Creating dataport node /dev/camkes_reverse_dest Allocating 8192 bytes for /dev/camkes_reverse_src dataport_map_guest@cross_vm_dataport.c:25 Dataport guest size and host size are different (8192 and 4096) dataport_vmcall_handler@cross_vm_dataport.c:75 Failed to map dataport into guest VM_FATAL_ERROR ::: vmexit handler return error vmm_print_guest_context:27 | ================== GUEST OS CONTEXT ================= vmm_print_guest_context:30 | exit info : reason 0x12 qualification 0x0 instruction len 0x3 interrupt info 0x0 interrupt error 0x0 vmm_print_guest_context:32 | guest physical 0x0 rflags 0x286 vmm_print_guest_context:34 | guest interruptibility 0x0 control entry 0x34 vmm_print_guest_context:37 | eip 0xd881714a vmm_print_guest_context:39 | eax 0x 1 ebx 0x 1 ecx 0x 1 vmm_print_guest_context:41 | edx 0x16a42000 esi 0x 2000 edi 0x 10 vmm_print_guest_context:43 | ebp 0xd6b17f0c vmm_print_guest_context:45 | cr0 0x80050033 cr3 0x16b1e000 cr4 0x2680 --------------------------------------------------------------------------------------------------------------------------------- I tried troubleshooting it a bit and changed the file: ~/camkes_vm_com/projects/vm-linux/camkes-linux-artifacts/camkes-linux-init-scripts/buildroot_init/camkes_init as follows: Earlier: dataport_init /dev/camkes_reverse_src 8192 /dev/camkes_reverse_dest 8192 Changed: dataport_init /dev/camkes_reverse_src 4096 /dev/camkes_reverse_dest 4096 But this also does not work. Please suggest. -- Thanks and Regards, Amit Goyal

2 2

Patent on formal verification
by Tom Mitchell 10 Dec '18

10 Dec '18

Patents possibly gone wrong. https://www.eff.org/deeplinks/2018/11/stupid-patent-month-patent-using-math… Claim 1 of the patent describes creating mathematical “axioms”—formal mathematical statements—that describe a computerized trading forum. The patented method then describes analyzing, with a “computer assessment system … the mathematical axioms that describe the operation of the trading forum.” In other words, the patent describes using formal proofs to check for bugs in a “computerized trading forum.” It’s formal verification—just applied to the financial services industry. -- T o m M i t c h e l l

1 0

Network lwip for imx6
by wong xuguo 10 Dec '18

10 Dec '18

Hi, I am a student fron Nanjing university, a fresh man of microkernel, specially, know very little about the seL4. Recently I accept a chellange about porting the lwip to sel4, on arch of imx6, does any one could give me a clue? I found the source of camkes does have this code, could I do something to port, to make the lwip work? What my aim is make a tcp echo server. Thank you for all of you help. Best regards from Xuguo Wang

4 4

sel4 on Raspberry Pi 3b Not Working
by Amit Goyal 06 Dec '18

06 Dec '18

Hi All, I tried running seL4 on Raspberry Pi 3b using the following links: https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I get the following: CACHE: Misaligned operation at range [20000000, 20000014] CACHE: Misaligned operation at range [20008c80, 200092ef] CACHE: Misaligned operation at range [200192f0, 203bb4f0] CACHE: Misaligned operation at range [203bc000, 203c6030] CACHE: Misaligned operation at range [203c6030, 203c8000] ## Starting application at 0x20000000 … and then nothing works and the processor halts. I have tried the pre-built uboot binary, complied uboot versions v2017.1 and v2016.11 as suggested by steve sloloski (on the blog) and uboot version v2016.05 (out of curiosity) but nothing works. Can someone please suggest a possible way out. -- Thanks and Regards, Amit Goyal

2 4

[sel4] Building seL4test for x86_64 on Debian
by Dave Richards 05 Dec '18

05 Dec '18

I thought I got all of the host dependencies installed, but evidently I am doing something wrong. I am building on a Debian 9 (x86_64) system. I ran the init script from the build directory with the -DPLATFORM=x86_64 and -DSIMULATION=0 options. I then ran ninja with no options. Please find attached the output of running these 2 steps. I'd appreciate a gentle nudge in the right direction. Thanks! Dave

1 0

Building seL4x86_64 on Debian
by Dave Richards 05 Dec '18

05 Dec '18

I thought I got all of the host dependencies installed, but evidently I am doing something wrong. I am building on Debian 9 (x86_64) system. I ran the init script from the build directory with the -DPLATFORM=x86_64 and -DSIMULATION=0 options. I then ran ninja with no options. Please find attached the output of running these 2 steps. I'd appreciate a gentle nudge in the right direction. Thanks! Dave

3 2

seL4 cache pinning
by 송대영 02 Dec '18

02 Dec '18

Hi, I read "Improving Interrupt Response Time in a Verifiable Protected Microkernel" paper. This paper improved IPC performance by using cache pinning and I want to know how to implement cache pinnng. But this paper doesn't refer how to manipulate cache lines. Would you give me some methods how to read cache lines and write cache lines?

3 2

Is the ASID used in seL4 by default?
by Dd Nirvana 02 Dec '18

02 Dec '18

Hi guys, I found that seL4's ARM version still need "isb" and "dsb" around updating TTBR0_EL1. This fence will flush the TLB and will affect IPC performance. However, it seems that enabling ASID can avoid this costs. I am not sure, is there any concern that makes seL4 to avoid using ASID? BTW, I have seen ASID management in seL4 (ASID control and ASID pool), so maybe I misunderstood something? Dong Du, Shanghai Jiao Tong University

2 1

sel4bench config problem
by 송대영 23 Nov '18

23 Nov '18

Hi, I have a sel4bench config problem. I use 'ccmake ..' command to configure sel4 configuration but system prints error with this message. Build files have been written to: /home/scribnote5/sel4bench_thesis/build CMake Warning at tools/seL4/cmake-tool/flags.cmake:123 (message): Kernel supports hardware floating point but toolchain does not Call Stack (most recent call first): tools/seL4/cmake-tool/base.cmake:58 (include) tools/seL4/cmake-tool/all.cmake:18 (include) CMakeLists.txt:21 (include) Please help me!

2 1

seL4 stack overflow
by Anna.Lyons＠data61.csiro.au 21 Nov '18

21 Nov '18

Hi everyone, I've created a proposal for an seL4 stack overflow, which will complement the mailing list. Please support it! https://area51.stackexchange.com/proposals/120611/sel4?referrer=oNjnX5y9POx… Cheers, Anna.

2 1

seL4 on Raspberry 3
by talos 19 Nov '18

19 Nov '18

Hi Did anyone try seL3 on raspberry pi 3? I tried following these links:https://research.csiro.au/tsblog/sel4-raspberry-pi-3/ https://docs.sel4.systems/Hardware/Rpi3.html https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html#fnref1 I set the serial port 115200, 8N1, but I only got some messy codes, I did not get the booting information! Did anyone find this cases? Thanks Sincerely

2 1

Re: [seL4] seL4 10.1.0 and camkes-3.6.0
by jonas.cl＠protonmail.com 15 Nov '18

15 Nov '18

Hi, Today I created a few pull-requests on seL4 repos to build x86-64 with clang: - https://github.com/seL4/seL4/pull/105 - https://github.com/seL4/musllibc/pull/4 - https://github.com/seL4/seL4_tools/pull/19 /Jonas ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Wednesday, November 14, 2018 5:28 PM, <devel-request(a)sel4.systems> wrote: > Message: 3 > Date: Wed, 14 Nov 2018 16:28:17 +0000 > From: Andy Helten andy.helten(a)goctsi.com > To: "Matthew.Brecknell(a)data61.csiro.au" > Matthew.Brecknell(a)data61.csiro.au, "devel(a)sel4.systems" > > <devel(a)sel4.systems> > > > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > Message-ID: > DM6PR17MB2314D1EF141DD6DD6A4779BE92C30(a)DM6PR17MB2314.namprd17.prod.outlook.com > > Content-Type: text/plain; charset="utf-8" > > Disclaimer: I've never compiled sel4 nor executed sel4 and, at this point, am just a follower of this mailing list (with tentative plans to use sel4 "someday") > > Regarding the issue that was fixed here, my first thought was "why did the compiler not complain?". My next thought was "maybe sel4 doesn't enable all warnings in their builds or they ignore the warnings!" But surely a kernel that focuses on security would enable all compiler warnings and fix them immediately as they are introduced. > > Turns out it doesn't matter what sel4 builds are doing, the gcc compiler has a bug that prevents warnings for several of these common "might be used uninitialized" cases. See here: > > https://gcc.gnu.org/bugzilla/show_bug.cgi?id=18501 > > It also appears this bug will not be fixed! An alternative for some projects, though maybe not sel4, is to also compile their code with clang, which does catch these uninitialized cases. If sel4 can use clang to catch these types of mistakes earlier, in a compiler warning, it might save a lengthy validation procedure to catch the error (if it gets caught at all). > > Just thought folks might be interested in this gcc bug -- I certainly wasn't aware of it. > > Andy > > -----Original Message----- > From: Devel devel-bounces(a)sel4.systems On Behalf Of Matthew.Brecknell(a)data61.csiro.au > Sent: Thursday, November 8, 2018 7:22 PM > To: devel(a)sel4.systems > Subject: Re: [seL4] seL4 10.1.0 and camkes-3.6.0 > > Hi, > > Now that the fix for this issue has made it through our integration pipeline, I can explain what happened, since some of you might be interested. The fix is here: > > https://github.com/seL4/seL4/commit/d12bb374ab47d2b13f438969d2eb5dde1021af84 > > At line 56, the target variable was originally declared uninitialised. > If the loop at lines 57 to 64 executes at least once, then the variable is initialised at line 58. But if the loop does not execute, then the variable would remain uninitialised when it is used at line 65. This would be the case if infer_cpu_gic_id was ever called with nirqs <= 0. > This is not a problem in the released kernel, becuase infer_cpu_gic_id is only ever called once in dist_init, with 32 <= nirqs <= 1024. > > However, the binary translation validation test that failed does not do the inter-procedural analysis that would be necessary to realise this. > When looking at infer_cpu_gic_id, the analysis allows nirqs to take any value. It considers that the loop might not execute, and therefore target might be uninitialised when it is used at line 65. The dataflow model that is produced by the analysis cannot model such undefined behaviour, and so the test fails. With the fix, the variable is never uninitialised, so the analysis does not run into this problem. > > In summary, the fix you see here keeps our proofs happy, but it does not increase the safety of the kernel. This function, as it is actually used, was already safe. > > In terms of our development process, this kind of failure in the binary translation validation is quite rare and difficult to predict. And since our proofs take quite a long time to run, we don't always insist that our kernel developers run the proofs for changes in boot code, which is currently unverified except for binary translation validation. We accept that these failures will occasionally happen, and we deal with them when they do. The functions dist_init and infer_cpu_gic_id are boot-only code, so this was one of those rare failures. > > Of course, we should insist on running all the tests for versions we intend to formally release, and we will for future releases. > > Best regards, > Matt > > From: Brecknell, Matthew (Data61, Kensington NSW) > Sent: Thursday, 8 November 2018 11:25 AM > To: devel(a)sel4.systems > Cc: Mcleod, Kent (Data61, Kensington NSW) > Subject: Re: seL4 10.1.0 and camkes-3.6.0 > > Hi, > > Due to an oversight on my part, seL4 10.1.0 was released without passing the full verification test suite. > > We have no reason to believe that there is any problem in the verified parts of this seL4 version. > > The test that failed is part of the binary translation validation, which produces a dataflow graph from the Isabelle/HOL model of the C code, and then attempts to automatically prove a refinement relation between the C and that dataflow graph. The failure occurred in boot code, which in any case is currently not verified. The failure does not mean that there is any problem with the C code. Most likely, it just means that some new code uses some C idiom which is currently not handled by the automatic translation process. > > All other components of the verification test suite pass, including security proofs and functional correctness proofs for the Isabelle/HOL model of the C code. > > Nevertheless, we intend to rectify this failure as soon as possible, and we'll make further announcements when we understand what happened. > > I want to reiterate that this was entirely my fault, and was not at all Kent's fault. > > Best regards, > Matt > > From: Devel devel-bounces(a)sel4.systems on behalf of Kent.Mcleod(a)data61.csiro.au Kent.Mcleod(a)data61.csiro.au > Sent: Thursday, 8 November 2018 8:44 AM > To: devel(a)sel4.systems > Subject: [seL4] seL4 10.1.0 and camkes-3.6.0 > > See an online copy of the release notes at: > https://docs.sel4.systems/sel4_release/seL4_10.1.0 > https://docs.sel4.systems/camkes_release/Camkes_3.6.0 > > 10.1.0 2018-11-07: SOURCE COMPATIBLE > > Changes > > -------- > > - structures in the boot info are not declared 'packed' > - these were previously packed (in the GCC attribute sense) > - some field lengths are tweaked to avoid padding > - this is a source-compatible change > - ARM platforms can now set the trigger of an IRQ Handler capability > - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability > and set the trigger (edge or level) in the interrupt controller. > > - Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57) > - AARCH64 support added for raspberry pi 3 platform. > - Code generation now use jinja2 instead of tempita. > - AARCH32 HYP support added for running multiple ARM VMs > - AARCH32 HYP VCPU registers updated. > - A new invocation for setting TLSBase on all platforms. > - seL4_TCB_SetTLSBase > - Kbuild/Kconfig/Makefile build system removed. > > camkes-3.6.0 2018-11-07 > Using seL4 version 10.1.0 > > Changes > > -------- > > - AARCH64 is now supported. > - CakeML components are now supported. > - Added `query` type to Camkes ADL to allow for querying plugins for component configuration values. > - Components can now make dtb queries to parse device information from dts files. > - Component definitions for serial and timer added on exynos5422, exynos5410, pc99. > - Preliminary support for Isabelle verification of generated capDL. > - See cdl-refine-tests/README for more information > - Simplify and refactor the alignment and section linking policy for generated Camkes binaries. > - Dataports are now required to declare their size in the ADL. > - Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. > - This change is BREAKING. > - Remove Kbuild based build system. > - Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. > - Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. > > > Upgrade Notes > > -------------- > > - Any dataport definitions that did not specify a size must be updated to use a size. > - Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. > - Projects must now use the new Cmake based build system. > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > -------------------------------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > --------------------------------------------------------------------------------- > > End of Devel Digest, Vol 54, Issue 12

2 1

seL4 10.1.0 and camkes-3.6.0
by Kent.Mcleod＠data61.csiro.au 14 Nov '18

14 Nov '18

See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_10.1.0> <https://docs.sel4.systems/camkes_release/Camkes_3.6.0> 10.1.0 2018-11-07: SOURCE COMPATIBLE ## Changes * structures in the boot info are not declared 'packed' - these were previously packed (in the GCC attribute sense) - some field lengths are tweaked to avoid padding - this is a source-compatible change * ARM platforms can now set the trigger of an IRQ Handler capability - seL4_IRQControl_GetTrigger allows users to obtain an IRQ Handler capability and set the trigger (edge or level) in the interrupt controller. * Initial support for NVIDIA Jetson TX2 (ARMv8a, Cortex A57) * AARCH64 support added for raspberry pi 3 platform. * Code generation now use jinja2 instead of tempita. * AARCH32 HYP support added for running multiple ARM VMs * AARCH32 HYP VCPU registers updated. * A new invocation for setting TLSBase on all platforms. - seL4_TCB_SetTLSBase * Kbuild/Kconfig/Makefile build system removed. ---- camkes-3.6.0 2018-11-07 Using seL4 version 10.1.0 ## Changes * AARCH64 is now supported. * CakeML components are now supported. * Added `query` type to Camkes ADL to allow for querying plugins for component configuration values. * Components can now make dtb queries to parse device information from dts files. * Component definitions for serial and timer added on exynos5422, exynos5410, pc99. * Preliminary support for Isabelle verification of generated capDL. - See cdl-refine-tests/README for more information * Simplify and refactor the alignment and section linking policy for generated Camkes binaries. * Dataports are now required to declare their size in the ADL. * Templates now use seL4_IRQHandler instead of seL4_IRQControl, which is consistent with the seL4 API. - This change is BREAKING. * Remove Kbuild based build system. * Remove caches that optimised the Kbuild build system, which are not required with the new Cmake build system. * Added virtqueue infrastructure to libsel4camkes, which allows virtio style queues between components. ## Upgrade Notes * Any dataport definitions that did not specify a size must be updated to use a size. * Any template that used seL4_IRQControl must be updated to use seL4_IRQHandler. * Projects must now use the new Cmake based build system.

4 4

Data61 Seeking Research Scientist
by Gerwin.Klein＠data61.csiro.au 14 Nov '18

14 Nov '18

Data61 Seeking Research Scientist ================================= We are looking for a full-time research scientist in formal verification to join us, the Trustworthy Systems group, at Data61, CSIRO. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities. Our vision is a world in which computer users can choose all three: correct, secure, and fast. We believe that most current approaches to building systems are fundamentally flawed. We aim to demonstrate a better way. Our approach is rooted in foundational, formal verification using theorem provers (e.g., Isabelle, HOL4), and high-performance system design. If you find this vision appealing, and have ideas about how to pursue it, we want to hear from you. Our team brings together a unique combination of expertise in systems, security, formal verification, and programming languages. We are the creators of seL4, the world's first operating system microkernel with a machine-checked proof (in Isabelle/HOL). seL4 boasts both extreme performance and foundational binary-level correctness and security proofs. We are also involved in CakeML, the most realistic verified compiler for a functional programming language, and a promising approach to scaling full verification up to applications code. We are building on these successes in various directions, including concurrency (formal reasoning and implementation), timing (real-time guarantees and timing channels), and whole-system verification using component systems (e.g., CAmKES) and code+proof co-generation. We publish in top conferences, and are involved in multiple international research collaborations. You will have the opportunity to teach at UNSW should you wish to take it. We have a flexible, friendly, and intellectually stimulating work environment. We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information. The salary range for this position (plus superannuation) is - Research Scientist: 97k-105k - Senior Research Scientist: 111k-130k depending on experience and qualifications. Apply online here: https://jobs.csiro.au/job/Sydney%2C-NSW-Research-ScientistSenior-Research-S… Your application should include a cover letter, CV, short research statement, and contact information for two references. This round of applications closes on 15 January 2019. For any questions on this position, please contact June.Andronick(a)data61.csiro.au

1 0

Data61 Seeking Proof Engineers
by Gerwin.Klein＠data61.csiro.au 14 Nov '18

14 Nov '18

Data61 Seeking Proof Engineers ============================== We are are hiring again! If only there were a place where I could prove theorems for money, change the world, and have fun while doing it... Sounds too good to exist? In the Trustworthy Systems team at Data61 that's what we do for a living. We are the creators of seL4, the world's first fully formally verified operating system kernel with extreme performance and strong security & correctness proofs. Our highly international team is located on the UNSW campus, close to the beautiful beaches of sunny Sydney, Australia, one of the world's most liveable cities. We are looking for multiple motivated proof engineers who want to join our team in Sydney, move things forward, and have global impact. You would - work on industrial-scale formal proofs in Isabelle/HOL - develop formally verified infrastructure for building secure systems on top of seL4 - contribute to improved proof automation and reasoning techniques - apply formal proof to real-world systems and tools To apply for this position, you should possess a significant subset of the following skills. - functional programming in a language like Haskell, ML, or OCaml - first-order or higher-order formal logic - basic experience in C - ability and desire to quickly learn new techniques - undergraduate degree in Computer Science, Mathematics, or similar - ability and desire to work in a larger team We are hiring at two levels, so if you are more qualified or experienced than the above would suggest, you can come in as a senior proof engineer. If you additionally have experience - in software verification with an interactive theorem prover such as Isabelle/HOL, HOL4, or Coq, and/or - with operating systems and microkernels you should definitely apply! If you have the right skills and background, we can provide training on the job. Continual learning is a central component of everything we do. You will work with a unique world-leading combination of OS and formal methods experts, students at undergraduate and PhD level, engineers, and researchers from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun, creative, and welcoming workplace with flexible hours & work arrangements. We value diversity in all forms and welcome applications from people of all ages, including people with disabilities, and those who identify as LGBTIQ. See https://ts.data61.csiro.au/diversity/ for more information. Salary ranges, in AUD (plus superannuation): - Junior Proof Engineer: 73k-93k - Senior Proof Engineer: 97k-105k depending on experience and qualifications. Apply online at the following link for the Proof Engineer positions: - https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/518443000/ - https://jobs.csiro.au/job/Sydney%2C-NSW-DATA-61/518441000/ Your application should include a cover letter, CV, undergraduate transcript (if applicable), and contact information for two references. This round of applications closes on 17 December 2018. For any questions on these positions, please contact Rafal.Kolanski(a)data61.csiro.au or June.Andronick(a)data61.csiro.au The seL4 code and proof are open source. Check them out at https://seL4.systems More information about Data61's Trustworthy Systems team at https://ts.data61.csiro.au There are additional proof engineering positions available on the Cogent project. Cogent is a language we designed to ease the verification of systems components around seL4. For expressions of interest, see contact details on https://ts.data61.csiro.au/projects/TS/cogent.pml Looking to do a PhD? Data61 and UNSW (https://www.unsw.edu.au/) offer scholarships! See https://ts.data61.csiro.au/students/research.pml for details.

1 0

Scheduling of vCPUs on x86
by Alexander Boettcher 10 Nov '18

10 Nov '18

Hello, the time spend by a vCPU TCB (tcbTimeSlice) seems to be not accounted/updated by the seL4 kernel on a timer ticks, which leads to starvation of other TCBs running on the same or lower priority level. In one of our test setups, if once a vCPU runs and doesn't give up its timeslice willful (e.g. guest goes in while loop and thereby not causing a VM exit to be handled by the VMM), all other TCBs (normal threads and vCPUs) on the same timeslice are not considered to be scheduled again, since tcbTimeSlice of the vCPU stays full forever. Following patch seems to fix the issue. Can you please have a look and verify that it is correct ? Or should it be solved on another place in the kernel differently. Just out of curiosity, why is a separate thread state in the scheduler for x86 (CONFIG_VFX) required that is not needed for scheduling of a vCPU on ARM ? I didn't expect the scheduler thread states to be different between hardware architectures in seL4. Cheers, -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

5 8

sel4bench IPC questions
by 송대영 08 Nov '18

08 Nov '18

HI, I have a question about sel4bench IPC. Thanks for the reply. 1. Making seL4_IPCBuffer and mapping into the thread is necessary? I think that sending short messages don't need seL4_IPCBuffer, is it right? 2. This is seL4_Call annotation in benchmark_param. /* Call fastpath between client and server in the different address space */ But I can't understand how to measure seL4_Call function performance. [Client thread] [Server thread] seL4_Call seL4_ReplyRecv(I'm not sure) 1) client send message. 2) server receive message. 3) server send message. 4) client receive message. seL4_Call performance in sel4bench excluding overhead , is it right? = 1) + 2) + 3) + 4) - 3) - 4) 3. This is seL4_Send annotation in benchmark_param. /* Send slowpath (no fastpath for send) same prio client-server, different address space */ But client_prio(seL4_MaxPrio - 1) and server_prio(seL4_MaxPrio - 2) is different.

2 1

Support for QNX-like booting from an XIP filesystem image
by Andrew Warkentin 07 Nov '18

07 Nov '18

For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I have patched seL4 to support for booting from an in-memory execute-in-place filesystem image that contains the kernel and all user-mode programs required to mount the root filesystem (similar to that of QNX, but with more of the functionality in the bootloader rather than the root server). The existing seL4 boot process may be OK for static embedded systems that are always cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with a boot image that will include files from multiple separately-installed packages and will possibly be customized to the system it is installed on. Requiring any image filesystem to be linked into the root server makes updating boot images more complex than being able to use a simple filesystem builder to make an image containing the kernel, root server, and everything else that is required (the main special considerations being placing the kernel and root server at fixed physical addresses and padding the image to allow for bss sections, which are easy enough). Also, I want it to be easy to manually boot UX/RT images, so you can just type something like "boot (hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most older Unices), and the bootloader will automatically load the kernel and all required modules from within the image as opposed to having to type a lot of boilerplate to load the kernel and root server (and anything else that may be required). In addition I don't think that the root server should need to have any support for parsing image filesystems and should be able to obtain all the files required for early boot from the MBI. I am using Multiboot2 with a few custom tags added and a few extra requirements regarding placement of modules. I currently have an in-memory loader that implements my variant of Multiboot2, and eventually want to implement a full disk-based bootloader. I have also implemented a page-oriented in-memory filesystem called XRFS (originally based on Linux romfs) with support for placing files at fixed addresses. The in-memory loader was parsing the filesystem and using a script to locate the modules within the image, although I have decided that it is overkill to do that, and it would allow the loader to be simpler if the filesystem image has its own MBH separate from that of the kernel (the magic number will be different from the kernel MBH as well), with tags for the kernel and each module, so that the loader's existing MBH-parsing code can be used to locate files in the image. As far as my kernel patches go, they extend the existing Multiboot2 code and do not interfere with the existing boot code. Right now they are x86-only, but I am planning to add Multiboot2 support to other architectures eventually as well. They do not introduce any dependency on my filesystem format in the kernel (it does know that there is an FS image and that there are modules contained within it, and assumes that modules are contiguous). Relocation of the root task is disabled when an FS image is present, since it will already be placed in a usable location in the image. Kernel-level ELF loading of modules is also disabled when using my Multiboot2 extensions, since my loader is capable of parsing ELF modules, loading them, and passing information on module sections and addresses to the kernel through tags. The part of the image containing the kernel is inaccessible to the root task for obvious reasons, so an additional requirement is that the kernel is the first file in the image, followed by the root server, and then all other files (XRFS is structured to allow the remainder of the image to be read even though the beginning is inaccessible). There is also support for passing the MBI through to the root task, which requires that the MBI is allocated immediately after the end of the filesystem image (a new structure is added to the bootinfo to provide the root server with the address of the MBI). >From what I've said, would there be any problems with including my patches in the mainline seL4 repository? Only the boot code is modified. Loading the root server works, but I haven't yet tested the MBI passthrough, so I am not quite ready to submit anything (currently I am working on converting my bootloader from parsing the filesystem itself to parsing an MBH in the FS image, like I said before).

2 3

Non CAmkES VM on x86
by Chris Guikema 07 Nov '18

07 Nov '18

DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed). Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released? Thanks, Chris Guikema

2 1

seL4 on Heterogeneous Processing Architectures (Zynq UltraScale+ MPSoCs)
by Blam Kiwi 06 Nov '18

06 Nov '18

I am investigating the use of seL4 on heterogeneous architectures such as the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm investigating that involves utilising both the Cortex-R5 cores and Core-A53 cores for different applications. I'm rather new to seL4 development so I'm a bit stuck and need some advice. It's easiest if I just list my requirements and assumptions for my architecture design: a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS Kernel to manage system resources and run virtual machines. b) I require the use of the Cortex R5 cores in DCLS mode for trusted code with high fault tolerance requirements. c) I require the use of the Cortex A53 cores for running unsafe Linux VMs. d) It's my understanding that seL4 lacks 64-bit multicore support for its own scheduler, but VMs running on seL4 could be provided with access to all the cores? (Eg: Linux) e) It's my understanding that seL4 lacks heterogeneous task scheduling, and cannot manage both the Cortex R5 and Cortex A53 cores. This leads me to make the following architectural conclusions: [1] It's not possible to boot an seL4 kernel on one processor and have it manage the other. [2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and boot an seL4 kernel on each. [3] Some domain specific protocol is required for the CPU modules to communicate and share resources. Any help or advice would be appreciated. Regards, Robbie

4 4

Passing Network Resource to Linux VM in TK1-SOM
by Daniel Wang 06 Nov '18

06 Nov '18

Hi all, I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint? Best Regards -Daniel Wang

2 2

run docker on sel4
by Jia He 06 Nov '18

06 Nov '18

Hi all I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker. I am investigating the proper implemenatation for running docker on sel4 on arm64. There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated. Is there any other ways or anything else to make the implatation more feasible? --- Cheers, Justin

3 2

seL4 IPC and SMP question.
by 송대영 05 Nov '18

05 Nov '18

HI, I have a question about IPC and SMP. I ran sel4bench on sabre lite(i.mx6, arm v7). 1. I want to confirm performance difference between Lazy Scheduling and Beno Scheduling. Can I configure scheduler? 2. Can you explain the difference when thread state is "ThreadState_Running" and "ThreadState_Restart"? 3. I tried "SMP Benchmark" but I can't understand what this benchmark exactly means. What "Cycles" means in this benchmark? smp : This is an intra-core ipc round-trip benchmark to check overhead of the kernel synchronization on ipc throughput. 4. I try to measure IPC performance with SMP is on. I used "seL4_TCB_SetAffinity" function so server executed in Core1 and client executed Core2. But performance results are too excessive. seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles. Are these results are available?

3 2

Booting seL4test on x86 hardware
by Alex Pavey 30 Oct '18

30 Oct '18

Hello, We are having issues being able to get the seL4test userland image to boot on x86 hardware. We have attempted to boot with syslinux off a USB, with PXELINUX, and with grub and see the same userland image loading issue across boot methods. Build steps: - Following https://docs.sel4.systems/Hardware/IA32 - Using "-DPLATFORM=x86_64" o Does not appear to boot (no serial output) - Using "-DPLATFORM=ia32" o Kernel boots but is unable to load userland image The manifest commit hash is: 01c11cfcd881c1da5b7520162fae40f6eae1c16b Hardware: - DELL Optiplex 980 with an Intel Core i7 860 processor We are seeing the following serial output: SYSLINUX 6.03 20171017 Copyright (C) 1994-2014 H. Peter Anvin et al Loading sel4kernel... ok Loading rootserver... ok Boot config: parsing cmdline 'sel4kernel' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false Detected 1 boot module(s): module #0: start=0x1d6000 end=0x4abdf4 size=0x2d5df4 name='rootserver' Parsing GRUB physical memory map Physical Memory Region from 0 size 9e400 type 1 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size df5cfc00 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from df6cfc00 size 54000 type 4 Physical Memory Region from df723c00 size 2000 type 3 Physical Memory Region from df725c00 size 8da400 type 2 Physical Memory Region from f8000000 size 4000000 type 2 Physical Memory Region from fed00000 size 400 type 2 Physical Memory Region from fed20000 size 80000 type 2 Physical Memory Region from fec00000 size 100000 type 2 Physical Memory Region from fee00000 size 100000 type 2 Physical Memory Region from ffb00000 size 500000 type 2 Physical memory region not addressable Physical memory region not addressable Multiboot gave us no video information ACPI: RSDP paddr=0xfec00 ACPI: RSDP vaddr=0xdfcfec00 ACPI: RSDT paddr=0xfc790 ACPI: RSDT vaddr=0xdfcfc790 ***WARNING*** SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com) consider enabling Kernel loaded to: start=0x100000 end=0x13a000 size=0x3a000 entry=0x100076 ACPI: RSDT paddr=0xfc790 ACPI: RSDT vaddr=0xdfcfc790 ACPI: FADT paddr=0xfc85c ACPI: FADT vaddr=0xdfcfc85c ACPI: FADT flags=0xa5 ACPI: DMAR paddr=0xfcdde ACPI: DMAR vaddr=0xdfcfcdde ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: 1 IOMMUs detected ACPI: MADT paddr=0xfc9c4 ACPI: MADT vaddr=0xdfcfc9c4 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x2 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x4 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x6 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x1 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x3 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x5 ACPI: Not recording this APIC, only support 1 ACPI: MADT_APIC apic_id=0x7 ACPI: Not recording this APIC, only support 1 ACPI: MADT_IOAPIC ioapic_id=8 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 1 CPU(s) detected ELF-loading userland images from boot modules: BOOT MODULE: 0x1d6000: 0x0 0x1d6010: 0x0 0x1d6020: 0x0 0x1d6030: 0x0 0x1d6040: 0x0 0x1d6050: 0x0 0x1d6060: 0x0 0x1d6070: 0x0 0x1d6080: 0x0 0x1d6090: 0x0 0x1d60a0: 0x0 Boot module does not contain a valid ELF image seL4 called fail at /host/sel4test/kernel/src/arch/x86/kernel/boot_sys.c:813 in function boot_sys, saying "boot_sys failed for some reason :(" halting... Kernel entry via Interrupt, irq 0 Thanks, Alex

3 4

Camkes x86 VM Build Error
by Amit Goyal 30 Oct '18

30 Oct '18

Hi, I am using Ubuntu 16.04 on 64 Bit, i7 machine and running the CAmkES x86 VM instructions available at: https://docs.sel4.systems/CAmkESVM After running: ../init-build.sh -DCAMKES_VM_APP=minimal I am getting the following error: -------------------------------------------------------------------------------------------------------------------------------- camkes-gen.cmake is out of date. Regenerating... CMake Error at tools/camkes/camkes.cmake:593 (message): Failed to generate camkes-gen.cmake: Traceback (most recent call last): File "/usr/lib/python2.7/runpy.py", line 174, in _run_module_as_main "__main__", fname, loader, pkg_name) File "/usr/lib/python2.7/runpy.py", line 72, in _run_code exec code in run_globals File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 678, in <module> sys.exit(main(sys.argv, sys.stdout, sys.stderr)) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 515, in main instantiate_misc_templates(renderoptions) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py", line 509, in instantiate_misc_templates outfile_name=outfile.name, imported=read, options=renderoptions) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Renderer.py", line 109, in render self.templates, **kwargs) File "/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Context.py", line 261, in new_context }.items()) + list(kwargs.items())) AttributeError: type object 'ObjectType' has no attribute '__members__' Call Stack (most recent call first): CMakeLists.txt:35 (GenerateCAmkESRootserver) -- Configuring incomplete, errors occurred! See also "/home/goyal/sel4/camkes_vm/build_vm/CMakeFiles/CMakeOutput.log". ------------------------------------------------------------------------------------------------------------------------------- I also tried to run the same instructions on a different machine (Ubuntu 16.04, 64 Bit, i5 machine) on which ../init-build.sh -DCAMKES_VM_APP=minimal is run successfully. It gets stuck on running ninja. I am getting the following error: -------------------------------------------------------------------------------------------------------------------------------- ghc-8.0.2: 106.97 MiB / 107.55 MiB ( 99.47%) downloaded... ghc-8.0.2: 107.24 MiB / 107.55 MiB ( 99.71%) downloaded... ghc-8.0.2: 107.50 MiB / 107.55 MiB ( 99.96%) downloaded... ghc-8.0.2: 107.55 MiB / 107.55 MiB (100.00%) downloaded... /home/akshat/.stack/programs/x86_64-linux/ghc-8.0.2.tar.xz.tmp: renameFile:renamePath:rename: does not exist (No such file or directory) Makefile:45: recipe for target 'parse-capDL' failed make: *** [parse-capDL] Error 1 ninja: build stopped: subcommand failed. -------------------------------------------------------------------------------------------------------------------------------- Can someone suggest a way out for both the problems. -- Thanks and Regards, Amit Goyal

2 3

can not build tutorials anymore
by Thad Seeberger 30 Oct '18

30 Oct '18

good day. I can no longer build tutorials. These used to build a month ago. My system hasn't changed and I can still build the older ones with no issues. I get lost trying to debug this cmake/python stuff. ./init --verbose --plat pc99 --tut hello-camkes-1 INFO:sh.command:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>: starting process DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: started process INFO:sh.command:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..', pid 17525>: process started DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: acquiring wait lock to wait for completion DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: got wait lock DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525 ['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G', 'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64', '-DTUTORIAL_DIR=hello-camkes-1', '..']>: exit code not set, waiting on pid -- The C compiler identification is GNU 7.3.1 -- The CXX compiler identification is GNU 7.3.1 -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc -- works -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/g++ -- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/g++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- The ASM compiler identification is GNU -- Found assembler: /opt/rh/devtoolset-7/root/usr/bin/gcc CMake Error at projects/sel4-tutorials/cmake/helpers.cmake:141 (message): Failed to render: PYTHONPATH=/home/john/sel4/projects/camkes/capdl/python-capdl-tool;python;/home/john/sel4/projects/sel4-tutorials/template.py;--tut-file;/home/john/sel4/projects/sel4-tutorials/tutorials/hello-camkes-1/hello-camkes-1;--out-dir;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/gen;--input-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/input_files;--output-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/output_files;--arch;x86_64;;;, Traceback (most recent call last): File "/home/john/sel4/projects/sel4-tutorials/template.py", line 154, in <module> sys.exit(main()) File "/home/john/sel4/projects/sel4-tutorials/template.py", line 142, in main render_file(args, env, state, file) File "/home/john/sel4/projects/sel4-tutorials/template.py", line 90, in render_file out_stream.write(template.render(context.get_context(args, state))) File "/home/john/sel4/projects/sel4-tutorials/tools/context.py", line 435, in get_context context.update(ObjectType.__members__.items()) AttributeError: type object 'ObjectType' has no attribute '__members__' Call Stack (most recent call first): projects/sel4-tutorials/cmake/helpers.cmake:164 (ExecuteGenerationProcess) projects/sel4-tutorials/CMakeLists.txt:29 (GenerateTutorial) -- Configuring incomplete, errors occurred! See also "/home/john/sel4/hello-camkes-1_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 91, in <module> File "./init", line 81, in main File "/home/john/sel4/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/john/sel4/projects/sel4-tutorials/common.py", line 69, in _init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output, _err=output) File "/sandbox/lib/python2.7/site-packages/sh.py", line 1427, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/sandbox/lib/python2.7/site-packages/sh.py", line 774, in __init__ self.wait() File "/sandbox/lib/python2.7/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/sandbox/lib/python2.7/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 .. STDOUT: STDERR:

2 2

camkes-arm-vmm run multiple VMs at once
by Daniel Wang 25 Oct '18

25 Oct '18

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

3 2

Kernel Exception in seL4 Tutorial
by Jeremiah Peschka 24 Oct '18

24 Oct '18

I’m attempting to build the seL4 tutorials on a local VM (Ubuntu 18.04 "Linux ubuntu 4.15.0-36-generic #39-Ubuntu SMP Mon Sep 24 16:19:09 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux”). I have confirmed that the VM has the pre-reqs present and the repository was synced using repo this afternoon. The builds succeed, but running the VM produces a kernel exception. Here is sample output from attempting to build the dynamic-1 tutorial: https://pastebin.com/NnShcREU A similar error occurs when I build the completed solution, as well. Using GDB, it appears that main is never reached. Thanks for any assistance, Jeremiah Peschka

2 6

seL4 IPC SMP
by 송대영 24 Oct '18

24 Oct '18

HI, I have question about IPC on SMP. I ran sel4bench on sabre lite(i.mx6, arm v7) which SMP is on. Sabre lite has 4 cores. I supposed that SMP improved IPC performances. But results were not. seL4_CALL SMP on 504 SMP off 336 Would you give me reason why these results are happened?

2 2

Camkes VM Linux tutorial
by hedi delpazir 23 Oct '18

23 Oct '18

Hi, After running ./init --plat pc99 --tut camkes-vm-linux(following https://docs.sel4.systems/Tutorials/camkes-vm-linux.html) following error will occurred: -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/gcc CMake Error at projects/camkes/vm/camkes_vm_helpers.cmake:21 (ApplyCommonReleaseVerificationSettings): ApplyCommonReleaseVerificationSettings Function invoked with incorrect arguments for function named: ApplyCommonReleaseVerificationSettings Call Stack (most recent call first): camkes-vm-linux/CMakeLists.txt:10 (include) -- camkes-gen.cmake is out of date. Regenerating... -- Configuring incomplete, errors occurred! See also "/home/hedi/sel4-tutorials-manifest/camkes-vm-linux_build/CMakeFiles/CMakeOutput.log". Traceback (most recent call last): File "./init", line 91, in File "./init", line 81, in main File "/home/hedi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 107, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/home/hedi/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 69, in _init_build_directory result = sh.cmake(args + ['..'], _cwd = directory, _out=output, _err=output) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 1427, in *call* return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 774, in *init* self.wait() File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 792, in wait self.handle_command_exit_code(exit_code) File "/home/hedi/.local/lib/python2.7/site-packages/sh.py", line 815, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=camkes-vm-linux .. STDOUT: STDERR: Any Idea?

2 1

CAmkES-VM Stalling
by Chris Guikema 23 Oct '18

23 Oct '18

Hello, I am seeing a weird issue with the CAmkES-VM. Just last week, I was able to run the VM successfully using the "minimal" version. I followed these steps: $ repo init -u https://github.com/seL4/camkes-vm-examples-manifest.git $ repo sync $ mkdir test && cd test $ ../init-build.sh -DCAMKES_VM_APP=minimal $ ninja Everything compiles correctly. I then had to use ccmake .. to switch the FPU save method to FXSAVE before recompiling. My QEMU command is: $ qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 1 -cpu Nehalem,+vmx -nographic My QEMU version is: $ qemu-system-x86_64 --version QEMU emulator version 2.5.0 (Debian 1:2.5+dfsg-5ubuntu10.32), Copyright (c) 2003-2008 Fabrice Bellard And I'm running on Ubuntu 16.04. I get as far as: [ 1.930000] clocksource: Switched to clocksource pit [ 2.274669] VFS: Disk quotas dquot_6.6.0 [ 2.324891] VFS: Dquot-cache hash table entries: 1024 (order 0, 4096 bytes) [ 2.463451] hugetlbfs: disabling because there are no supported hugepage sizes [ 2.562973] random: fast init done After that, everything just runs extraordinarily slowly, or ends up stalling out completely. This is a change from a couple weeks previously, were I could get to the login prompt within ~10s using the minimal VM configuration. Has anything changed in the past few weeks that would have caused this? Thanks, Chris

2 1

MCS tutorial
by hedi delpazir 23 Oct '18

23 Oct '18

Hi, After running ninja in build directory(following https://docs.sel4.systems/Tutorials/mcs.html) following error will occurred: [15 of 16] Compiling CapDL.Parser ( CapDL/Parser.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/CapDL/Parser.o ) [16 of 16] Compiling Main ( Main.hs, .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL-tmp/Main.o ) Linking .stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/parse-capDL/parse-capDL ... capDL-tool-1.0.0.1: copy/register Installing executable(s) in /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin stack install Copying from /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/.stack-work/install/x86_64-linux/lts-9.21/8.0.2/bin/parse-capDL to /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build/parse-capDL Copied executables to /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build: - parse-capDL Warning: Installation path /home/hedi/sel4-tutorials-default/ipc_build/ipc/parse_capdl_tool-prefix/src/parse_capdl_tool-build not found on the PATH environment variable. ninja: build stopped: subcommand failed. Any idea?

2 1

FOSDEM 2019 - Microkernels developer room - CfP
by Alexander Boettcher 12 Oct '18

12 Oct '18

FYI -------- Forwarded Message -------- Subject: FOSDEM 2019 - Microkernels developer room - CfP Date: Thu, 11 Oct 2018 11:48:24 +0200 From: Sebastian Sumpf <Sebastian.Sumpf(a)genode-labs.com> Reply-To: Genode users mailing list <users(a)lists.genode.org> To: users(a)lists.genode.org FOSDEM 2019 - Microkernels and Component-based OSes devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2019 [1] in Brussels, Belgium and will share a developer room on Sunday February 03, 2019 [2]. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-, unikernel-, and componenent-based operating systems. Possible topics include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * enabling support for hardware (architectures, device drivers) * used languages and tools * maintenance and testing * security and robustness * trends and challenges * use cases, experiences, lessons learned and demos Please use the Pentabarf [3] system to submit your proposals. You do not need to create a new account if you already have one. When in doubt, please use the devroom mailing list [4]. If you do not want to give a talk yourself, you may still send suggestions for what else you would like to see, or do in the devroom. Please send your suggestions to the mailing list. The deadline for your proposal is on December the 1st 2018. Make sure to include the following in your proposal: * title of your talk (will be printed in the FOSDEM booklet) * your full name (will be printed in the FOSDEM booklet) * a short abstract (one or two paragraphs) * duration of your talk (please, at least 25 and no longer than 55 min) The official devroom schedule (along with the accepted talks) will be announced on December the 15th on the devroom's mailing list and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. About FOSDEM FOSDEM is a two-day event organised by volunteers to promote the widespread use of free and open source software. Taking place in the beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the best such conference in Europe. FOSDEM covers a wide spectrum of free and open source software projects, and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) with network/internet connectivity and projectors where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and discussions. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, certification exams and project stands. Every year, FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. Participation and attendance is totally free, though the organisers gratefully accept donations and sponsorship. No registration necessary. About the devroom Since the first Microkernel devroom in 2012 this devroom has been part of each following FOSDEM. By now it has become a somewhat institutionalized tradition for the micro kernel community to meet there; to this date over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the Microkernel devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Social events It also has become a habit that the microkernel projects dine together somewhere in Brussels. The year 2019 will not be any different, so there is going to be a microkernel family dinner on Saturday night. We try place a reservation, so we will inform you about the exact location and time later. Consult the FOSDEM web and other projects for additional social events such as the famous FOSDEM-organized Friday Beer Event and the FOSDEM-arranged free sightseeing tours for spouses. Important dates recap * 01.12.2018: Deadline for submissions * 15.12.2018: Schedule published and speakers notified of acceptance * 03.02.2019: The devroom takes places Links [1] http://fosdem.org [2] https://fosdem.org/2019/practical/transportation [3] https://penta.fosdem.org/submission/FOSDEM19 [4] https://lists.fosdem.org/listinfo/microkernel-devroom See you all at FOSDEM! _______________________________________________ Genode users mailing list users(a)lists.genode.org https://lists.genode.org/listinfo/users

1 0

Reverse back to Original TK1-SOM U-boot
by Daniel Wang 12 Oct '18

12 Oct '18

Hi all, I’m using a TK1-SOM board. Following the document (https://docs.sel4.systems/Hardware/CEI_TK1_SOM/#u-boot <https://docs.sel4.systems/Hardware/CEI_TK1_SOM/#u-boot>) I flashed the U-boot to enable booting HYP mode. How do I reverse back to the original U-boot so that I can boot the original on board Linux? Thank you! Best Regards -Daniel Wang

2 5

US Army SBIR calls for open HW/SW stack
by Gernot.Heiser＠data61.csiro.au 09 Oct '18

09 Oct '18

… and mentions seL4 prominently: https://www.sbir.gov/sbirsearch/detail/1508741

1 0

seL4 IPC fastpath question
by 송대영 08 Oct '18

08 Oct '18

Hello, I have question about seL4 IPC fastpath. I ran sel4bench on sabre lite(arm v7). 1. IPC fastpath can apply in seL4_Call and seL4_Reply_Recv, is it right? seL4_Send, seL4_Recv can't apply IPC fastpath. 2. IPC_fastpath can only send message that message's length is 0, is it right? I found these comments. /* Call slowpath, long IPC (10), same prio client to server, different address space */ /* ReplyRecv slowpath, long IPC (10), same prio server to client, on the slowpath, different address space */ 3. In seL4 IPC mechanism, IPC only use registers not memory?

3 2