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
Hello,
I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE
extensions (NXP IMX6UL).
One of the experiments I wish to do is measure how fast I can get from POR
to seL4 doing something meningful.
To achive optimal boot speed I have a custom bootloader that does the bare
minimum.
The boot flow looks like this;
1. POR
2. Init HW
3. Load & verify blobs for trust zone and seL4
4. Jump to TEE init (OP-TEE)
5. Tee init code returns to bootloader with the CPU in HYP mode
At this point we're back in the bootloader, there is no MMU, D cache or I
cache active
6. Configure MMU
7. Jump to seL4 kernel entry
I'm currently struggling with getting the MMU properly setup and I was
hoping that someone here might shed some light on
what I would need to do. I've looked at the elf-loader and from what I can
understand it will setup a basic memory-mapping
for the kernel only.
Some of the questions that stand out in my head are :
1) How should the hand over work between the BL and seL4 with respect to
setting up more mappings, for example IO memory. Should the PGD & PMD
tables
created by the bootloader be shared with the kernel?
2) What needs to be configured before calling the seL4 entry?
Thanks,
Jonas
We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform.
Instructions are available for building and running the seL4 test suite on RISC-V: <https://docs.sel4.systems/Hardware/RISCV>
See an online copy of the release notes at:
<https://docs.sel4.systems/sel4_release/seL4_9.0.1>
<https://docs.sel4.systems/camkes_release/CAmkES_3.4.0>
# seL4 Version 9.0.1 Release
Announcing the release of `seL4 9.0.1` with the following changes:
9.0.1 2018-04-18: BINARY COMPATIBLE
## Changes
* On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs
which use any of the following functions may break, if the program relies on these functions to mask the
`label` field to the previous width of 20 bits.
- `seL4_MessageInfo_new`
- `seL4_MessageInfo_get_label`
- `seL4_MessageInfo_set_label`
* Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or
or multicore support on the Spike simulation platform. There is *no verification* for this platform.
## Upgrade Notes
---
# Full changelog
Refer to the git log in
<https://github.com/seL4/seL4> using `git log 9.0.0..9.0.1`
# More details
See the
[9.0.1 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf) included in the release or ask on the mailing list!# CAmkES Version camkes-3.3.0 Release
----
# CAmkES Version camkes-3.4.0 Release
Announcing the release of `` with the following changes:
camkes-3.4.0 2018-04-18
Using seL4 version 9.0.1
## Changes
## Upgrade Notes
---
# Full changelog
Use `git log camkes-3.3.0..camkes-3.4.0` in
<https://github.com/seL4/camkes-tool>
# More details
See the
[documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.4.0/docs/i…
or ask on the mailing list!
Hello,
Congrats on the RISC-V release!
I noticed some Device Tree code snuck in, replacing some hard coded bits in
the platform, and is intended to be exposed to the rootserver…
Any interest or intention to bring that to the ARM code, and possibly avoid
building kernels for specific platforms?
Thanks,
Jeff
Hello all, I'm new to seL4 and embedded systems, please bear with me. I'm
trying to use Sabrelite's UART1 (PS_SERIAL0), while I can make it write
data (putchar), I can't make it read (getchar).
The code is as follows on sel4 7.0.0, using platsupport/sel4platsupport:
ps_io_ops_t io_ops;
error = sel4platsupport_new_io_ops(vspace, vka, &io_ops);
printf("Initialising io_ops: %d\n",error);
ps_chardevice_t serial0;
ps_cdev_init(PS_SERIAL0,&io_ops,&serial0)
ps_chardevice_t serial1;
ps_cdev_init(PS_SERIAL1,&io_ops,&serial1); //CONSOLE
int character;
while (1) {
character = ps_cdev_getchar(&serial0);
//printf("%d\n",character);
if (character != -1) {
ps_cdev_putchar(&serial1,character);
printf("%d\n",character);
}
}
This runs fine on QEMU with -serial file/ttyUSB -serial mon:stdio. Next I
tried to run this on the Sabrelite board:
-Clone the 08-09 uboot from git, according to https://sel4.systems/Info/
Hardware/sabreLite/
-Apply patches 1 and 2 (applying 3 and 4 caused uboot to stall)
-Put uboot into SPI flash
-Restart, run the sel4 image on the SD card, with UART2 connected to PC's
RS232 and displayed by minicom, and UART1 connected to /dev/ttyUSB0
-Have a python script writing 'A's to /dev/ttyUSB0
sel4 loads but fails to read anything from /dev/ttyUSB0, UART1 just
receives EOFs (-1s). The rxd seems to always be 0. Swapping the UARTs
works, at the cost of losing the console:
while (1) {
character = ps_cdev_getchar(&serial1);
//printf("%d\n",character);
if (character != -1) {
ps_cdev_putchar(&serial0,character);
printf("%d\n",character);
}
}
So UART2 (default console) can read and write, while UART1 can write but
not read. Has anyone encountered the same problem? Suggestions much
appreciated.
Regards,
Leow Wei Xiang
I was running the following commands to build camkes:
1. repo init -u https://github.ls com/sel4/camkes-manifest.git
2. repo sync
3. make clean
4. make ia32_simple_defconfig; make silentoldconfig
5. make -j4
6. qemu-system-i386 -nographic -m 512 -cpu Haswell -kernel
images/kernel-ia32-pc99 -initrd
images/capdl-loader-experimental-image-ia32-pc99
Earlier it used to work perfectly fine but now it requires cmake 3.7.2
or higher which can be obviously be done by using pip install.
I just wanted to convey this so that the same may be updated on
prerequisites page.
(https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md)
--
Thanks and Regards,
Amit Goyal
Hi Kofi,
I am getting the attached error (Error Log.txt) while running seL4test.
Earlier it
used to run perfectly fine.
I am running the following commands:
$ repo init -u https://github.com/seL4/sel4test-manifest.git
$ repo sync
$ make clean
$ make ia32_simulation_release_xml_defconfig
$ make -j libmuslc && make
$ make simulate-ia32
Can you please look into this.
--
Thanks and Regards,
Amit Goyal
