Re: [seL4] Integer overflow bug in capdl-loader

Adrian, That is great to hear. Thanks for the feedback. Jeff Kubascik On 9/28/2017 12:24 AM, Adrian.Danis@data61.csiro.au wrote:

Hi Jeff,

The change looks good to me. Have applied it internally and will let it go through CI.

Thanks! Adrian

On Thu 28-Sep-2017 6:08 AM, Jeff Kubascik wrote:

...

Hello,

I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a bug that occurs when a device physical memory region includes the highest address, i.e. where the memory region ends at 0xFFFFFFFF on 32 bit systems. When I create a CAmkES component that uses the highest address, I see the following error.

ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..100ac81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[33000..1aefff] vaddr=[8000..183fff] virt_entry=befc Enabling MMU and paging Bootstrapping kernel Booting all finished, dropped to user space <>

Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() [Err seL4_NotEnoughMemory]:

I have traced this problem to an integer overflow bug in the capdl-loader. The patch below shows how I have addressed this error.

From 22c9dd76a31713c98710830c2ea865a4e5d8a078 Mon Sep 17 00:00:00 2001 From: Jeff Kubascik Date: Wed, 27 Sep 2017 13:52:36 -0400 Subject: [PATCH] Fixed integer overflow bug in capdl-loader that occurs when a device physical memory region ends at 0xFFFFFFFF

--- capdl-loader-app/src/main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index 34eedb0..305da2a 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -554,7 +554,7 @@ static int find_device_object(void *paddr, seL4_Word type, int size_bits, seL4_C /* Assume we are allocating from a device untyped. Do a linear search for it */ for (unsigned int i = 0; i < bootinfo->untyped.end - bootinfo->untyped.start; i++) { if (bootinfo->untypedList[i].paddr <= (uintptr_t)paddr && - bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) >= (uintptr_t)paddr + BIT(size_bits)) { + bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) - 1 >= (uintptr_t)paddr + BIT(size_bits) - 1) { /* just allocate objects until we get the one we want. To do this * correctly we cannot just destroy the cap we allocate, since * if it's the only frame from the untyped this will reset the