- Devel - lists.sel4.systems

How to write safe C code for free?
by Wean Irdeh 05 Aug '18

05 Aug '18

Hello. I'm a poor person looking for an advice. I know this is the right place since all of you have huge expertise in formal verification. I'm not a smart person (maybe I'm stupid), but I'm interested in open source contribution using C language. Is there any solution to write C code free from undefined behavior and vulnerability without paying for any tools?

3 2

using libmuslc library question
by Leonid Meyerovich 03 Aug '18

03 Aug '18

Hello, I have tried to call usleep() function from seL4 'main' thread and it crashes the system with error: Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on code at address 0x200 with status 0x82000006 in thread 0xff807bfe2200 "rootserver" at address 0x200 With stack: How to use this library? Thank you, Leonid

1 0

about compile error
by wong xuguo 03 Aug '18

03 Aug '18

Dear Sir/Lady, This is a student from china, I am very interested in the sel4, works on the camkes, When I first compile the project camkes, I met a problem: camkes.c:502: undefined reference to `component_control_main' I know this means it not implemented this function, but this function seems produced by a auto method, so could you tell how to solve this problem? I follow the command: https://docs.sel4.systems/CAmkES/ to compile the : repo init -u https://github.com/seL4/camkes-manifest.git

2 1

Question on multi-partition seL4 image/load for x86
by Jim Marek 02 Aug '18

02 Aug '18

seL4 Developers/SMEs: Does anyone have a seL4 load/configuration that includes more than 2 partitions with at least 2 of the partitions each having a dedicated Ethernet interface assigned to it? I am focused on an x86 host platform. Currently I have a Dell 7910 19" rack unit I am wanting to host on and it has 4 Ethernet ports. Thanks, Jim Marek Enterprise Architect Rockwell Collins

2 3

Question about wrapper files
by Holm, Elinor M 30 Jul '18

30 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are there for testing, or something else? Elinor Holm Software Engineer 781-410-5221 This message and/or attachments may include information subject to GDC4S S.P. 1.8.6 and GD Corporate Policy 07-105 and are intended to be accessed only by authorized recipients. Use, storage and transmission are governed by General Dynamics and its policies. Contractual restrictions apply to third parties. Recipients should refer to the policies or contract to determine proper handling. Unauthorized review, use, disclosure or distribution is prohibited. If you are not an intended recipient, please contact the sender and destroy all copies of the original message.

3 2

CAmkES 3.5.0 Build Error
by Amit Goyal 28 Jul '18

28 Jul '18

Hi, I am running CAmkES 3.5.0 on Ubuntu 16.04, 64 Bit, i5 machine, CMake 3.11.4. I am getting the following error on running ../init --plat pc99 --tut hello-camkes-1 --solution (although seL4 10.0.0 works perfectly fine). ------------------------------------------------------------------------------------------------------------------------------- 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/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/projects/sel4-tutorials/common.py", line 58, 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-1 -DBUILD_SOLUTIONS=TRUE .. STDOUT: -- The C compiler identification is GNU 5.3.1 -- The CXX compiler identification is GNU 5.3.1 -- 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 -- 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 -- Performing test HARD_FLOAT with flags -mfloat-abi=hard -- Test HARD_FLOAT FA... (295 more, please see e.stdout) 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 tools/camkes/camkes.cmake:581 (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/akshat/Desktop/sel4_10.0/try/camkes-tutorials-manifest/tools/camkes/camkes/runner/__main__.py", lin... (614 more, please see e.stderr) -------------------------------------------------------------------------------------------------------------------------------- Can you please suggest a way around? -- Thanks and Regards, Amit Goyal

2 2

Question about wrapper files
by Holm, Elinor M 27 Jul '18

27 Jul '18

I built sel4test using the init-build.sh command with -DPLATFORM=x86_64 and -DSIMULATION=TRUE and then ran ninja. I'm using QEMU as my emulator. Within the build directory I created, there's a kernel directory. In that directory, there are a bunch of C files with names that include "wrapper." For instance, there's a file named kernel_all_pp_prune_wrapper_temp.c. I'm having trouble understanding what the wrapper files do. Are they for testing, or something else? Elinor Holm

1 0

Image lies outside of usable physical memory v2
by Jeremy Fields 26 Jul '18

26 Jul '18

http://sel4.systems/pipermail/devel/2016-July/000918.html I'm running into the same issue, with likely the same cause. I wanted to see if there is any further insight that can be given on this? I'm guessing there hasn't been any updates to seL4's memory allocation in this aspect. (I'm using seL4 9.0.1) My naive attempt of commenting out that particular check in seL4 just results in the machine hard resetting when it runs (if only it were that easy). >Unfortunately I cannot say that we will get around to fixing this in a particularly timely manner. (2016) Any chance this is on a roadmap? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

2 1

Implementing a Filesystem on CAmkES
by Grant Jurgensen 25 Jul '18

25 Jul '18

Hello all, I was hoping to get some advice on how to implement a filesystem on my CAmkES project. For now I'm targeting FAT32, but that is flexible. So far, my plan is to port the libsdhcdriver to my platform (which shouldn't be too bad. I'm targeting exynos5, and I see exynos4 is already supported). After that, I assume I'm on my own when it comes to creating a filesystem interface. Perhaps there is an existing library for this that can hook into any standard SD controller implementation? Finally, is there an easy way to integrate said filesystem into musllibc such that one could use the standard open/read/write/close functions? Does this sound like the best way to go, or am I missing a simpler solution? Thanks, Grant

3 2

Re: [seL4] Understanding how SEL4 recognises UART on board
by Sathya Narayanan N 19 Jul '18

19 Jul '18

Hi Experts, I am curious to know how SEL4 recognises the existence of UART on the board and mapped to a particular memory address. I see there is no DTB/ DTS files read from memory. could someone help me understand the concept here ? Or is it something hardcoded in the kernel ? -- regards, Sathya

2 1