Re: [seL4] port SeL4 to renesas rcar-H3 development board
Hi yayan. Thank you for your reply. Sorry for ask but I just have few more questions: *sel4-tools* - the elfloader-tool that is used to loads the arm kernel seams a bit confused for me. I suppose that it just generate a .elf file representing the kernel it is right? - I don't think they are related. But In which way the elfloader-tool interacts with U-boot? - The sel4-tools/ CMakeList.txt :165 has a line *"if (ElfloaderImageEFI) "*. I'm not sure if it is supported by the U-boot within the rensas H3ULCB board. In case that not. what I should do ? GIC: The renesas H3ULCB has a GIC-400 unit and seams it is no supported by SeL4. may I wrong? - if it is not supported, I should implemented in order to make Sel4 works in this board? - how it is used by the seL4 kernel? you can check up my work here: https://github.com/Daparrag/seL4/tree/rcar_h3sel4 thank you. On Mon, 18 Feb 2019 at 23:48, wrote: > Hi Diego, > > > core_entry_head and init_cpus are for bringing up secondary cores. If you > want to utilise more than one core, you need to implement the functions. I > am not sure about your board, but PSCI (power state coordination > interface) is usually used to bring up secondary cores. Please have a look > at the TX1 plat. Your SoC manual should also explain how to bring up > secondary cores. > > > The elfloader assumes the the uart port for printf is initialised by the > uboot or other boot loaders. Otherwise, the elfloader needs to set up the > port. > > > Hope this can help a bit. > > > > Regards, > > Yanyan > > > -- > *From:* Devel on behalf of Diego Alejandro > Parra Guzman > *Sent:* Monday, February 18, 2019 6:11 PM > *To:* devel@sel4.systems > *Subject:* Re: [seL4] port SeL4 to renesas rcar-H3 development board > > Hi guys !!! > > Thank you for your quick replay. > > I'm try to port Sel4 kernel to the* renesas H3 ULCB* board with two > clusters (ARM57),(ARM53) each one with 4 cores > > I just have couple of questions regarding with the elf loader in > sel4-tools: > > there is some files in* elfloader-tool/plat/** those are intended to > initialize the CPU and the UART on the platform. In there, there is a > function written in assembly called *core_entry_head* and a function > *init_cpus*implemented in smp.c file. > *Could you please explain me a little bit what is the purpose of these > functions ? * > > In the case of *init_cpus* where is suppose to be that information? I > means, I should reference the ARM57 or ARM53 cpu manual or maybe to the > boot section in the SoC manual. > > > from the other hand the *renesas H3 ULCB* doesn't have a physical UART > port. Instead, it has an Serial Communication Interface with FIFO (SCIF) > that can be configure properly to be compatible with *UART* interfaces. > The point is that I'm using this interface in order to implement the > * __fputc()* function following the one implemented in sys_fput.c file. > Unfortunately, I don't understand why in your implementation there is > not an initialization for the *UART. could you tell me why not?* > > Thank you. > > best regards > > On Sat, 16 Feb 2019 at 06:57, Diego Alejandro Parra Guzman < > dapar...@correo.udistrital.edu.co> wrote: > >> Hi guys !!! >> >> Thank you for your quick replay. >> >> I'm try to port Sel4 kernel to the* renesas H3 ULCB* board with two >> clusters (ARM57),(ARM53) each one with 4 cores >> >> I just have couple of questions regarding with the elf loader in >> sel4-tools: >> >> there is some files in* elfloader-tool/plat/** those are intended to >> initialize the CPU and the UART on the platform. In there, there is a >> function written in assembly called *core_entry_head* and a function >> *init_cpus*implemented in smp.c file. >> *Could you please explain me a little bit what is the purpose of these >> functions ? * >> >> In the case of *init_cpus* where is suppose to be that information? I >> means, I should reference the ARM57 or ARM53 cpu manual or maybe to the >> boot section in the SoC manual. >> >> >> from the other hand the *renesas H3 ULCB* doesn't have a physical UART >> port. Instead, it has an Serial Communication Interface with FIFO (SCIF) >> that can be configure properly to be compatible with *UART* interfaces. >> The point is that I'm using this interface in order to implement the >> * __fputc()* function following the one implemented in sys_fput.c >> file. Unfortunately, I don't understand why in your implementation >> there is not an initialization for the *UART. could you tell me why >> not?* >> >> Thank you. >> >> best regards >> >> On Wed, 13 Feb 2019 at 15:21, Diego Alejandro Parra Guzman < >> dapar...@correo.udistrital.edu.co> wrote: >> >>> >>> Hi, >>> >>> I'm new with seL4 kernel and I would like to port it to the ARM-based >>> renesas rcar-H3 board >>> >>> I would like to ask of you have a development manual that i can follow >>> with some basics about how to do it? >>> >>
Re: [seL4] port SeL4 to renesas rcar-H3 development board
Hi Diego, The file type of the elfloader can be efi, elf, binary, or uimage. The seL4 kernel and payload applications are bundled in the elfloader file; and the elfloader sets up the environment, loads the kernel and application into the correct memory regions, and jumps to the kernel entry point. The uboot loads the elfloader into memory (e.g. tftpboot) and jumps to the entry point of the elfloader. The uboot should support ELF or binary, and you can build the elfloader as an ELF or binary file. There is a configuration option for the output file format. GIC-400 is supported by the seL4. However, if your board's bootloader loads the elfloader in secure world, maybe you need to configure the security-related settings of the GIC controller. The GICv2 architecture specification is a good reference. Thanks for sharing the link, and just let us know if you have more questions. Regards, Yanyan From: Diego Alejandro Parra Guzman Sent: Wednesday, February 20, 2019 3:45 AM To: Shen, Yanyan (Data61, Kensington NSW); devel@sel4.systems Subject: Re: [seL4] port SeL4 to renesas rcar-H3 development board Hi yayan. Thank you for your reply. Sorry for ask but I just have few more questions: sel4-tools * the elfloader-tool that is used to loads the arm kernel seams a bit confused for me. I suppose that it just generate a .elf file representing the kernel it is right? *I don't think they are related. But In which way the elfloader-tool interacts with U-boot? * The sel4-tools/ CMakeList.txt :165 has a line "if (ElfloaderImageEFI) ". I'm not sure if it is supported by the U-boot within the rensas H3ULCB board. In case that not. what I should do ? GIC: The renesas H3ULCB has a GIC-400 unit and seams it is no supported by SeL4. may I wrong? * if it is not supported, I should implemented in order to make Sel4 works in this board? * how it is used by the seL4 kernel? you can check up my work here: https://github.com/Daparrag/seL4/tree/rcar_h3sel4 thank you. On Mon, 18 Feb 2019 at 23:48, mailto:yanyan.s...@data61.csiro.au>> wrote: Hi Diego, core_entry_head and init_cpus are for bringing up secondary cores. If you want to utilise more than one core, you need to implement the functions. I am not sure about your board, but PSCI (power state coordination interface) is usually used to bring up secondary cores. Please have a look at the TX1 plat. Your SoC manual should also explain how to bring up secondary cores. The elfloader assumes the the uart port for printf is initialised by the uboot or other boot loaders. Otherwise, the elfloader needs to set up the port. Hope this can help a bit. Regards, Yanyan From: Devel on behalf of Diego Alejandro Parra Guzman mailto:dapar...@correo.udistrital.edu.co>> Sent: Monday, February 18, 2019 6:11 PM To: devel@sel4.systems Subject: Re: [seL4] port SeL4 to renesas rcar-H3 development board Hi guys !!! Thank you for your quick replay. I'm try to port Sel4 kernel to the renesas H3 ULCB board with two clusters (ARM57),(ARM53) each one with 4 cores I just have couple of questions regarding with the elf loader in sel4-tools: there is some files in elfloader-tool/plat/* those are intended to initialize the CPU and the UART on the platform. In there, there is a function written in assembly called core_entry_head and a function init_cpusimplemented in smp.c file. Could you please explain me a little bit what is the purpose of these functions ? In the case of init_cpus where is suppose to be that information? I means, I should reference the ARM57 or ARM53 cpu manual or maybe to the boot section in the SoC manual. from the other hand the renesas H3 ULCB doesn't have a physical UART port. Instead, it has an Serial Communication Interface with FIFO (SCIF) that can be configure properly to be compatible with UART interfaces. The point is that I'm using this interface in order to implement the __fputc() function following the one implemented in sys_fput.c file. Unfortunately, I don't understand why in your implementation there is not an initialization for the UART. could you tell me why not? Thank you. best regards On Sat, 16 Feb 2019 at 06:57, Diego Alejandro Parra Guzman mailto:dapar...@correo.udistrital.edu.co>> wrote: Hi guys !!! Thank you for your quick replay. I'm try to port Sel4 kernel to the renesas H3 ULCB board with two clusters (ARM57),(ARM53) each one with 4 cores I just have couple of questions regarding with the elf loader in sel4-tools: there is some files in elfloader-tool/plat/* those are intended to initialize the CPU and the UART on the platform. In there, there is a function written in assembly called core_entry_head and a function init_cpusimplemented in smp.c file. Could you please explain me a little bit what is the purpose of these functions ? In the case of init_cpus where i
[seL4] ENTROPY 2019: Second Call for Papers
NEW: two more invited speakers ** Second Call for papers — ENTROPY 2019 ENabling TRust through Os Proofs … and beYond Second International workshop on the use of theorem provers for modelling and verification at the hardware-software interface https://protect-au.mimecast.com/s/h5JtCjZroMFQkjkKFW-1Th?domain=entropy2019.sciencesconf.org Co-located with EuroS&P'19, KTH, Stockholm, June 2019 ** INVITED SPEAKERS Dominique Bolignano, Prove & Run Gernot Heiser, University of New South Wales Frank Piessens, KU Leuven Peter Sewell, University of Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 AIM AND SCOPE Low level software such as kernels and drivers, along with the hardware this software runs on, is critical for application security. In contrast with user applications, OS kernel software runs in privileged CPU mode and is thus highly critical. Large projects such as seL4, VeriSoft, CertiKoS and Prosper have invested considerable resources in developing formally verified systems such as hypervisors and microkernels, supplying proofs that they satisfy critical properties. Such proofs are delicate in terms of the scale and complexity of real systems, the models used in performing the proof search, and the relations between the two, which recent vulnerabilities such as Spectre and Meltdown have shown to be a highly non-trivial issue. The purpose of this workshop is to share, compare and disseminate best practices, tools and methodologies to verify OS kernels, also setting the stage for future steps in the direction of fully verified systems, dealing with issues related to modelling, model validation, and large proof maintenance through system evolution. On one hand, we need to make low-level proofs more scalable, modular and cost-effective. On the other hand, once certified systems are available, preservation and maintenance of their proofs of validity become key questions. The goal of the ENTROPY workshop is to provide a forum for researchers and practitioners in this space, linking operating systems, formal methods, and hardware architecture, interested in system design as well as machine verified mathematical proofs using proof assistants such as Coq, Isabelle and HOL4. This will be the second edition of the ENTROPY workshop series. The first workshop was organised by the Pip Development Team at University of Lille in 2018. TOPICS OF INTEREST Specific topics include, but are not limited to: * Verified kernels and hypervisors * Verified security architectures and models * Tools and frameworks for hardware security analysis * Tools and frameworks for security analysis * Formal hardware models and model validation techniques * Theorem prover based tools and frameworks for verification of low level code * Combinations of static analysis and theorem proving * Theories and techniques for compositional security analysis * Case studies and industrial experience reports * Proof maintenance techniques and problems * Compositional models and verification techniques * Proof oriented design The aim of the workshop is to stimulate innovation and active exchange of ideas, so position papers, work-in-progress and industrial experience submissions are welcome. SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (10 pages, references included, IEEE format) 2. Short papers, position papers, industry experience reports, work-in-progress submissions (4 pages, references included, IEEE format) All papers should be in English and describe original work that has not been published or submitted elsewhere. The submission category should be clearly indicated. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in IEEE Xplore in a companion volume to the regular EuroS&P proceedings. For formatting and submission instructions see https://protect-au.mimecast.com/s/h5JtCjZroMFQkjkKFW-1Th?domain=entropy2019.sciencesconf.org. PROGRAM CHAIRS Mads Dam, KTH Royal Institute of Technology David Nowak, CNRS and University of Lille PROGRAM COMMITTEE Christoph Baumann, Ericsson AB Gustavo Betarte, Univ. de la República, Uruguay David Cock, ETH Zurich Mads Dam, KTH Royal Institute of Technology (chair) Anthony Fox, ARM Deepak Garg, MPI Saarbrucken Ronghui Gu, Columbia University Samuel Hym, Univ. Lille Thomas Jensen, INRIA and Univ. Rennes Toby Murray, Univ. Melbourne David Nowak, CNRS & Univ. Lille (chair) Vicente Sanchez-Leighton, Orange Labs Thomas Sewell, Chalmers ___ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
