Devel January 2019

devel@sel4.systems

6 participants
7 discussions

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

TLB issue
by Stefan Kalkowski 15 Nov '19

15 Nov '19

Dear sel4 community, yesterday I've started to develop a low-level platform test to stress several multi-processor aspects on top of the Genode API. Thereby, I've recognized that on sel4/x86_64 the TLB is practically not always cleaned properly in SMP systems. The test spawns threads of one protection domain on each available cpu. Each thread accesses one of the first words of a shared dataspace. Afterwards the main thread on CPU 0 detaches and destroys the dataspace. Unfortunately, the threads on other CPUs still successfully access the corresponding memory instead of triggering a fault. To be able to reproduce the problem, you might investigate the simple test case here: https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7… My colleague Alexander Boettcher already investigated the problem in part, and might share his insights with you. Best regards Stefan -- Stefan Kalkowski Genode labs https://github.com.skalk | https://genode.org

3 3

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

21 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 19 Jan '19

19 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

Running 2 VM Linux on Camkes
by Amit Goyal 09 Jan '19

09 Jan '19

Hi, I am using Ubuntu 16.04 on 64 Bit, i7 machine and following CAmkES x86 VM instructions available at: https://docs.sel4.systems/CAmkESVM I am able to successfully run single guest vm. I am now trying to run 2 guest vms at the same time. For this, I changed a) minimal.camkes as follows: -------------------------------------------------------------------------------------------------------------------------------- #ifdef HAVE_AUTOCONF #include <autoconf.h> #endif import <VM/vm.camkes>; #include <configurations/vm.h> #define VM_GUEST_CMDLINE "earlyprintk=ttyS0,115200 console=ttyS0,115200 i8042.nokbd=y i8042.nomux=y \ i8042.noaux=y io_delay=udelay noisapnp pci=nomsi debug root=/dev/mem" component Init0 { VM_INIT_DEF() } component Init1 { VM_INIT_DEF() } assembly { composition { VM_COMPOSITION_DEF() VM_PER_VM_COMP_DEF(0) VM_PER_VM_COMP_DEF(1) } configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) VM_PER_VM_CONFIG_DEF(1) vm0.simple_untyped23_pool = 20; vm0.heap_size = 0x2000000; vm0.guest_ram_mb = 128; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = "bzimage"; vm0.kernel_relocs = "bzimage"; vm0.initrd_image = "rootfs.cpio"; vm0.iospace_domain = 0x0f; vm1.simple_untyped23_pool = 20; vm1.heap_size = 0x2000000; vm1.guest_ram_mb = 128; vm1.kernel_cmdline = VM_GUEST_CMDLINE; vm1.kernel_image = "bzimage"; vm1.kernel_relocs = "bzimage"; vm1.initrd_image = "rootfs.cpio"; vm1.iospace_domain = 0x0f; } } --------------------------------------------------------------------------------------------------------------------------------- b) CMakeLists.txt as follows: --------------------------------------------------------------------------------------------------------------------------------- cmake_minimum_required(VERSION 3.8.2) project(minimal) # Include CAmkES VM helper functions include("../../vm/camkes_vm_helpers.cmake") include("../../vm-linux/vm-linux-helpers.cmake") # Declare VM component: Init0 DeclareCAmkESVM(Init0) DeclareCAmkESVM(Init1) # Get Default Linux VM files GetDefaultLinuxKernelFile(kernel_file) GetDefaultLinuxRootfsFile(rootfs_file) # Decompress Linux Kernel image and add to file server DecompressLinuxKernel(extract_linux_kernel decompressed_kernel ${kernel_file}) AddToFileServer("bzimage" ${decompressed_kernel} DEPENDS extract_linux_kernel) # Add rootfs images into file server AddToFileServer("rootfs.cpio" ${rootfs_file}) # Initialise CAmkES Root Server with addition CPP includes DeclareCAmkESVMRootServer(minimal.camkes) --------------------------------------------------------------------------------------------------------------------------------- I can successfully build the system and 2 vm images are being created namely: vm0_group.bin, vm1_group.bin On running the system using: sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=true --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0" I get the following error: --------------------------------------------------------------------------------------------------------------------------------- <<seL4(CPU 0) [decodeUntypedInvocation/209 T0xffbfec00 "rootserver" @804853d]: Untyped Retype: Insufficient memory (1 * 4194304 bytes needed, 2048 bytes available).>> <<seL4(CPU 0) [decodeInvocation/542 T0xffbfec00 "rootserver" @804853d]: Attempted to invoke a null cap #0.>> create_objects@main.c:767 [Err seL4_InvalidCapability]: Untyped retype failed with unexpected error seL4 root server abort()ed Debug halt syscall from user thread 0xffbfec00 "rootserver" halting... Kernel entry via Unknown syscall, word: 523QEMU: Terminated --------------------------------------------------------------------------------------------------------------------------------- I have 2 doubts: a) Can someone suggest a possible way to get this running. b) Is it possible to see the 2 VMs running on separate terminals at the same time. -- Thanks and Regards, Amit Goyal

2 2

An RFC process for seL4
by Curtis.Millar＠data61.csiro.au 02 Jan '19

02 Jan '19

Hi Everyone, We are currently in the process of setting up and moving to a public Jira instance to manage many of our development issues. The first part of this move involves setting up a request for comments (RFC) process which will be implemented using a Jira project. You can find out more about the RFC process in the first RFC: https://sel4kernel.atlassian.net/browse/RFC-1 You are encouraged to leave feedback on the issue, but doing so requires that you are logged in with an Atlassian Cloud account. The introduction of a public issue tracker will allow us to better engage with our community, accept more contribution from outside the seL4 development team, and better communicate the ways in which we are changing and improving the seL4 ecosystem. In the long term, we hope to use this to track all of the major issues currently under development across the ecosystem, accept issues submitted by the public, and open issues up for members of the greater community to work on. The issue tracker will initially be used as the basis of the RFC process, which will allow for the community to get involved with larger changes to the ecosystem. Many of the details of the process can only be clearly resolved as it becomes used more regularly as part of ongoing development, so much of how it works is still to be determined. We are hoping to finalise this process at the beginning of the new year before we use it to present a number of other changes we have been planning so we can get your feedback before their design and implementation is finalised. This new issue tracker and RFC process are just part of greater ongoing changes on which we are working to grow the community and to increase its involvement. We wish you all a happy holiday season and look forward to the start of a new year with seL4. Cheers, Curtis

2 2

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel January 2019