- Devel - lists.sel4.systems

python-capdl sets incorrect permissions on elf setions
by Joseph Takagi 28 Jan '18

28 Jan '18

Hi I believe the capdl python tool does not correctly set permissions on data loaded from component ELF files. I am wondering if this is a known issue with a fix or whether I'm best off diving in and attempting to fix it myself. Im running on a 32-bit ARM platform The camkes generated linker scripts result in several ELF sections (including .rodata .text and .bss) being lumped together in a single ELF segment. The permissions on this segment in the ELF segment header are RWE. This can be seen from the example output below. readelf -l foo_group_bin Elf file type is EXEC (Executable file) Entry point 0x107b64 There are 4 program headers, starting at offset 52 Program Headers: Type Offset VirtAddr PhysAddr FileSiz MemSiz Flg Align EXIDX 0x021ad8 0x00111ad8 0x00111ad8 0x00008 0x00008 R 0x4 LOAD 0x010000 0x00100000 0x00100000 0x12178 0xd9000 RWE 0x10000 <-- .bss .text .rodata etc. are here with RWE permissions LOAD 0x030000 0x00200000 0x00200000 0x00000 0x01000 RW 0x10000 GNU_STACK 0x000000 0x00000000 0x00000000 0x00000 0x00000 RWE 0x10 Section to Segment mapping: Segment Sections... 00 .ARM.exidx 01 .text .init .fini .rodata .eh_frame .ARM.exidx .data .init_array .fini_array .jcr __vsyscall .bss guarded 02 ignore_fooregs 03 The individual sections are given more sensible permissions via their respective section headers, as can be seen below: .text has permissions 'AE' for alloc and execute, .rodata has 'A' and .bss has 'AW', etc. readelf -S ./foo_group_bin There are 28 section headers, starting at offset 0x8524c: Section Headers: [Nr] Name Type Addr Off Size ES Flg Lk Inf Al [ 0] NULL 00000000 000000 000000 00 0 0 0 [ 1] .text PROGBITS 00100000 010000 00eb68 00 AX 0 0 4096 <-- .text can't be written [ 2] .init PROGBITS 0010eb68 01eb68 000014 00 AX 0 0 4 [ 3] .fini PROGBITS 0010eb7c 01eb7c 000014 00 AX 0 0 4 [ 4] .rodata PROGBITS 0010f000 01f000 002ad4 00 A 0 0 4096 <-- .rodata is read-only [ 5] .eh_frame PROGBITS 00111ad4 021ad4 000004 00 A 0 0 4 [ 6] .ARM.exidx ARM_EXIDX 00111ad8 021ad8 000008 00 AL 1 0 4 [ 7] .data PROGBITS 00112000 022000 000168 00 WA 0 0 4096 [ 8] .init_array INIT_ARRAY 00112168 022168 000004 00 WA 0 0 4 [ 9] .fini_array FINI_ARRAY 0011216c 02216c 000004 00 WA 0 0 4 [10] .jcr PROGBITS 00112170 022170 000004 00 WA 0 0 4 [11] __vsyscall PROGBITS 00112174 022174 000004 00 WA 0 0 4 [12] .bss NOBITS 00112178 022178 000b08 00 WA 0 0 8 [13] guarded NOBITS 00113000 022178 0c6000 00 WA 0 0 4096 [14] ignore_fooregs NOBITS 00200000 030000 001000 00 WA 0 0 1048576 [15] .debug_info PROGBITS 00000000 022178 027a60 00 0 0 1 [16] .debug_abbrev PROGBITS 00000000 049bd8 00a4d4 00 0 0 1 [17] .debug_loc PROGBITS 00000000 0540ac 0113f1 00 0 0 1 [18] .debug_aranges PROGBITS 00000000 0654a0 000ef8 00 0 0 8 [19] .debug_line PROGBITS 00000000 066398 00c5ff 00 0 0 1 [20] .debug_str PROGBITS 00000000 072997 0060c1 01 MS 0 0 1 [21] .comment PROGBITS 00000000 078a58 000038 01 MS 0 0 1 [22] .ARM.attributes ARM_ATTRIBUTES 00000000 078a90 000039 00 0 0 1 [23] .debug_frame PROGBITS 00000000 078acc 002638 00 0 0 4 [24] .debug_ranges PROGBITS 00000000 07b108 002238 00 0 0 8 [25] .shstrtab STRTAB 00000000 085137 000114 00 0 0 1 [26] .symtab SYMTAB 00000000 07d340 005230 10 27 1269 4 [27] .strtab STRTAB 00000000 082570 002bc7 00 0 0 1 Key to Flags: W (write), A (alloc), X (execute), M (merge), S (strings) I (info), L (link order), G (group), T (TLS), E (exclude), x (unknown) O (extra OS processing required) o (OS specific), p (processor specific) The ELF.py code from python-capdl applies the segment permissions to the entire segment so disregards the permissions in the ELF section headers. As a result, data which shouldn't be writable or executable are so. I can confirm this through analysis of the capdl output which shows the entire segment being mapped as 64KB pages with RWE permissions set. Any advice on this would be appreciated. Joe Takagi

2 1

Fileserver connection error in RefOS
by ALVI Aslam (MORPHO) 23 Jan '18

23 Jan '18

Hello All, Greetings, I was trying to run RefOs for ia32_defconfig. Found some error while building but after removing all of them I was able to run it. But now I have an error while selfLoader is trying to laod Terminal or Timer_Server. [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [/fileserv/terminal] ERROR main(): Error while connecting to file server. [00.84] PROCSERV | proc_exit_handler(): Process PID 2043 exiting with status 0 !!! [00.85] PROCSERV | proc_syscall_postaction(): Releasing process 2043 [/fileserv/terminal]... [00.0] SELFLOADER | main(): --- Starting RefOS process selfloader --- [00.1] SELFLOADER | main(): Connect to the server for [fileserv/timer_server] ERROR main(): Error while connecting to file server. I have also attached the full log of execution. I have also debugged it and found that while resolving the serverPath its get failed. Please help me out to resolve this issue. Thank You in advance Regards, Aslam

1 0

Hyperkernel paper
by Jeff Waugh 23 Jan '18

23 Jan '18

Hi seL4 friends, Any thoughts and/or feelings about the Hyperkernel paper from SOSP'17? This paper describes an approach to designing, implementing, and formally > verifying the functional correctness of an OS kernel, named Hyperkernel, > with a high degree of proof automation and low proof burden. https://homes.cs.washington.edu/~helgi/papers/hyperkernel.pdf Thanks, Jeff

2 1

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 04 Jan '18

04 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 04 Jan '18

04 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