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:
My colleague Alexander Boettcher already investigated the problem in
part, and might share his insights with you.
https://github.com.skalk | https://genode.org
When running sel4 in my processor it is taking too long to get this line
"firstname.lastname@example.org:65 Failed to allocate object of
size 268435456, error 1"
Is there any options to reduce allocation object size?
Or any other methods to speed up
CDAC, Trivandrum, India
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
Co-located with EuroS&P'19, KTH, Stockholm, June 2019
Dominique Bolignano, Prove & Run
Gernot Heiser, University of New South Wales
Frank Piessens, KU Leuven
Peter Sewell, University of Cambridge
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
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….
Mads Dam, KTH Royal Institute of Technology
David Nowak, CNRS and University of Lille
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
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
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?*
On Sat, 16 Feb 2019 at 06:57, Diego Alejandro Parra Guzman <
> 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
> 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:
>> 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
>> 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
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.
I would be highly pleased to have a piece of your opinion on this matter.
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.
Diego Alejandro Parra Guzmán
Estudiante de ingeniería electrónica
Universidad distrital FJC