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