- Devel - lists.sel4.systems

some questions about camkes-manifest
by yadong.li 25 Mar '19

25 Mar '19

hi, I have some questions about camkes-manifest 1、I find the libsdhcdrivers in /projects/projects_libs of the project. But where can I find the superset of these libs by git? I can't find the maintenance branch about libsdhcdrivers (like 'seL4_libs' ) in https://github.com/seL4 2、I can't find who use the function of libsdhcdrivers, what is the plan of the lib ? Is there some demo using sdhc ? Thank you very much

2 1

Hello. Nice to meet you. I’m MK
by KIM MK 11 Mar '19

11 Mar '19

Hello Micro kernel develper I’m MK. Nice to meet u. I’ll research and commit ARMv8 and virtualization in Sel4 你好。谢谢。 반갑습니다 Thank you BR， MK Sent from my iPhone

1 0

How to (and how not to) use seL4 IPC
by Gernot.Heiser＠data61.csiro.au 11 Mar '19

11 Mar '19

Folks might be interested in this blog: https://microkerneldude.wordpress.com/2019/03/07/how-to-and-how-not-to-use-… Gernot

2 3

ENTROPY 2019: Second Call for Papers
by Toby.Murray＠data61.csiro.au 20 Feb '19

20 Feb '19

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… 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…. 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

1 0

Re: [seL4] port SeL4 to renesas rcar-H3 development board
by Diego Alejandro Parra Guzman 19 Feb '19

19 Feb '19

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 < daparrag(a)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 < > daparrag(a)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? >> >> I followed the tutorials and so one. But I will appreciate if you have >> something guidelines to start. >> >> Thank you >> >> BR >> Diego. >> -- >> Diego Alejandro Parra Guzmán >> Estudiante de ingeniería electrónica >> Universidad distrital FJC >> > > > -- > Diego Alejandro Parra Guzmán > Estudiante de ingeniería electrónica > Universidad distrital FJC > -- Diego Alejandro Parra Guzmán Estudiante de ingeniería electrónica Universidad distrital FJC

2 3

sel4 at Developers Conference 2019
by Jheengut Pritvi 14 Feb '19

14 Feb '19

Hi, I have been following and keeping track of the development of sel4 for more than 3 years. Unfortunately, I have not been able to install sel4 on my odroid U3 and it also has been a long time that I have built and run sel4. I am also part of the organising team of the Developers Conference since 2015 and this year is the fifth edition held in the Voila hotel and Flying Dodo in Bagatelle in the Republic of Mauritius. This year, I have a session about sel4. https://sessionize.com/s/jheengut/an_introduction_to_the_sel4_microke/21360 I would be highly pleased to have a piece of your opinion on this matter. Cheers Pritvi Jheengut

1 0

port SeL4 to renesas rcar-H3 development board
by Diego Alejandro Parra Guzman 14 Feb '19

14 Feb '19

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? I followed the tutorials and so one. But I will appreciate if you have something guidelines to start. Thank you BR Diego. -- Diego Alejandro Parra Guzmán Estudiante de ingeniería electrónica Universidad distrital FJC

4 3

Poll for Separation Kernel (microkernel) CC Protection Profile
by Holger Blasum 20 Jan '19

20 Jan '19

Hello seL4 devel, microkernel-based systems can be used as separation kernels[*] for security. At the moment there is a poll on input for a Common Criteria for Information Technology Security (CC) separation kernel protection profile draft, organized by a certMILS.eu colleague from Rostock Univ, at https://evasys.uni-rostock.de/evasys/online.php?p=ccuf-sk-wg The idea is to have a base protection profile (PP) that all players can agree with and to specify additional functionality as add-ons to the PP (e.g., in the form of PP modules). The questionnaire is an opportunity to provide early feedback. Note that there are no mandatory questions, i.e. you can freely move around / you can leave any question unanswered - the only condition for your feedback be submitted to the collection system is that you go to the last page and use the submit button there. We invite feedback via that poll by end of this week. If, beyond the questionnaire, you want to join the Common Criteria User's Forum separation kernel working group, or anyone would like to have more time, just let me know by answering to this email. [*] https://en.wikipedia.org/wiki/Multiple_Independent_Levels_of_Security Best, -- Holger Blasum, SYSGO

1 1

seL4 Training and ARMv8 virtualization release
by Robert VanVossen 18 Jan '19

18 Jan '19

All, We at DornerWorks wanted to let the seL4 community know about some seL4 training opportunities that we will be providing on behalf of the seL4 Center of Excellence (CoE). First, we will be providing an introductory webinar that provides an overview and explains the basics of seL4. Webinar: Intro to seL4 Thursday, February 7 11 a.m. EST Register Now: https://dornerworks.clickmeeting.com/intro-to-sel4/register Second, a more advanced two day training will take place on March 7th. This is a paid training that will provide information on seL4, libraries, CAmkES, the proof, and supported platforms. The training will also have hands-on labs that will include configuring CAmkES applications, debugging seL4 applications with GDB, and writing an HTTP server application to serve as a real life example. You can see more information and sign up here: https://www.sae.org/learn/content/c1874/ Finally, we wanted to let people know about our release of our ARMv8 virtualization feature. We recently received approval to release these features to the public. We have a press release providing additional details, a link to the code, and user instructions: https://dornerworks.com/news/new-commits-to-open-source-sel4. Currently, the release is on the DornerWorks github and based on an earlier version of seL4 and its libraries. We are working with Data61 to update to the latest versions and then mainline into the Data61 repositories. This may take some time as we integrate our ARMv8 virtualization code with Data61's ARMv8 virtualization code. Cheers, Robbie VanVossen DornerWorks, Ltd.

1 0

ENTROPY 2019: Call for Papers
by Toby Murray 13 Jan '19

13 Jan '19

************************************************************************** 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 Co-located with EuroS&P'19, KTH, Stockholm, 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. INVITED SPEAKERS (to be extended) Frank Piessens, KU Leuven Peter Sewell, Univ. Cambridge IMPORTANT DATES Paper submission: March 11 2019 Author notification: April 10, 2019 Camera-ready versions: April 22, 2019 (strict) Workshop: 16 June 2019 SUBMISSION AND PUBLICATION There are two categories of submissions: 1. Regular papers describing fully developed work and complete results (8 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://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 -- Toby Murray, DPhil (University of Oxford) Senior Lecturer, School of Computing and Information Systems University of Melbourne http://people.eng.unimelb.edu.au/tobym/ toby.murray(a)unimelb.edu.au

1 0