- Devel - lists.sel4.systems

Userspace Debugging for ia32
by ALVI Aslam (MORPHO) 23 Jan '18

23 Jan '18

Hello Team, I need some help to start a userspace debugging for ia32. Since as per the instruction mention in the link https://wiki.sel4.systems/Debugging%20guide I was able to use GDB for kzm based defconig. But how can I start userspace debugging for ia32 based defconig? Thank You & Regards, Aslam

2 1

seL4 vs. Integrity-178B
by Baconicsynergy 22 Jan '18

22 Jan '18

Hello friends :) First off, congratulations on being the new primary microkernel of choice for the Genode Operating System Framework! I'm very excited. Now to my questions - how does the formal verification of seL4 compare with the Integrity-178B security guarantees? Also, how do two structurally compare with each other in terms of design principles and implementation? Best regards, Joel Desermeau seL4

2 1

seL4 8.0.0 and CAmkES camkes-3.2.0 release
by Kent.Mcleod＠data61.csiro.au 18 Jan '18

18 Jan '18

seL4 8.0.0 and CAmkES camkes-3.2.0 release = seL4 8.0.0 = Note: Meltdown and Spectre patches are not included in this release and will be included in a forthcoming release once they have been verified. Once they are merged they will still be accessible through the master branch of seL4 on github. Release notes: https://wiki.sel4.systems/seL4%208.0.0 CHANGES file in https://github.com/seL4/seL4/tree/8.0.0 = CAmkES camkes-3.2.0 = Release notes: https://wiki.sel4.systems/camkes-3.2.0 CHANGES file in https://github.com/seL4/camkes-tool/tree/camkes-3.2.0 = Miscellaneous updates = == CMake build system == Replacing the current kbuild build system with a new CMake build system is still in progress. The kernel only CMake build is now used by l4v. Initial CMake versions for sel4test, sel4bench and our CAmkES projects are still being developed. We intend to do a release that contains the Kbuild and CMake scripts working side by side, and will then start to remove the Kbuild scripts after that. == Changes to manifests for our projects == Each project that we maintain now has a default.xml and master.xml manifest file. master.xml is used to specify the branch tips of the upstream git repositories that a project uses. default.xml now pins all of the repositories to revisions that last passed our regression tests. For this current release and future releases a release tag will be created on each manifest repo specifying the revision of default.xml that uses the released revisions of all the repositories. The seL4 and camkes-tool repos will still be tagged on each release, and all other repositories will have versioned branches created the same as before. We have only just finished testing this change and the various documentation will be updated over the coming days. == Meltdown and Spectre == As mentioned above, Meltdown and Spectre related patches are not present in this release and will be merged into the kernel once verification is complete. There will likely be a blog post accompanying their release. ?

1 0

Re: [seL4] x86 kernel address space side channels
by Jeroen "Slim" van Gelderen 05 Jan '18

05 Jan '18

Thanks for clarifying that. Do you have any information on whether AMD is wrong claiming that their architecture is not vulnerable? On Thu, Jan 4, 2018 at 11:29 AM, Alex Elsayed <eternaleye(a)gmail.com> wrote: > > On Jan 4, 2018 07:37, "Jeroen "Slim" van Gelderen" <askslim(a)gmail.com> > wrote: > > On Wed, Jan 3, 2018 at 4:37 PM, Alex Elsayed <eternaleye(a)gmail.com> wrote: > >> In addition, Intel has published a press release, claiming that this >> issue (counter to some claims elsewhere) does in fact affect other >> vendors and architectures: >> >> https://newsroom.intel.com/news/intel-responds-to-security-r >> esearch-findings/ > > > Contrary to the PR, Intel CPUs do indeed have a design flaw aka bug which > makes them vulnerable to Meltdown. Meltdown has not been reproduced on ARM > or AMD and AMD thinks Meltdown is not applicable to their chips due to > architectural differences. > > The Spectre attack is the attack that is applicable across the board. > > As far as Linux is concerned only Intel machines will be hit with the > KPI-related slowdown (5%-30%) since KPI will be disabled on AMD CPUs. (And > I assume this goes for Windows too.) This looks bad for Intel, hence the > FUD. > > > It's a bit more nuanced than that. First of all, section 6.4 of the > Meltdown paper is quite clear: non-Intel CPUs _do_ still perform the > problematic access; it's the particular covert channel they use to extract > the information from it that does not port over. Many expect this to > change; the authors themselves see that whether AMD or ARM are affected is > _unknown-_, not that they are unaffected. > > Second, the patch from AMD to disable KPTI has not been accepted AFAIK, > and AArch64 is adding KPTI. > > Third, Meltdown is a _less severe_ attack by far compared to Spectre. > Meltdown can be addressed by KPTI, but some forms of Spectre use little > besides the BTB, which is known[1] to be infeasible to flush in software. > > Fourth, Intel (and I) posted that link _prior_ to the release of the > papers, at a time when all that was known to the public was "very serious > vulnerability in speculative execution" - its claims should be read in that > context. > > [1]: https://arxiv.org/abs/1612.04474 > > > -- Jeroen "Slim" van Gelderen

1 0

x86 kernel address space side channels
by Corey Richardson 05 Jan '18

05 Jan '18

https://lwn.net/Articles/738975/ That's really painful, for Linux ;) I don't think seL4 is really impacted? I'm having a hard time thinking about what sensitive information could be disclosed by probing the kernel window. Maybe which memory regions caps being accessed by other concurrently running threads occupy? You could use that to make a covert channel, if the two threads trying to communicate are running in parallel. It seems really dubious that that could give you anything useful otherwise, and as the literature shows timing side channels are unavoidable on x86. Thought it was interesting and worth sharing! -- cmr http://octayn.net/ +16038524272

6 8

I/O and PCIE on TX1
by Jon Lamb 04 Jan '18

04 Jan '18

Hi seL4 Dev Team, I'm currently working on (mostly learning at this point) how we could add TX1 platform support for a PCIE network card (Intel 82580), using TK1 and others as a reference. I'm fairly new to working with PCI, but after looking around I think I have a general idea on what I need to do. I would appreciate it very much if someone with more experience could tell me if I'm on the wrong path here: * Using the TX1 TRM, I would populate the missing physical device region definitions in 'tx1/plat/machine/devices.h', and update the 'dev_p_regs[]' struct in 'tx1/plat/machine/hardware.h' * Figure out if I need to build up SMMU support (also a newbie here), I'm having doubts on whether I can bang on physical addresses or not without it * Construct a suitable implementation of 'ps_io_port_ops_t' for handling the I/O routines for libpci * Put together a hello world main program to exercise some of libpci's functionality * Once things are looking good there, move up to libethdrivers and port the needed bits for our Ethernet adapter using existing references (and eventually hooking up to lwip hopefully) At this point, I've been avoiding camkes for the sake of learning how everything works and if anyone can recommend a good starting C project for doing I/O on an ARM platform, that would be very helpful. Thanks in advance. -- Jon Lamb Software Engineer | *PolySync* 1020 SE 11th Ave, Portland, OR 97214 *c* 888.810.4284 x701 <888.810.4284%C2%A0x713> | *e* jlamb(a)polysync.io | *w* polysync.io <http://www.polysync.io/>

2 2

iMX6 dvfs registers
by Zippy Maniac 02 Jan '18

02 Jan '18

Hi, Sorry for pestering (again). I am trying to access the DVFS registers from a seL4 component and they seem to be read only. I can read/write them from UBoot and the kernel. So my guess is the registers require privilege even though I have yet to find a definitive statement to this effect in the ARM / NXP documentation. So the question is. Is it possible to give a component the necessary access rights to the DVFS registers via camkes? Or is there some other sort of workaround I could employ to gain access? Cheers, Zippy

2 1

Dynamic Loading of application
by PANCHAL Vishalkumar (MORPHO) 18 Dec '17

18 Dec '17

Hello, Can we use ELF-Loader tool functions into the user_space application (here, main_app) to Dynamically load the image of other application (app-1, app-2, app-3) from external device ? [cid:image008.png@01D374F1.2B37E4A0] Regards, Vishal PANCHAL Software Engineer | Noida | R&D P : +91 (120) 4072 549 M. +91 94266 38316 E. vishalkumar.panchal(a)morpho.com<mailto:vishalkumar.panchal@morpho.com> [Idemia]<https://www.idemia.com/> Join us on [Facebook]<https://www.facebook.com/IdemiaGroup/> [Twitter]<https://twitter.com/IdemiaGroup> [LinkedIn]<https://www.linkedin.com/company-beta/3488/> [Youtube]<https://www.youtube.com/user/SafranMorpho/> [www.idemia.com]<https://www.idemia.com/> [OT-MORPHO is now IDEMIA] # " This e-mail and any attached documents may contain confidential or proprietary information. If you are not the intended recipient, you are notified that any dissemination, copying of this e-mail and any attachments thereto or use of their contents by any means whatsoever is strictly prohibited. If you have received this e-mail in error, please advise the sender immediately and delete this e-mail and all attached documents from your computer system." #

2 1

Questions concerning the capability management system
by Timotej Tomandl 18 Dec '17

18 Dec '17

Hi, while reading about seL4 I have found a presentation "The seL4 capability system" by Matthew P. Grosvenor (https://www.cl.cam.ac.uk/resea rch/security/ctsrd/cheri/workshops/pdfs/20160423-sel4-capabilities.pdf), sadly I was able to track down only the slides, not the talk itself. It mentions the "Aurora project", the constraint solver running in static memory + stack space, concerning itself with the capability allocation. There are these questions which popped into my mind: 1. Is the source code of the Aurora project available anywhere? Is there any more information than the presentation available? 2. Is the constraint solver still necessary with the current version of the API? 3. If it is still necessary, then - what is the necessary strength of the constraint solver? - is a design, in which either the root process or the microkernel itself has to include such a constraint solver in static memory + stack space necessary for a microkernel with the guarantees of seL4 or is it a side-effect of the design decisions? Regards, Timotej Tomandl

2 1

Questions about Tx1 Physical Memory usage
by Muneeswaran Rajendran 14 Dec '17

14 Dec '17

Hi all, I’m trying to understand the implementation details and physical memory usage of seL4 for Tx1 we have available physical memory in Tx1 is 6GB. DRAM (4GB) - available address range 8000_0000 - FFFF_FFFF DRAM2 (4GB to 6GB) - available address range - 1_0000_0000 - 2_7FFF_FFFF In the hardware.h file (/kernel/include/plat/tx1/plat/machine/hardware.h),the avail_p_regs[] ={.start = 0x80000000, .end = 0xa7f00000 } '1MiB starting from 0xa7f00000 is reserved by the elfloader for monitor mode hooks'.I understand from the code its required only for Tk1. (/projects/tools/elfloader-tool/src/plat/tk1/monitor.S). As per my understanding is not not applicable for Tx1 so we can use contiguous region of physical ram 2GB to 4GB. Also it's allow to use higher physical memory for seL4 kernel ie > 4GB ? Thanks in advance. Regards, Munees

2 1