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
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've been looking at doing some builds with cmake and ninja experimentally
again.
Is anyone else doing this?
I noticed that some bugs are being filed about warnings from clang, but I
was only able to get some of the cmake + ninja stuff working when I used
gcc. How are people using clang?
So far, I haven't gotten a working build with cmake of sel4-tests. Is there
a good way to trouble shoot this or should I post more detailed info in a
thread on this list?
Thanks,
- Bruce
Hi,
Does anyone know when the Haskell support will be released in public? In the Language support section of https://wiki.sel4.systems/Suggested%20projects is says that it will be released in the near future, but the page was last edited on June 2016. I propose that the language section also contains links to where the source can be found.
I am also writing since I am working on porting the sel4-tutorial to Idris, which could be added to the list of languages, with a link to https://github.com/mokshasoft/sel4-idris-manifest There is a long way to go before it is finished, but if people want to help I accept patches.
/Jonas
Sent from [ProtonMail](https://protonmail.com), Swiss-based encrypted email.
Hi all,
Anyone has openssl working for seL4? I compiled a version of openssl it links correctly but as soon as the code calls BIO_new_mem_buf() the system crashed with:
FAULT HANDLER: data fault from vm.control (ID 0x03) on address 0xffffffb4 ,pc = 0xe259c, fsr = 0x3800006
If openssl is not available for now I wonder has anyone used other crypto library before, such as wolfssl, bearssl, etc.?
Best Regards
-Daniel Wang
Hi all,
With help from Dr. Chubb, I found there is a config to build CAmkES-ARM-VM as binary instead of ELF. However when I boot it on TK1 the process abort after loader code as follow. It is the same result when I convert ELF to BIN. Do you have any suggestion why this is happening (the paddrs and virt_entry are correct). Thank you very much!
Tegra124 (TK1-SOM) # ext2load mmc 0 0x90000000 capdl-loader-experimental-image-arm-tk1-bin
31897292 bytes read in 884 ms (34.4 MiB/s)
Tegra124 (TK1-SOM) # go 0x90000000
## Starting application at 0x90000000 ...
Copy monitor mode vector from 90001000 to a7f00000 size 50
Number of IRQs: 192
Load seL4 in nonsecure HYP mode 600001d3
ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3
paddr=[90000000..91e7ffff]
ELF-loading image 'kernel'
paddr=[80000000..8003cfff]
vaddr=[e0000000..e003cfff]
virt_entry=e0000000
ELF-loading image 'capdl-loader-experimental'
paddr=[8003d000..81f3efff]
vaddr=[10000..1f11fff]
virt_entry=184f8
Enabling MMU and paging
Jumping to kernel-image entry point...
abort() called.
Best Regards
-Daniel Wang
Data61 Seeking Proof Engineers
==============================
We are are hiring again!
If only there were a place where I could prove theorems for money, change the
world, and have fun while doing it...
Sounds too good to exist?
In the Trustworthy Systems team at Data61 that's what we do for a living. We
are the creators of seL4, the world's first fully formally verified operating
system kernel with extreme performance and strong security & correctness
proofs. Our highly international team is located on the UNSW campus, close to
the beautiful beaches of sunny Sydney, Australia, one of the world's most
liveable cities.
We are looking for 3 motivated proof engineers who want to join our team in Sydney,
move things forward, and have global impact. We are expanding our team,
because seL4 is going places. There are active projects around the world in
- Automotive - because cars have been hacked enough
- Aviation - for more security and safety for autonomous vehicles
- Defence - protecting confidential information
- Connected consumer devices - with security built in from the start
- Spaceflight - because awesome
To make these projects successful, we need to scale formal verification.
You would
- work on industrial-scale formal proofs in Isabelle/HOL
- develop formally verified infrastructure for building secure systems
on top of seL4
- contribute to improved proof automation and better reasoning techniques
- apply formal proof to real-world systems and tools
To apply for this position, you should possess a significant subset of the
following skills.
- functional programming in a language like Haskell, ML, or OCaml
- first-order or higher-order formal logic
- basic experience in C
- ability and desire to quickly learn new techniques
- undergraduate degree in Computer Science, Mathematics, or similar
- ability and desire to work in a larger team
We are hiring at two levels, so if you are more qualified or experienced than
the above would suggest, you can come in as a senior proof engineer.
If you additionally have experience
- in software verification with an interactive theorem prover such as
Isabelle/HOL, HOL4, or Coq, and/or
- with operating systems and microkernels
you should definitely apply!
If you have the right skills and background, we can provide training on the
job. Continual learning is a central component of everything we do. You will
work with a unique world-leading combination of OS and formal methods
experts, students at undergraduate and PhD level, engineers, and researchers
from 5 continents, speaking over 15 languages. Trustworthy Systems is a fun,
creative, and welcoming workplace with flexible hours & work arrangements.
We value diversity in all forms and welcome applications from people of all
ages, including people with disabilities, and those who identify as LGBTIQ.
See https://ts.data61.csiro.au/diversity/ for more information.
Salary ranges for this position, in AUD (plus superannuation):
- Junior: 80-91K
- Senior: 95-103K
depending on experience and qualifications.
Apply online at the following links:
- https://jobs.csiro.au/job/Sydney%2C-NSW-Proof-Engineer/464792900/
- https://jobs.csiro.au/job/Sydney%2C-NSW-Senior-Proof-Engineer/464792300/
Your application should include a cover letter, CV, undergraduate transcript
(if applicable), and contact information for two references.
This round of applications closes 15 April 2018.
The seL4 code and proof are open source. Check them out at https://seL4.systems
More information about Data61's Trustworthy Systems team at
https://ts.data61.csiro.au
Still studying? We also have internship opportunities!
https://ts.data61.csiro.au/students/
Hi,
I am new to sel4 and was thus practising the tutorials given at:
https://wiki.sel4.systems/Tutorials
While compiling tutorial 2 exercises, I got the attached error (I have
also attached the main.c file). Can someone please help me in resolving
it.
--
Thanks and Regards,
Amit Goyal