- Devel - lists.sel4.systems

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