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
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
Hey there,
are some of you going to the 35C3 congress in Leipzig, Germany?
I'm trying to understand seL4 and get into developing for it.
I'd love to talk to someone if anyone's around.
Best regards and merry Christmas,
Daniel
P.S. My "home" is the Selfnet assembly
Hello Kent,
Thanks for the reply :) The moving/copying was to demonstrate the
differences between the tutorial and the solution. Creating and completing
a new copy of the tutorial doesn't give the expected results either.
My understanding is, when we run "./init --tut hello-camkes-1", the build
directory is immediately built off the incomplete tutorial, hence it's
missing client.instance.bin.dir etc. This isn't fixed when we complete the
tutorial and ninja. Hence when someone goes through the tutorial, it
doesn't give the expected "Starting the client". If this is the case, could
you point me to where I can rectify this?
On an separate note, I'm experiencing the same issues as
https://sel4.systems/pipermail/devel/2018-October/002221.html. The simulate
script exists, but qemu (at least 2.5.0+) seems to only allow
"kernel-irqchip=on|off", not split. May I know which version of qemu we
should be using?
Regards,
Leow Wei Xiang
On Tue, Dec 18, 2018 at 2:10 PM <Kent.Mcleod(a)data61.csiro.au> wrote:
> Hi,
>
>
> Renaming the source directory and the build directories aren't supported
> as CMake and Ninja rely on the absolute and relative paths remaining
> consistent. You are still able to copy the contents of the source
> directory from the solution into the source directory of the non solution
> and use the same build directory. The reason why you only see ...Booting all
> finished is because when the tutorial starts, there are no components
> defined in the camkes assembly, so no components will be loaded by the
> initial task. This is why you don't see any output.
>
>
> I don't believe there is an issue, but let me know if I have misunderstood
> what you meant.
>
>
> Kind regards,
>
> Kent.
>
>
>
> ------------------------------
> *From:* Devel <devel-bounces(a)sel4.systems> on behalf of Wei Xiang Leow <
> leowweixiang1991(a)gmail.com>
> *Sent:* Tuesday, December 18, 2018 4:42 PM
> *To:* devel(a)sel4.systems
> *Subject:* [seL4] CAmkES tutorial build system
>
> Hello, there seem to be issues with the tutorial build system, at least
> for CAmkES tutorial 1. After adding the necessary details and running, I
> get "...Booting all finished", no further messages. The solution runs fine,
> I get "Starting the client" etc.
>
> Made fresh copies of the tutorial and solution, and overwrote the
> tutorial's files with the solution's. Diff shows that only .tute_config
> (--solution) and the .md files differ. Diff on the "_build" folders shows
> multiple differences. I assume there is an issue there?
>
> mkdir tutorial; mkdir solution
> ./init --tut hello-camkes-1
> mv hello-camkes-1 tutorial
> mv hello-camkes-1_build tutorial
> ./init --tut hello-camkes-1 --solution
> mv hello-camkes-1 solution
> mv hello-camkes-1_build solution
> cp solution/hello-camkes-1/hello-1.camkes
> tutorial/hello-camkes-1/hello-1.camkes
> diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1
> ############################
> Files tutorial/hello-camkes-1/hello-camkes-1.md and
> solution/hello-camkes-1/hello-camkes-1.md differ
> Files tutorial/hello-camkes-1/.tute_config and
> solution/hello-camkes-1/.tute_config differ
> ############################
>
> diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build
> ############################
> Files tutorial/hello-camkes-1_build/build.ninja and
> solution/hello-camkes-1_build/build.ninja differ
> Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and
> solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ
> Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and
> solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ
> Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and
> solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ
> Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and
> solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ
> Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles:
> client.instance.bin.dir
> Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles:
> echo.instance.bin.dir
> Files
> tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes
> and
> solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes
> differ
> Files
> tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md
> and
> solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md
> differ
> Files tutorial/hello-camkes-1_build/rules.ninja and
> solution/hello-camkes-1_build/rules.ninja differ
> ############################
>
> cp -r tutorial/hello-camkes-1 hello-camkes-1
> cp -r tutorial/hello-camkes-1_build hello-camkes-1_build
> cd hello-camkes-1_build
> ninja
> ./simulate
> ############################
> ...
> Booting all finished, dropped to user space
> ############################
>
> <another terminal>
> rm -r hello-camkes-1
> rm -r hello-camkes-1_build
> cp -r solution/hello-camkes-1 hello-camkes-1
> cp -r solution/hello-camkes-1_build hello-camkes-1_build
> cd hello-camkes-1_build
> ninja
> ./simulate
> ############################
> ...
> Booting all finished, dropped to user space
> Starting the client
> -------------------
> Component echo saying: hello world
> After the client
> ############################
>
> Regards,
> Leow Wei Xiang
>
Hello, there seem to be issues with the tutorial build system, at least for
CAmkES tutorial 1. After adding the necessary details and running, I get
"...Booting all finished", no further messages. The solution runs fine, I
get "Starting the client" etc.
Made fresh copies of the tutorial and solution, and overwrote the
tutorial's files with the solution's. Diff shows that only .tute_config
(--solution) and the .md files differ. Diff on the "_build" folders shows
multiple differences. I assume there is an issue there?
mkdir tutorial; mkdir solution
./init --tut hello-camkes-1
mv hello-camkes-1 tutorial
mv hello-camkes-1_build tutorial
./init --tut hello-camkes-1 --solution
mv hello-camkes-1 solution
mv hello-camkes-1_build solution
cp solution/hello-camkes-1/hello-1.camkes
tutorial/hello-camkes-1/hello-1.camkes
diff -rq tutorial/hello-camkes-1 solution/hello-camkes-1
############################
Files tutorial/hello-camkes-1/hello-camkes-1.md and
solution/hello-camkes-1/hello-camkes-1.md differ
Files tutorial/hello-camkes-1/.tute_config and
solution/hello-camkes-1/.tute_config differ
############################
diff -rq tutorial/hello-camkes-1_build solution/hello-camkes-1_build
############################
Files tutorial/hello-camkes-1_build/build.ninja and
solution/hello-camkes-1_build/build.ninja differ
Files tutorial/hello-camkes-1_build/CMakeFiles/CMakeOutput.log and
solution/hello-camkes-1_build/CMakeFiles/CMakeOutput.log differ
Files tutorial/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt and
solution/hello-camkes-1_build/CMakeFiles/TargetDirectories.txt differ
Files tutorial/hello-camkes-1_build/hello-camkes-1/ast.pickle and
solution/hello-camkes-1_build/hello-camkes-1/ast.pickle differ
Files tutorial/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake and
solution/hello-camkes-1_build/hello-camkes-1/camkes-gen.cmake differ
Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles:
client.instance.bin.dir
Only in solution/hello-camkes-1_build/hello-camkes-1/CMakeFiles:
echo.instance.bin.dir
Files
tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes
and
solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-1.camkes
differ
Files
tutorial/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md
and
solution/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/old/hello-camkes-1.md
differ
Files tutorial/hello-camkes-1_build/rules.ninja and
solution/hello-camkes-1_build/rules.ninja differ
############################
cp -r tutorial/hello-camkes-1 hello-camkes-1
cp -r tutorial/hello-camkes-1_build hello-camkes-1_build
cd hello-camkes-1_build
ninja
./simulate
############################
...
Booting all finished, dropped to user space
############################
<another terminal>
rm -r hello-camkes-1
rm -r hello-camkes-1_build
cp -r solution/hello-camkes-1 hello-camkes-1
cp -r solution/hello-camkes-1_build hello-camkes-1_build
cd hello-camkes-1_build
ninja
./simulate
############################
...
Booting all finished, dropped to user space
Starting the client
-------------------
Component echo saying: hello world
After the client
############################
Regards,
Leow Wei Xiang
Is it (or would it be) possible to specify more than the single root server
module and have seL4 create virtual addresses, cap. Spaces, threads (leaving
them suspended) and pass the information about these modules to the root
server? In this way it would be possible to have GRUB load a multi-server
seL4 environment.
Thanks,
Dave
Good day everyone!
I want to try to port sel4 to mips. I will be grateful if you give me the
literature that will help me understand the structure of sel4 and its
logical interaction with arm/riscv.
Hi All,
I am using Ubuntu 16.04 on 64 Bit, i7 machine and running Camkes
Cross-VM communication tutorial available at:
https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html
I am able to build the system properly but when I run the system, I get
the following error:
---------------------------------------------------------------------------------------------------------------------------------
Creating dataport node /dev/camkes_reverse_src
Creating dataport node /dev/camkes_reverse_dest
Allocating 8192 bytes for /dev/camkes_reverse_src
dataport_map_guest@cross_vm_dataport.c:25 Dataport guest size and host
size are different (8192 and 4096)
dataport_vmcall_handler@cross_vm_dataport.c:75 Failed to map dataport
into guest
VM_FATAL_ERROR ::: vmexit handler return error
vmm_print_guest_context:27 | ================== GUEST OS CONTEXT
=================
vmm_print_guest_context:30 | exit info : reason 0x12 qualification
0x0 instruction len 0x3 interrupt info 0x0 interrupt error 0x0
vmm_print_guest_context:32 | guest physical 0x0 rflags
0x286
vmm_print_guest_context:34 | guest interruptibility 0x0
control entry 0x34
vmm_print_guest_context:37 | eip 0xd881714a
vmm_print_guest_context:39 | eax 0x 1 ebx 0x 1
ecx 0x 1
vmm_print_guest_context:41 | edx 0x16a42000 esi 0x 2000
edi 0x 10
vmm_print_guest_context:43 | ebp 0xd6b17f0c
vmm_print_guest_context:45 | cr0 0x80050033 cr3 0x16b1e000 cr4
0x2680
---------------------------------------------------------------------------------------------------------------------------------
I tried troubleshooting it a bit and changed the file:
~/camkes_vm_com/projects/vm-linux/camkes-linux-artifacts/camkes-linux-init-scripts/buildroot_init/camkes_init
as follows:
Earlier: dataport_init /dev/camkes_reverse_src 8192
/dev/camkes_reverse_dest 8192
Changed: dataport_init /dev/camkes_reverse_src 4096
/dev/camkes_reverse_dest 4096
But this also does not work.
Please suggest.
--
Thanks and Regards,
Amit Goyal
Patents possibly gone wrong.
https://www.eff.org/deeplinks/2018/11/stupid-patent-month-patent-using-math…
Claim 1 of the patent describes creating mathematical “axioms”—formal
mathematical statements—that describe a computerized trading forum. The
patented method then describes analyzing, with a “computer assessment
system … the mathematical axioms that describe the operation of the trading
forum.” In other words, the patent describes using formal proofs to check
for bugs in a “computerized trading forum.” It’s formal verification—just
applied to the financial services industry.
--
T o m M i t c h e l l