Hello, I have question about sel4's new ninja build tool.
*1. From now on, sel4-tutorials use ninja build tool, so I repo new
sel4-tutorials.Last step, I executue this command "../init-build.sh --plat
pc99 --tut hello-1" but It prints with this error messages.What's the
problem?---------------------------------------------------------------------------------------------CMake
Warning at tools/cmake-tool/flags.cmake:123 (message): Kernel supports
hardware floating point but toolchain does notCall Stack (most recent call
first): tools/cmake-tool/base.cmake:58 (include)
tools/cmake-tool/all.cmake:16 (include) CMakeLists.txt:23 (include)CMake
Error at projects/sel4-tutorials/CMakeLists.txt:34 (message): You must
select a tutorial for compilation. Select using -DTUTORIAL=<PREFERENCE>.
Choose one of
hello-1;hello-2;hello-2-nolibs;hello-3;hello-3-nolibs;hello-4;hello-4-app;hello-timer;hello-timer-client.--
Configuring incomplete, errors occurred!See also
"/home/scribnote5/sel4-tutorials-manifest/build_hello_1/CMakeFiles/CMakeOutput.log".2.
How can I build sel4 ia32 images in sel4bench?This command
"../init-build.sh -DPLATFORM=ia32 -DHARDWARE=TRUE -DAARCH32=TRUE
-DRELEASE=TRUE -DFAULT=TRUE -DFASTPATH=TRUE" doesn't make sel4bench image
file.*
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,
I need your help in trying to understand what is the best way to implement
a permanent fix I can push on the seL4 repository regarding the
incompatibility issues between the libethdriver and MUX interface of the
platsupport.
This apply to the iMX6 ethernet driver. I'm not sure about other platforms.
In short, the problem is that platsupport takes ownership of the entire MUX
(maps the I/O) when the io_ops are initialized:
Repo: seL4/seL4_libs
File: libsel4platsupport/src/io.c
Function: sel4platsupport_new_io_ops
...
mux_sys_init(io_ops, get_mux_dependencies(), &io_ops->mux_sys);
...
The above call end up calling the platform-specific mux_sys_init that maps
only the first 4Kb of IO space from address 0x020e0000 (the base address of
the IOMUX controller - note: the IOMUX controller uses 16Kb of address
space for its registers, not 4Kb!!!):
Repo: seL4/util_libs
File: libplatsupport/src/plat/imx6/mux.c
Function: mux_sys_init
...
MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc);
return imx6_mux_init_common(mux);
The pointer "io_ops->mux_sys->priv" should point to the base address of the
IOMUX of the SoC (in the virtual memory space of the calling process).
The Ethernet driver unfortunately attempts to map the IOMUX again:
Repo: seL4/util_libs
File: libethdrivers/src/plat/imx6/uboot/mx6qsabrelite.c
Function: setup_iomux_enet
...
void *base = RESOURCE(&io_ops->io_mapper, IOMUXC);
...
// Modify the IOMUX registers, then release the mapped IO:
...
UNRESOURCE(&io_ops->io_mapper, IOMUXC, base);
but using a larger size (the full 16Kb from the same base address of the
IOMUX controller).
So, the ethernet controller attempt to map the IO fails because it is
already mapped, and nothing works.
Right now in my project I've entirely commented out the initialization of
the MUXC from the sel4platsupport_new_io_ops function.
I understand that if the io_ops attempt to map the MUX (and leave it
mapped) there must be a reason, unfortunately I fail to see it. The
structure describing the MUXC register (struct imx6_iomuxc_regs, defined in
libplatsupport/src/plat/imx6/mux.c) is private and not accessible outside
that file, and the only two interface functions available
(mux_feature_enable/mux_feature_disable) are not enough to be usable by the
ethernet driver.
The ethernet driver could also attempt to reuse the same mapped IOMUX
(beside that the size of the mapped area is different and won't work
anyway), but that will require using the 'priv' field of the
io_ops->mux_sys (beside, even trying to map the whole 16Kb of the IOMUX and
have the driver to reuse the same mapped address, for some unknown reasons
it doesn't work).
So, what is the right approach to fix this problem?
Why the MUX subsystem maps some IO, never release it and keep it private
for most of it?
The IOMUX has been introduced somewhere between version 1.0 and 9.x... and
it seems a half-baked job... Can we just comment it out if nobody is using
it?
Or if you have some ideas/suggestions on how to expand it in such a way the
ethernet driver could use, please let me know. I'll be happy to implement
it.
Regards,
Fabrizio
I just checked out a fresh copy of https://github.com/
SEL4PROJ/camkes-arm-vm-manifest and built an image for the TK1 using the
docker build environment. I copied the resulting image to an SD card and it
boots fine.
If I switch to the unsecure mode, I get an error on boot.
SMMU Address translation error:
ID: 98 address: 0xae5be000 type: 6 direction: 0x0
IOPT permission: read 0x0 write 0x0 nonsecure 0x0
[ 10.204777] mmc1: ADMA error
I have not made any changes, so my vm.smmu settings are all default.
Any thoughts or help?
Mike
* I have question about process and thread in tutorials. 1. sel4 doesn't
have process concept.But making new process is exist in tutorial
hello-4.What is the exactly difference trhead in hello-2 and process in
hello-4?2. In tutorials hello-4, where can I find access path that hello-4
process link hello-4-app?It means I think hello-4 process should designate
hello-4-app's path.*
Hello,
I understand that the proof for seL4 implies that the compiler and linker
do not need to be trusted, because their output can be verified by a tool.
Does this output-verification also apply to CAmkES
C code for components and interfaces?
Specifically, I'm working on a project where we want to have certain
functionality implemented in C to be run on the seL4 microkernel. Would we
gain any proof by using compcert, or is the output-verification sufficient?
And is there any way to execute previously-compiled C binaries in a CAmkES
component?
I tried system calls, but I learned that won't work with the microkernel :-)
I looked into the build architecture of the project, but I couldn't find
where CAmkES components were being compiled.
I looked into replacing gcc with compcert for the system, but there are
used many flags available to gcc that are not available to compcert, so I
scratched that idea.
Thank you for your help.
-Michael
Hi Members,
I am trying to port SEL4 on RISCV hardware. I am stuck in finding the
DTB/DTS files path in sel4test folder. Could someone guide me where these
files exist and how to change the memory map for UART console. Actually, We
changed the code for putchar in systems.c for Linux. So, I am trying to
figure out, how to do something similar for SEL4.
Please let me know, if someone has ported SEL$ to RISCV hardware.
--
regards,
Sathya
