We now fixed this in the mainline repositories. Thanks for sharing. ________________________________ From: Devel on behalf of Nogin, Aleksey Sent: Thursday, 21 November 2019 7:52 PM To: devel@sel4.systems Subject: [seL4] Nasty bug in global-components/templates/rpc-signalling.template.c After spending a few hours debugging time server not working for me, I realized that global-components/templates/rpc-signalling.template.c that was added earlier this year contains the following /*- set badge = str(configuration[c.instance.name].get("%s_attributes" % c.interface.name)).strip('"') -*/ […] /*- do badges.sort() -*/ […] int /*? me.interface.name ?*/_largest_badge(void) { return /*? badges[len(badges) - 1] ?*/; } Unfortunately for me, my Trusted Build generated camkes had the attributes numbered 1,2,3,10,11,12,13 and therefore the above core was claiming that the time_server_largest_badge is 3 :(. Obviously, the issue is the combination of the str and sort, resulting in the last badge being the one largest lexicographically, not numerically :(. Replacing the str with int (and correspondingly removing the strip) solved the problem for me. P.S. Well, solved that particular problem for me, not the problem of time server not working – looks like now I will have to debug FAULT HANDLER: data fault from time_server.time_server_0_control (ID 0x2) on address 0x84b8ba, pc = 0x42439d, fsr = 0x4 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x42439d FAULT HANDLER: rsp :0x454cf0 FAULT HANDLER: rflags :0x10202 FAULT HANDLER: rax :0x413a33 FAULT HANDLER: rbx :0x437e88 FAULT HANDLER: rcx :0x0 FAULT HANDLER: rdx :0x437e98 FAULT HANDLER: rsi :0x28 FAULT HANDLER: rdi :0x437e98 FAULT HANDLER: rbp :0x454d70 FAULT HANDLER: r8 :0xffffffff FAULT HANDLER: r9 :0x0 FAULT HANDLER: r10 :0xe8 FAULT HANDLER: r11 :0x293 FAULT HANDLER: r12 :0x413a32 FAULT HANDLER: r13 :0x84b8ba FAULT HANDLER: r14 :0x0 FAULT HANDLER: r15 :0x0 FAULT HANDLER: fs_base :0x44a460 FAULT HANDLER: gs_base :0x0 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x0000000000458fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000458000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x0000000000457000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000456000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000455000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0000000000451000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0000000000450000 -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x0000000000400000 – :( Aleksey CONFIDENTIALITY NOTICE: The information transmitted in this email, including attachments, is intended only for the person(s) or entity to which it is addressed and may contain confidential, proprietary and/or privileged material exempt from disclosure under applicable law. Any review, retransmission, dissemination or other use of, or taking of any action in reliance upon this information by persons or entities other than the intended recipient is prohibited. If you received this message in error, please contact the sender immediately and destroy any copies of this information in their entirety.