- Devel - lists.sel4.systems

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