- Devel - lists.sel4.systems

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

RISC-V - sel4test and sel4bench running on SiFive's Unleashed Platform
by Hesham Almatary 18 Jul '18

18 Jul '18

Hi everyone, I pushed my local seL4/RISC-V work to GitHub which contains the following new features: * A new option to run seL4 in machine mode. * A port of seL4 to QEMU's SiFiveU and virt platforms. * DTB parsing in seL4 to read and use UARTs when available. * Ported seL4 to run on VC707 FPGA Freedom Unleashed platform. * Initial Benchmarking support in seL4. * Initial sel4bench port that can measure IPC and trap timing. Link for more details: http://heshamelmatary.blogspot.com/2018/07/new-sel4test-and-sel4bench-relea… -- Hesham

1 0

Porting sel4 on RISCV architecture
by Sathya Narayanan N 16 Jul '18

16 Jul '18

Hi Experts, This is Sathya from IIT Madras. We are working on porting SEL4 on RISCV architecture running on FPGA. We have ported linux on the FPGA. I have some doubts regarding OS porting. I am stuck at the end. Before my actual query, let me tell my platform. Hardware - 64 bit RISCV design running on FPGA. It doesn't support compressed instn and multiarch. Operating system - SEL4, repo synced from latest official repository. Tools - Latest synched from RISCV official repo. Query - I simulated sel4test on spike and then I am trying to port it on FPGA. We have UART to be mapped to 0x11400 address location. I set scan->reg to this value. I understood, incase of simulation, the DTB argument passed to init_first_hart function comes from spike simulator (file - sim.cc). Now, for FPGA I want to pass the DTB value to the init_first_hart() function. I am planning to write a DTS file and somehow read the data from DTS file here. I am trying to know, what is the right method to do for SEL4 ? Can you please let me understand, how you went ahead for SEL4 ? Is there any changes, I have to do in the repo code ? any readings would you suggest to proceed ahead ? -- regards, Sathya

3 4

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 13 Jul '18

13 Jul '18

Thanks again for the reply. I was looking for the foolproof way to write safe C code, but seems like the best way to go forward is to carefully design and code. Your advice is helpful to me. On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > >> Clang does have a static analyzer builtin that can be help in some > cases. That being said, the best way forward is for you as a developer to > understand the types of code that can lead to problems and not rely > entirely on a static analyzer. > > >>> >>> >

1 0

Re: [seL4] How to write safe C code for free?
by Wean Irdeh 13 Jul '18

13 Jul '18

Thanks a lot for the reply. What is your opinion on static checking tool and safe subset of C? Does that help? On Friday, July 13, 2018, Dean Pucsek <dean(a)lightbulbone.com> wrote: > Hello Wean, > > It is certainly possible to learn how to program in C without spending any > money; all it requires is a basic toolchain and a willingness to learn. > don't sell yourself short by hinting that you might be "stupid" (you almost > certainly aren't). > > In order to get started with C I suggest setting up an environment to > experiment in; for that look into installing LLVM/Clang ( > http://releases.llvm.org/) there are pre-built binaries for most major > operating systems. Once that is done all you need is a text editor (Notepad > on Windows or one of the other many free options) and some patience. As for > tutorials and resources, some options are: > > - Searching on Google for "c tutorial"; one result that looks interesting > is http://www.learn-c.org/. > - Finding an open source project that interests you and trying to > understand the code then implement a change. > - While not free, may people swear by the K&R book as a great resource to > start. > > In terms of writing code that is free of undefined behaviour and > vulnerabilities your best bet is to learn what code constructs cause those > to occur and how to avoid them. A great book for this is The Art of > Software Security Assessment by Mark Dowd, there is a PDF of Chapter 6 (C > Language Issues) available at https://trailofbits.github.io/ > ctf/vulnerabilities/references/Dowd_ch06.pdf. > > Learning about C, undefined behaviour, and vulnerabilities doesn't happen > overnight so be patient and enjoy the journey. > > --Dean > > > >

1 0

Help ! Simulating SEL4 with Zero testcases running
by Sathya Narayanan N 13 Jul '18

13 Jul '18

Hi Experts, I am running sel4 simulation on spike. I want to disable test cases from running. I tried setting default value "" from ".*" in Kconfig file. Is this enough ? Or is something else to be done ? -- regards, Sathya

2 2

Re: [seL4] sel4test cross compiling for arm
by Kofidoku.Atuah＠data61.csiro.au 13 Jul '18

13 Jul '18

?Hey Thad, Thanks for catching that: it turns out that we weren't passing -nostdlib to the linker when linking the ELFLoader, so the cross-toolchain's linker was trying to link the ELFLoader against the cross toolchain's libc, but it shouldn't be doing that and it should instead be using our libmuslc. A fix has been pushed out and you should be seeing it shortly. Thanks for your patience, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

1 0

seL4 vm examples with Qemu
by Mike Clark 12 Jul '18

12 Jul '18

Is it currently possible to boot the camkes-vm-example applications using qemu? I followed the directions here (https://github.com/seL4/camkes-vm-examples) to get a build of the minimal application. I then tried to follow the directions here ( https://docs.sel4.systems/Hardware/Qemu/#running-qemu) to boot using qemu. Unfortunately I get an error when trying to boot. The error says: *"seL4 caled fail at /host/camkes_vm/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :("* *halting...* *Kernel entry via Interrupt, irq 0* I'm running this on a ubuntu 16.04 machine with an Intel i5-4200U ( https://ark.intel.com/products/75459/Intel-Core-i5-4200U-Processor-3M-Cache… ). Thanks!

2 1