Devel December 2015

devel@sel4.systems

22 participants
18 discussions

Timing side channel via idle thread code?
by Brian Mastenbrook 12 Dec '15

12 Dec '15

While pulling up the Haskell model to respond to the previous question, I noted the following statement: "The idle thread's code is at an arbitrary location in kernel memory. For convenience in the Haskell model, we place it in the globals frame, but there is no need for it to be in user-accessible memory." Given that the globals frame is mapped cacheable, doesn't this lead to a potential timing side channel? Tasks would be able to determine whether the idle thread's code has been evicted from cache, which may or may not reveal something interesting about the state of the system as a whole. -- Brian Mastenbrook CTO Wearable Inc. Makers of AirStash

3 2

vspace_reserve_range_at
by Robert VanVossen 12 Dec '15

12 Dec '15

Hello, I am trying to map a device 1:1 in my root thread. When I try to reserve a range at the specific location, using the vspace_reserve_range_at() function I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000. Is there something that the kernel or the root task needs to do before this to make this range available for reservation? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

2 1

vspace_reserve_range_at
by Robert VanVossen 12 Dec '15

12 Dec '15

Hello, I am trying to create a 1:1 physical to virtual mapping in my root thread. My first step in attempting this is to reserve the virtual address I need using the vspace_reserve_range_at() function, but I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000 Is there something I need to do in the kernel or in the root thread to actually allow this memory to be reserved? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

1 0

verifying concurrency
by Gergely Buday 09 Dec '15

09 Dec '15

Hi there, what should I read if I want to understand the verification of concurrent programs related to the sel4 project? I have found https://ssrg.nicta.com.au/publications/papers/Daum-phd.pdf https://ssrg.nicta.com.au/publications/papers/Daum_DSW_08.pdf http://ssrg.nicta.com.au/projects/concurrency/ Are there others? Cheers - Gergely

3 2

Reminder: Microkernel-devroom CfP deadline is on this Sunday
by Jakub Jermar 07 Dec '15

07 Dec '15

Hi folks, the CfP deadline for the Microkernel devroom at FOSDEM 2016 is due this Sunday. See the original CfP [1] for information on what to do if you would like to give a talk about some microkernel-related topic. At the same time, I would like to encourage you to submit a talk proposal. It would be shame not to let the wider microkernel community know about the latest and greatest developments in your project. Lastly, please forward this reminder to whoever you think may want to give a talk in the devroom and is not among the recipients of this message. Thanks, Jakub [1] http://trac.helenos.org/wiki/Devroom2016

1 0

haskell on sel4
by Tim Newsham 05 Dec '15

05 Dec '15

I just noticed the web page says "we have Haskell sort-of running on seL4 (thanks or friends from Galois for their help), should be released in the near future" This is great news. Are you able to share any details such as when any of this will be public, what the porting strategy was (is this similar to HalVM?), what dependencies haskell compiled code requires, if there are sel4 bindings, etc? Tim

3 4

Initial Thread physical to Virtual Mapping
by Robert VanVossen 04 Dec '15

04 Dec '15

Hello, I am attempting to integrate the Xilinx drivers, provided through their SDK, with seL4 on the Zynq7000. In the root thread, I created a virtual mapping for the SD Card peripheral, and I pass that virtual address into the driver, so that it is reading and writing to it. The controller has a built-in DMA that gets used for data transfer. I created a buffer in the root thread's virtual space to pass to the DMA, but it needs a physical address. I calculated the virtual/physical offset from the physical and virtual addresses for the application that are given by the elfloader, but that didn't seem to be the correct mapping. Is there a good way to get that mapping, either from within the application itself or from the kernel before hand? Thanks, Robbie VanVossen DornerWorks

3 2

Assigning GPIO buffer to a new process
by Karl Apsite 02 Dec '15

02 Dec '15

Ahoy there! I'm working on a Zynq 7000 - ZC702 dev board. I've setup a capability associated with the GPIO buffer, and have successfully ran a small test in the root process that could read a button's state via GPIO. The next step is to send the capability to a second process so that it can read the button's state. I'm having some trouble understanding how I should go about using the IPC calls to achieve this transfer. I'll try to give a summary of my efforts, to clear up where I am, and what I've done so far. To start: I borrowed (heavily) from the 4th tutorial that established two separate processes Main: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… App: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… I felt inclined to inform the second process about the whereabouts of the new endpoint as opposed to making an assumption as to where it was allocated. I crammed the address into the argc/argv constructs as the process starts, and it seems to be able to continue just fine. 1. Is that an OK thing to do? I understand that I shouldn't be too willing to share vital information freely between both processes, and I'm not sure if abusing argc/argv to inform the second process is appropriate here. I left the main thread in seL4_Wait(). My idea is: other processes are expected to send a message representing a command that main can respond to. Main can check the message, badge(s), and privileges as necessary, and respond with the capability if it so desires. With the capability in hand, and a tag with extracaps set to one, I was NOT able to successfully send the cap. The second process would only receive a tag with extra caps set to zero, so it must be failing somewhere along the way. I loaded the cap into the first slot using seL4_SetCap(0, my_cap) and the cap was functioning previously, so I doubt it's erroring when I send. I expect an error on the receiving end somewhere. I have NOT been able to prepare a path for a capability in the second process, and notify seL4 of the location using seL4_GetCapReceivePath(root_node, new_cap, 32). 2. How should the second process obtain a reference to its root cnode? 3. How should the second process allocate a new cnode? I think the new_process_t structure in the main process has the addresses I'm after (to obtain the root cnode at least, and maybe allow me to a new cnode?), but I don't understand the implications of informing the second process about the information in the new_process_t structure. 4. Is the new process expected to know all of that information? 5. Is there an API to establish this sort of information (along with the IPC endpoint that I had to cram into argc/argv earlier?)

2 1

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel December 2015