- Devel - lists.sel4.systems

camkes tutorial build compilation error
by Thad Seeberger 03 Apr '18

03 Apr '18

Good day, I am working thru the examples. make arm_hello-camkes-0_defconfig; make -- compiles and run on qemu The I tried x86 architecture make ia32_hello-camkes-0_defconfig; make -- build error I cant find declarations for any of the listed errors. I'm guessing these should be dynamically defined before the build based on the architecture. Please let me know what I'm doing wrong. thx [CC] kernel_final.s /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c: In function ‘decodeIA32PageDirectoryInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: error: ‘X86PageDirectoryGetStatusBits’ undeclared (first use in this function); did you mean ‘performIA32PageDirectoryGetStatusBits’? case X86PageDirectoryGetStatusBits: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~ performIA32PageDirectoryGetStatusBits /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/32/kernel/vspace_32paging.c:263:10: note: each undeclared identifier is reported only once for each function it appears in /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86FrameInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:854:10: error: ‘X86PageMap’ undeclared (first use in this function); did you mean ‘ARMPageMap’? case X86PageMap: { /* Map */ ^~~~~~~~~~ ARMPageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1012:10: error: ‘X86PageRemap’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageRemap: { /* Remap */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1143:10: error: ‘X86PageUnmap’ undeclared (first use in this function); did you mean ‘X86PageRemap’? case X86PageUnmap: { /* Unmap */ ^~~~~~~~~~~~ X86PageRemap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1166:10: error: ‘X86PageMapIO’ undeclared (first use in this function); did you mean ‘X86PageMap’? case X86PageMapIO: { /* MapIO */ ^~~~~~~~~~~~ X86PageMap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1175:10: error: ‘X86PageGetAddress’ undeclared (first use in this function); did you mean ‘ARMPageGetAddress’? case X86PageGetAddress: { ^~~~~~~~~~~~~~~~~ ARMPageGetAddress /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86PageTableInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1236:21: error: ‘X86PageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86PageTableUnmap) { ^~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1246:21: error: ‘X86PageTableMap’ undeclared (first use in this function); did you mean ‘X86PageTableUnmap’? if (invLabel != X86PageTableMap ) { ^~~~~~~~~~~~~~~ X86PageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c: In function ‘decodeX86MMUInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1365:25: error: ‘X86ASIDControlMakePool’ undeclared (first use in this function); did you mean ‘ARMASIDControlMakePool’? if (invLabel != X86ASIDControlMakePool) { ^~~~~~~~~~~~~~~~~~~~~~ ARMASIDControlMakePool /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/kernel/vspace.c:1434:25: error: ‘X86ASIDPoolAssign’ undeclared (first use in this function); did you mean ‘ARMASIDPoolAssign’? if (invLabel != X86ASIDPoolAssign) { ^~~~~~~~~~~~~~~~~ ARMASIDPoolAssign /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c: In function ‘Arch_decodeIRQControlInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:122:10: error: ‘X86IRQIssueIRQHandlerIOAPIC’ undeclared (first use in this function); did you mean ‘invokeIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerIOAPIC: { ^~~~~~~~~~~~~~~~~~~~~~~~~~~ invokeIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/interrupt.c:144:10: error: ‘X86IRQIssueIRQHandlerMSI’ undeclared (first use in this function); did you mean ‘X86IRQIssueIRQHandlerIOAPIC’? case X86IRQIssueIRQHandlerMSI: { ^~~~~~~~~~~~~~~~~~~~~~~~ X86IRQIssueIRQHandlerIOAPIC /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c: In function ‘decodeX86PortInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:21: error: ‘X86IOPortOut8’ undeclared (first use in this function) if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~ /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:50: error: ‘X86IOPortOut16’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:62:80: error: ‘X86IOPortOut32’ undeclared (first use in this function); did you mean ‘X86IOPortOut16’? if (invLabel == X86IOPortOut8 || invLabel == X86IOPortOut16 || invLabel == X86IOPortOut32) { ^~~~~~~~~~~~~~ X86IOPortOut16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:75:10: error: ‘X86IOPortIn8’ undeclared (first use in this function); did you mean ‘X86IOPortOut8’? case X86IOPortIn8: { /* inport 8 bits */ ^~~~~~~~~~~~ X86IOPortOut8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:89:10: error: ‘X86IOPortIn16’ undeclared (first use in this function); did you mean ‘X86IOPortIn8’? case X86IOPortIn16: { /* inport 16 bits */ ^~~~~~~~~~~~~ X86IOPortIn8 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/ioport.c:103:10: error: ‘X86IOPortIn32’ undeclared (first use in this function); did you mean ‘X86IOPortIn16’? case X86IOPortIn32: { /* inport 32 bits */ ^~~~~~~~~~~~~ X86IOPortIn16 /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c: In function ‘decodeX86IOPTInvocation’: /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:195:21: error: ‘X86IOPageTableUnmap’ undeclared (first use in this function); did you mean ‘ARMPageTableUnmap’? if (invLabel == X86IOPageTableUnmap) { ^~~~~~~~~~~~~~~~~~~ ARMPageTableUnmap /home/maddthad/camkes-tutorials-manifest/kernel/src/arch/x86/object/iospace.c:201:21: error: ‘X86IOPageTableMap’ undeclared (first use in this function); did you mean ‘X86IOPageTableUnmap’? if (invLabel != X86IOPageTableMap ) { ^~~~~~~~~~~~~~~~~ X86IOPageTableUnmap make[1]: *** [kernel_final.s] Error 1 make: *** [kernel_elf] Error 2

2 1

Status of cmake support?
by Bruce Mitchener 30 Mar '18

30 Mar '18

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

2 1

Haskell and language support
by jonas.cl＠protonmail.com 28 Mar '18

28 Mar '18

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.

2 3

OPENSSL for seL4
by Daniel Wang 27 Mar '18

27 Mar '18

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

1 0

Booting BIN abort after elfloader
by Daniel Wang 26 Mar '18

26 Mar '18

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

1 0

3 open positions for Proof Engineers at Data61
by Gerwin.Klein＠data61.csiro.au 20 Mar '18

20 Mar '18

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/

1 0

Unable to Compile Tutorial 2 Exercises
by Amit Goyal 20 Mar '18

20 Mar '18

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

2 1

Ethernet driver for TK-1
by Michal Podhradsky 20 Mar '18

20 Mar '18

Hello, I would like to use a similar Ethernet driver component as for x86 platforms here: https://github.com/seL4/camkes-vm/tree/master/components/Ethdriver But in the camkes-vm-arm repository I don't see an equivalent component: https://github.com/SEL4PROJ/camkes-arm-vm/tree/master/apps/vm/components Is the ethernet currently just passed to Linux? And if so, what would entail making a new driver etc similar to x86 platforms? Regards Michal

2 1

VM and VMM Communication for ARM
by Daniel Wang 17 Mar '18

17 Mar '18

Hi all, I have a couple questions about VM an VMM communication for CAMKES-ARM-VM. Please correct me if I’m wrong. I found when VMM load Linux device it installs a vgic (install_linux_devices() -> vm_install_vgic()) But how exactly a interrupt caused by VM is distributed from GIC to VGIC (kernel to VMM)? I saw that we can register a virq to the VGIC (vm_virq_new()), but I’m not sure when a interrupt is generated how it is passed to the VGIC. Second, I found that we can install virtual devices to VM (e.g. for Vchan communication). Seems like when Linux tries to access the mapped virtual device, a page_fault will generated. Does it create a interrupt? How does it processed by VMM code exactly? I found post_main() in the generated camkes.c file has 3 threads, case 3 runs the control thread -> run(), case 5 runs vevent interface vevent__run(), and case 7 runs fault hander. Does it triggers vevent? I’m not sure the control flow. Thank you in advance! Best Regards -Daniel Wang

1 0

irq_server example? Interrupt handlers?
by Richard Clark 14 Mar '18

14 Mar '18

Hi all! I have an Ethernet driver underneath an lwip implementation that I've gotten to run threaded tcpip. It happily passes messages back and forth and all around between half a dozen threads over a dozen ports all on localhost. Every once in a while though, it wants to send a packet to the outside world... this of course invokes the Ethernet driver, which rather annoyingly, is polled. I am looking for the proper way to convert my polled Ethernet driver to be interrupt-driven.... however the sel4 interrupt-handling/dispatching seems to escape my grasp and I could use a little help... It would appear that there is a mechanism to register a request to receive a message whenever an interrupt occurs? irq_server.c? Are there some nice simple examples out there? Is there an easier way perhaps? Thanks! Richard H. Clark ________________________________ 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.

2 1