- Devel - lists.sel4.systems

How to prove correctness of my own program?
by Adam Badura 30 May '17

30 May '17

I expect this might be (or even probably is) a bad place to ask this but at the same time I didn't find any better coming from the Contact Information page (http://sel4.systems/contact/) I'm working on a conference paper (not sure if I will make it but still trying to - code::dive <http://codedive.pl/> if anyone would be interested) about proving program correctness. Considering my own knowledge in the field and expected knowledge of the audience there would be nothing new in that paper - more like an update on what is the current state of the field. Yet I wanted to supply also some examples. As main example I would like to show proof (or at least parts of it) of correctness (adherence to specification) of C++ code, possibly reduced to C code if need be. After research in this topic and finding this project some time ago it felt natural to reuse its tools. But I fail to do so. Could you possibly guide me? Using your tools and techniques what should I do to prove correctness of some piece of code. I think source code level would be more than enough - for this task no need to verify binary in any form. As a side example I would like to show how your proves look like. I'm not sure what you are generating / writing as a proof (that gets later verified automatically). I imagine a sequence of something. Some formulas in natural deduction perhaps? Or something else? Whatever that would be I guess it must be pretty long so it is not like I would show and analyze it all but instead would like to somehow let the audience "feel the size". If - as I expect - this is not the right place to ask and you cannot help me with above questions, could you at least point me to where to ask them? Adam Badura

2 1

camkes-arm-vm not registering GPIO?
by Steven Johnston 30 May '17

30 May '17

Hi All, I am playing around with the capabilities of the camkes-arm-vm project pn the Tegra TK1 and and wondering if someone else has come across this issue. It looks like GPIO functionality is not available in the buildroot. I can confirm the GPIO source is present and is being built: camkes-arm-vm/libs/libplatsupport/rc/plat/tk1/gpio.c camkes-arm-vm/libs/libplatsupport/plat_include/tk1/platsupport/plat/gpio.h [CC] src/plat/tk1/gpio.o The expected sysfs support is not present and looking and the relevant dmesg: # dmesg | grep gpio [ 0.057543] gpiochip_add: GPIOs 0..255 (tegra-gpio) failed to register [ 1.485061] input: gpio-keys as /devices/soc0/gpio-keys/input/input0 Any thoughts on what could be causing GPIO to the failing to register? Steven

2 4

About timer tests (CONFIG_HAVE_TIMER) in sel4test testsuites
by Jesse-SC Chou (周書正) 26 May '17

26 May '17

Hi seL4-hackers, I am porting the sel4test project to my custom target board, which contains an ARM Cortex-A7 core. The porting work is based on NVidia TK1 Cortex-A15 platform. In current stage, the seL4 kernel has booted up and the test benches can be tested. I can pass all tests except for the timer tests (turn off CONFIG_HAVE_TIMER). In my target, only ARM generic timer is used. My questions are: 1. Are the timer tests (CONFIG_HAVE_TIMER) designed for other platform timer besides ARM generic timer? If I only use ARM generic timer, should these timer tests be passed? 2. My goal is to running Linux with seL4 VMM on my target. The sel4platsupport_get_default_timer() is platform specific. If I only use ARM generic timer, should sel4platsupport_get_default_timer() be ported to return the ARM generic timer? If yes, is there any example for me to reference? BRs, Jesse

2 2

CapDL Spec Error
by Chris Guikema 22 May '17

22 May '17

Hello All, Has anyone come across this error before? [GEN] imx6_net.cdl While forming CapDL spec: failed to find dataport symbol 'camkes router router_send_buf data' in ELF router_group_bin make[1]: *** [imx6_net.cdl] Error 255 make[1]: *** Deleting file `imx6_net.cdl' make: *** [imx6_net] Error 2 Thanks, Chris Guikema

2 4

Blog post: seL4, CAmkES, and L4v dependencies
by Luke.Mondy＠data61.csiro.au 19 May '17

19 May '17

Hello all, We have published a blog post about how we manage software dependencies within Trustworthy Systems, and how it has been adapted to produce a relatively user-friendly interface. It is relevant for people both new and old to the seL4 ecosystem, as it simplifies and compartmentalises the elaborate software dependencies sometimes required to get things to build. You can read the blog post here: https://research.csiro.au/tsblog/getting-started-sel4-camkes-l4v-dependenci… If you have any feedback or changes you would like made, please let us know on the GitHub repo. Cheers, Luke -- Luke Mondy, Systems Administrator, Trustworthy Systems DATA61 | CSIRO M +61 0415 281 991 | https://ts.data61.csiro.au

1 0

Is there has any seL4 project support ARM Cortex-A7 ?
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi Everyone, Is there has any seL4 project support ARM Cortex-A7 ? I found seL4 official projects in below link. https://github.com/seL4 https://github.com/SEL4PROJ I use sel4test project that repo from https://github.com/seL4/sel4test-manifest.git And I found Xilinx zynq7000 support ARM Cortex-A9 in sel4test like below. File: sel4test/projects/sel4test/master-configs/zynq7000_release_xml_defconfig # # seL4 System # # CONFIG_ARCH_X86 is not set CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y # CONFIG_ARM1136JF_S is not set # CONFIG_ARM_CORTEX_A8 is not set CONFIG_ARM_CORTEX_A9=y # CONFIG_ARM_CORTEX_A15 is not set # CONFIG_PLAT_EXYNOS54XX is not set I can’t find seL4 project support ARM cortex-A7. Does anyone find it? Thanks, Joyce Peng

3 3

sel4test data abort when boot strap test program
by Joyce Peng(彭美僑) 19 May '17

19 May '17

Hi all, I tried to run seL4 test suite on my ARM Cortex-A7 target board. There is no error message when boot up seL4 kernel and boot strap test program on seL4 user land. But I got a “data abort” message after call sel4utils_map_page(..vaddr) and do memset(vaddr, 0, PAGE_SIZE_4K); There are some debug information list below. <1> I add debug message before the program that happen data abort diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c index c366a35..70d378a 100644 --- a/libsel4utils/src/vspace/bootstrap.c +++ b/libsel4utils/src/vspace/bootstrap.c @@ -107,13 +107,13 @@ static void *alloc_and_map(vspace_t *vspace, size_t size) { error = sel4utils_map_page(data->vka, data->vspace_root, frame.cptr, vaddr, seL4_AllRights, 1, objects, &num); + LOG_ERROR("my-hacker\n"); if (error) { vka_free_object(data->vka, &frame); LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error); return NULL; } + LOG_ERROR("my-hacker alloc_and_map() before memset vaddr=0x%x\n",vaddr); /* Zero the memory */ memset(vaddr, 0, PAGE_SIZE_4K); <2>Printed messages: ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p5 paddr=[20000000..2051881f] ELF-loading image 'kernel' paddr=[22000000..22032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[22033000..22463fff] vaddr=[8000..438fff] virt_entry=15f50 Enabling MMU and paging Jumping to kernel-image entry point... 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() alloc_and_map@bootstrap.c:111 my-hacker alloc_and_map@bootstrap.c:119 my-hacker alloc_and_map() before memset() vaddr=0xdf7fe000 <3>When happen data abort, the value of CPU registers: r1:0 r3:0xdf7fe000 lr:0xcbe8 <4>Objdump sel4test-driver. 0000cbc8 <memset>: cbc8: e3520000 cmp r2, #0 cbcc: e92d4030 push {r4, r5, lr} cbd0: 08bd8030 popeq {r4, r5, pc} cbd4: e0803002 add r3, r0, r2 cbd8: e6ef1071 uxtb r1, r1 cbdc: e3520002 cmp r2, #2 cbe0: e5431001 strb r1, [r3, #-1] cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6 It seems to write virtual address 0xdf7ff000. <5>The virtual address 0xdf7fe000 is not map in page table It seems sel4utils_map_page() not create page table for user land program correctly. Can anyone help me, how to solve this problem? Thanks! Joyce Peng(彭美僑)

4 12

seL4 on Cortex-A5
by Andrew Gacek 19 May '17

19 May '17

Is there any support for seL4 on the Cortex-A5? -Andrew

3 2

Change Access Right to Memory Pages
by Norrathep Rattanavipanon 04 May '17

04 May '17

Hello, I have some questions about how to change access rights in seL4. (I'm using native seL4, not camkes) 1) Currently, I'm using seL4_ARCH_Page_Remap to change an access right (from R/W to R/O) to a specific page (of other processes) at run-time. I'm doing as follows: seL4_CPtr frame = vspace_get_cap(&(p.vspace), p.thread.stack_top-1); // only for the stack int error = seL4_ARCH_Page_Remap(frame, ppd.cptr, seL4_CanRead, seL4_ARCH_Default_VMAttributes); Am I doing it correctly? The code seems to work fine for me but I just want to double check. 2) If my understanding in 1) is correct, the remap function only takes 1 cap at a time. So if I want to modify access rights of many pages, do I have to call the remap function multiple times? Or is there a more efficient way to do so? 3) I am also curious how the kernel handles the remap function. Does it simply flip/change some bits? Or does it involve page-related operations as well? e.g. unmap that page first and then remap the same region with a new access right? I guess it should be the former but I need to be sure about that. Thank you, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 7

seL4 Upgrading Issues
by Chris Guikema 04 May '17

04 May '17

Hello, I have developed an Ethernet application using CAmkES 2.2 and seL4 3.2. Because we are going to open-source the design and other documentation, I thought it would be a good idea to upgrade to the latest version of seL4 and CAmkES. I can pull the latest kernel and merge the compatible libraries with my changes and get everything to compile; however, when I load it on the board it fails... Failed to find any untyped capable of creating an object at address 0x20c4000 Failed to find a way to map address 0x20c4000 Failed to find any untyped capable of creating an object at address 0x20c8000 Failed to find a way to map address 0x20c8000 Failed to find any untyped capable of creating an object at address 0x20e0000 Failed to find a way to map address 0x20e0000 Failed to find any untyped capable of creating an object at address 0x21bc000 Failed to find a way to map address 0x21bc000 Here is my CAmkES configuration which sets up the Ethdrivers cnode and untypes. Keep in mind this works with seL4 3.2 ethdriver.simple = true; ethdriver.cnode_size_bits = 12; ethdriver.simple_untyped20_pool = 4; ethdriver.heap_size = 0; ethdriver.mmios = "0x02188000:0x4000:12, 0x021BC000:0x4000:12, 0x020E0000:0x4000:12, 0x020A4000:0x4000:12, 0x020B0000:0x4000:12, 0x020C4000:0x4000:12, 0x020C8000:0x1000:12"; Can anyone see the problem? Thanks, Chris Guikema

2 2