Hi all,
I’m trying to test secure boot with the CAmkES-arm-vm. I found that U-boot has its implementation of secure boot called verified boot, but it seems only support FIT image format. I’m wondering is there a way to convert the final ELF image to an FIT image? I’m studying the details of different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much!
Best Regards
-Daniel Wang
Compile now no problem however I'm getting error when running. I believe
its an invalid opcode exception. I think my build not matching the qemu but
I've tried diff machines and they do the same.
I also get this warning during build, not sure if this relevant:
Warning: Installation path
/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool not
found on the PATH environment variable.
make: Leaving directory
`/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool'
Qemu commanr, lines with ????? suspect:
qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99
-initrd images/capdl-loader-experimental-image-ia32-pc99
(process:98550): GLib-WARNING **: gmem.c:483: custom memory allocation
vtable not supported
Boot config: parsing cmdline 'images/kernel-ia32-pc99 '
Boot config: console_port = 0x3f8
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
???? Warning: Your kernel was not compiled for the current
microarchitecture.
Parsing GRUB physical memory map
Physical Memory Region from 0 size 9fc00 type 1
Physical Memory Region from 9fc00 size 400 type 2
Physical Memory Region from f0000 size 10000 type 2
Physical Memory Region from 100000 size 1fefe000 type 1
Adding physical memory region 0x100000-0x1f800000
Physical Memory Region from 1fffe000 size 2000 type 2
Physical Memory Region from fffc0000 size 40000 type 2
Multiboot gave us no video information
Kernel loaded to: start=0x100000 end=0x160000 size=0x60000 entry=0x10005e
ACPI: RSDP paddr=0xf7180
ACPI: RSDP vaddr=0xdfcf7180
ACPI: RSDT paddr=0x1ffffbc1
ACPI: RSDT vaddr=0xdffffbc1
ACPI: FADT paddr=0x1ffff1c0
ACPI: FADT vaddr=0xdffff1c0
ACPI: FADT flags=0x80a5
ACPI: 0 IOMMUs detected
ACPI: MADT paddr=0x1ffffb11
ACPI: MADT vaddr=0xdffffb11
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd
ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd
ACPI: 1 CPU(s) detected
Detected 1 IOAPICs, but configured to use PIC instead
Detected 1 boot module(s):
module #0: start=0x161000 end=0x25aed0 size=0xf9ed0
name='images/capdl-loader-experimental-image-ia32-pc99'
ELF-loading userland images from boot modules:
size=0x189000 v_entry=0x804f544 v_start=0x8048000 v_end=0x81d1000
p_start=0x25b000 p_end=0x3e4000
Moving loaded userland images to final location: from=0x25b000 to=0x160000
size=0x189000
Starting node #0 with APIC ID 0
Booting all finished, dropped to user space
Caught cap fault in send phase at address 0x0
while trying to handle:
?????? user exception 0x6 code 0x0
in thread 0xff3f5d00 "rootserver" at address 0x805130e
With stack:
0x80cfda0: 0x0
0x80cfda4: 0x0
0x80cfda8: 0x0
0x80cfdac: 0x0
0x80cfdb0: 0x0
0x80cfdb4: 0x0
0x80cfdb8: 0x0
0x80cfdbc: 0x0
0x80cfdc0: 0x0
0x80cfdc4: 0x0
0x80cfdc8: 0x0
0x80cfdcc: 0x0
0x80cfdd0: 0x0
0x80cfdd4: 0x0
0x80cfdd8: 0x0
0x80cfddc: 0x0
QEMU: Terminated
Have a great day.
Hi all,
I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong).
Here is what I did so far:
1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev);
---------------------------------------------------
vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){
//uint32_t data = fault_get_data(fault);
uint32_t data = fault_get_ctx(fault)->r1;
vchan_entry_point(vm, data);
// fflush(stdout);
advance_fault(fault);
return 0;
}
struct device vchan_dev = {
.devid = DEV_CUSTOM,
.name = "vchan-driver",
.pstart = 0x2040000,
.size = 0x1000,
.handle_page_fault = &vchan_device_fault_handler,
.priv = NULL,
};
---------------------------------------------------
2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following:
---------------------------------------------------
int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) {
int res = 0;
int err;
unsigned phys_ptr = virt_to_phys(vmcall);
vmcall->data = data;
vmcall->cmd = cmd;
vmcall->phys_data = virt_to_phys(data);
vmcall->size = sz;
down(&hyp_sem);
/*
Set up arguments for the ARM hyp call
*/
asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1");
asm volatile (".arch_extension virt\n\t” "hvc #0");
asm volatile ("mov %0, r0" : "=r" (res) : : );
err = vargs->err;
up(&hyp_sem);
return err;
}
---------------------------------------------------
The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information.
---------------------------------------------------
# modprobe driver.ko
[81.826621] driver: loading out-of-tree module taints kernel
Bad sys call from [Linux]: scone 0 at PC: 0xbf000214
Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407)
—————————————————————————
I’m not sure if this error is triggered by the modified call_into_hypervisor() or by event_thread_run()->eventfd_signal().
Any help would be appreciated! Thanks in advance.
Best Regards
-Daniel Wang
Hi,
After hours of debugging I have discovered a quite nasty issue where
seL4_Wait() crash if I build the kernel without optimization (gcc option
-O0) on a pc99 tested with qemu.
How to reproduce: Just create an endpoint (from a vka) and call
seL4_Wait(). The simplest reproducer can be obtained from the hello-2
tutorial:
- Copy the main.c from the solution directory in the apps/hello-2/src/main.c
- Add the following codes right after the creation of vka (TASK 5, approx
line 150):
{
printf("WAITING----------------------------------------------\n");
seL4_Word myBadge;
vka_object_t ep_object = {0};
error = vka_alloc_endpoint(&vka, &ep_object);
ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n");
seL4_Wait(ep_object.cptr, &myBadge);
printf("---------------------------------------------- DONE!!\n");
}
Essentially the added code, creates an endpoint using vka and calls
seL4_Wait() on it... I expect the code to block forever since there are no
other threads that can unblock it...
- Build it and run it with:
make pc99_hello-2_defconfig
make
make simulate
Expected output:
Booting all finished, dropped to user space
4 untypeds of size 12
4 untypeds of size 13
[...]
6 untypeds of size 29
WAITING----------------------------------------------
- Now change the configuration using 'make menuconfig' and select:
seL4 Kernel -> Build Options -> Compiler optimisation flag (-O2)
and change it to -O0, save the new configuration.
- Rebuild and run:
make simulate
Now you get a kernel exception:
[...]
6 untypeds of size 29
WAITING----------------------------------------------
========== KERNEL EXCEPTION ==========
Vector: 0xd
ErrCode: 0xa658
IP: 0xe0118ce5
SP: 0xffaf7e28
FLAGS: 0x86
CR0: 0x8001003b
CR2: 0x0 (page-fault address)
CR3: 0x142000 (page-directory physical address)
CR4: 0x100290
Stack Dump:
*0xffaf7e28 == 0xe011a658
*0xffaf7e2c == 0x0
*0xffaf7e30 == 0x0
*0xffaf7e34 == 0xe011a658
*0xffaf7e38 == 0x8
*0xffaf7e3c == 0x202
*0xffaf7e40 == 0x0
*0xffaf7e44 == 0x0
*0xffaf7e48 == 0x10
*0xffaf7e4c == 0x7
*0xffaf7e50 == 0x0
*0xffaf7e54 == 0x0
*0xffaf7e58 == 0x0
*0xffaf7e5c == 0x0
*0xffaf7e60 == 0x0
*0xffaf7e64 == 0x0
*0xffaf7e68 == 0x0
*0xffaf7e6c == 0x0
*0xffaf7e70 == 0x0
*0xffaf7e74 == 0x0
Halting...
halting...
Kernel entry via Interrupt, irq 157
Version info:
- gcc: gcc (GCC) 4.8.5 20150623 (Red Hat 4.8.5-11)
- qemu: QEMU emulator version 2.0.0, Copyright (c) 2003-2008 Fabrice
Bellard
- Build environment: CentOS Linux release 7.3.1611 (Core)
Other info:
- gcc 4.8.5 doesn't seem to support the 'Nehalem' x86 microarchitecture,
so I am selecting the 'Generic' microarchitecture (Toolchain Options -> X86
microarchitecture)
- Even the tutorial 'hello-timer' fails exactly with the same exception
without any modifications if you build the kernel with -O0.
- Tested on a Beaglebone black: no problems compiling kernel with -O0
Regards,
Fabrizio Bertocci
Real-Time Innovations, Inc.
Hi all,
I was going through the tutorials, unfortunately I've been finding very
challenging to follow the instructions as I keep encountering issues after
issue.
First, the repo command seems to be incorrect. In document:
https://docs.sel4.systems/Tutorials/
it says:
repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -m
sel4-tutorials.xml
but the manifest file 'sel4-tutorials.xml' does not exist on the git
repository (of the sel4-tutorial-manifest).
What is the correct manifest file to use? There are two manifests (in any
branch and tag): master.xml and default.xml. default.xml seems to use the
'new' format of identifying the individual versions of the libraries
(through the hash).
Let's assume the correct manifest to use is the 'default.xml' from the
'sel4-tutorials' branch and initialize the workspace with:
repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest -b
sel4-tutorials
repo sync
So, now: first tutorial, ok (but this tutorial does very little). Second
tutorial (hello-2), not so good... to avoid mistake, I am copying directly
the solution into the app area:
cp projects/sel4-tutorials/solutions/hello-2/src/main.c
apps/hello-2/src/main.c
make pc99_hello-2_defconfig
make
... and the build fails with:
[...]/workspaces/sel4-tutorials-2/stage/x86/pc99/lib/libsel4allocman.a(virtual_pool.o):
In function `_add_page':
[...]/workspaces/sel4-tutorials-2/libs/libsel4allocman/src/mspace/virtual_pool.c:52:
undefined reference to `vspace_get_map_obj'
The missing function appears to be part of libsel4vspace, that is missing
from the library dependency list. Let's add it to add it to the
apps/hello-2/Makefile:
diff --git a/exercises/hello-2/Makefile b/exercises/hello-2/Makefile
index 25c0b35..97a4fc6 100644
--- a/exercises/hello-2/Makefile
+++ b/exercises/hello-2/Makefile
@@ -28,6 +28,7 @@ ASMFILES += $(patsubst $(SOURCE_DIR)/%,%,$(wildcard
$(SOURCE_DIR)/src/plat/${PLA
# Libraries required to build the target
LIBS = c sel4 sel4muslcsys \
sel4simple sel4vka sel4allocman \
+ sel4vspace \
sel4platsupport platsupport \
utils sel4simple-default sel4utils sel4debug
Now it builds successfully, unfortunately when running, the child thread
doesn't appear to run at all. This is the output of qemu running 'make
simulate':
Booting all finished, dropped to user space
4 untypeds of size 12
5 untypeds of size 13
5 untypeds of size 14
4 untypeds of size 15
4 untypeds of size 16
4 untypeds of size 17
4 untypeds of size 18
5 untypeds of size 19
5 untypeds of size 20
2 untypeds of size 21
4 untypeds of size 22
4 untypeds of size 23
2 untypeds of size 24
3 untypeds of size 25
3 untypeds of size 26
3 untypeds of size 27
1 untypeds of size 28
6 untypeds of size 29
main: hello world
I would have expected seeing on the output the string 'thread_2: hallo
wereld' somewhere...
Why the thread 2 does not run? This code was working last time I checked
(version 5.2).
I tried then to continue testing the tutorials, and I went to the hello-3.
Hello-3 is based on the Hello-2 but adds an endpoint for IPC between the
main thread and the child thread.
Surprisingly, this app not only builds out of the box without errors
(apparently libsel4vspace was already added to its Makefile), but even
running it, works as expected:
Booting all finished, dropped to user space
3 untypeds of size 12
5 untypeds of size 13
5 untypeds of size 14
4 untypeds of size 15
4 untypeds of size 16
4 untypeds of size 17
4 untypeds of size 18
5 untypeds of size 19
5 untypeds of size 20
2 untypeds of size 21
4 untypeds of size 22
4 untypeds of size 23
2 untypeds of size 24
3 untypeds of size 25
3 untypeds of size 26
3 untypeds of size 27
1 untypeds of size 28
6 untypeds of size 29
main: hello world
thread_2: hallo wereld
thread_2: got a message 0x6161 from 0x61
main: got a reply: 0xffff9e9e
Right now I suspect that seL4_TCB_Configure() does not work correctly if we
don't provide an endpoint (because that's essentially the main difference
between the two tests).
Can somebody try to run the tutorials and perhaps confirm the problem?
Regards,
Fabrizio Bertocci
Real-Time Innovations, Inc.
Sunnyvale, CA
Hi all,
I'm using the docker build environment provided by
https://github.com/SEL4PROJ/seL4-CAmkES-L4v-dockerfiles
Currently, "make sel4" fails with this message:
E: Package 'ncurses-dev' has no installation candidate
Anyone experimenting the same behaviour?
Cheers,
Paolo
Dear all,
I stumbled into some problems with AutoCorres and would be grateful if
someone could help me. I used the recent version autocorres1.4 under
Isabelle2017.
A) Running under MacOS, cpp is apparently not running inside install_C_file
(yes, I installed the cpp wrapper:
>>>>>>>>>>>>>>>>>>>>>>
!/bin/bash
# Wrapper for clang C preprocessor on MacOS
export L4CPP="-DTARGET=ARM -DTARGET_ARM -DPLATFORM=Sabre -DPLATFORM_Sabre"
llvm-gcc -Wno-invalid-pp-token -E -x c $@
<<<<<<<<<<<<<<<<<<<<<<
and made sure that it is in the path of the shell in which I started Isabelle.)
Does anyone know a cause for this behaviour or a feasible workaround ?
(besides doing the expansions by hand)
Is there an explicit Isabelle shell variable where the path to cpp must be set ?
B) I get a weird crash of AutoCorres without a clue what might cause it:
I have a T4.h file with
>>>>>>>>>>>>>>>>>>>>>>>
#define N_TEETH ( 100 * MODULO ) // shaft encoder's number of teeth per turn
#define SIZE_OF_SPEED_FIFO 10 // number of samples to compute average speed
extern const char *InputField[];
enum State { S1=1, S2, S3, S4, S5, S6, SFail=0 };
enum Status { FAIL, SUCCESS };
enum InputPatterns { Ph1 = 1, Ph2 = 5, Ph3 = 4, Ph4 = 6, Ph5 = 2, Ph6 = 3 };
struct OBits {
int C1 ;
int C2 ;
int C3 ;
} Obits;
/********* Output data *****************/
extern enum Status O_Position_Valid;
extern unsigned int O_Position_Count;
extern unsigned int Relative_Position;
extern int Instantaneous_Speed;
extern int Mean_Speed;
<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
and a T4.c file with:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>>
#include "T4_AlgoODO.h"
enum Status O_P_V = SUCCESS;
unsigned int O_P_C = 0;
unsigned int Relative_Position = 0;
int I_Speed = 0;
int Mean_Speed = 0;
int Acceleration = 0;
int scale = 1000;
int PI_approx = 3141;
struct OBits Input;
enum State OState;
const unsigned int Radius = 500;
const unsigned int Sampling_Rate = 400;
unsigned int F_O_P_C = 0;
int Speed_FIFO[10 /*SIZE_OF_SPEED_FIFO*/];
int FIFO_pointer = 0;
<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<
Loading this in Isabelle/AutoCorres with:
>>>>>>>>>>>>>>>>>>>>>>>>>
install_C_file "code/c/T4.c”
<<<<<<<<<<<<<<<<<<<<<<<<<
results in the following AutoCorres crash:
…
exception Fail raised (line 175 of "~/codebox/odo_new/odo/autocorres-1.4/c-parser/calculate_state.ML"): translate_inttype: incomplete array!
Can anybody tell me what this means and propose a workaround ?
Best regards
B. Wolff
Hi!
I could use a clue as to the cause of this problem.
The program has its free slots start index set correctly.
It is trying to allocate a dma buffer. (4k with a known physical address).
The vspace has been properly set up and knows the phys addresses of its free memory.
This used to work fine in a different process, but I can't find anything I've done
different/wrong in this one...
I've added some extra printfs, and some debug code (in kernel/src/object/untyped.c).
/* Ensure that the destination slots are all empty. */
slots.cnode = CTE_PTR(cap_cnode_cap_get_capCNodePtr(nodeCap));
slots.offset = nodeOffset;
slots.length = nodeWindow;
for (i = nodeOffset; i < nodeOffset + nodeWindow; i++) {
status = ensureEmptySlot(slots.cnode + i);
if (status != EXCEPTION_NONE) {
userError("Untyped Retype: Slot #%d from %p in destination window non-empty.", (int)i, (void *)slots.cnode);
userError("Untyped Retype: At offset #%d length %d.", (int)nodeOffset, (int)nodeWindow);
int j = 0;
for(j=0;j<2048;j++){
status = ensureEmptySlot(slots.cnode + (i + j));
if (status == EXCEPTION_NONE) {
userError("Next Free Slot at #%d from %p.", (int)(i+j), (void *)slots.cnode);
status = EXCEPTION_SYSCALL_ERROR;
break;
}
}
return status;
}
}
And finally, here is the output from the console:
<<seL4(CPU 0) [decodeCNodeInvocation/94 T0xffffff8001a25400 "Lockmaproc" @4196e8]: CNode Copy/Mint/Move/Mutate: Destination not empty.>>
<<seL4(CPU 0) [decodeUntypedInvocation/166 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: Slot #196 from 0xffffff807f000000 in destination window non-empty.>>
<<seL4(CPU 0) [decodeUntypedInvocation/167 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Untyped Retype: At offset #196 length 1.>>
<<seL4(CPU 0) [decodeUntypedInvocation/172 T0xffffff8001a25400 "Lockmaproc" @420f2c]: Next Free Slot at #197 from 0xffffff807f000000.>>
_refill_pool@split.c:187 Failed to retype untyped, error 8
vka_alloc_object_at_maybe_dev@object.h:59 Failed to allocate object of size 4096, error 1
dma_alloc@page_dma.c:92 Failed to allocate untyped of size 12
I need a hint... help?
Thanks!
Richard
________________________________
This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
Hi there,
I have written a seL4 app using CAmkES, that I am continuously building
using Jenkins.
I'd like to add a test step to this continuous integration process,
launching the app with qemu and parsing the output to validate my
expectations.
The thing is, although all the active ("control") components reach their
last instruction after a while, seL4 does not "exit" (which is expected
I guess) and qemu does not stop, keeping my continuous integration job
running for ever.
Any idea on how to achieve this?
Thank you very much in advance.
Cheers,
Paolo Crisafulli