Hello all,
I recently spent a lot of time getting the camkes-vm-linux tutorial to
work, because it is the only example I could find of compiling a kernel
module for the linux vm as a part of the camkes build process.
Unfortunately, the kernel module doesn't seem to work. For more
information, see the previous email chain as well as
https://github.com/NeisesResearch/vm_measure/wiki/Building-the-camkes_vm_li…
.
In lieu of doing things the right way, I believe I could compile a kernel
module for the linux kernel that is provided as part of the camkes build
system. I believe this is how the introspect-app accomplishes its work.
However, I need to have the exact kernel and exact configuration in order
to compile the kernel module correctly.
Can anyone point me to the correct kernel version and configuration, so
that I can target the provided linux kernel for module compilation?
Or if there's a better way to get a kernel module in there, please let me
know.
Cheers,
Michael Neises
Hello seL4-devs,
I am working with seL4 running as a hypervisor with multiple VMs. I am aware of vchan (inactive) and VirtIO Net as mechanisms for inter-VM communication on top of seL4. However, I am looking to have a shared memory inter-VM communication between my VMs. Is there a well-maintained mechanism with shared memory and notifications for inter VM communication?
I have been trying to create a CAmkES example with dataport and I found out this "seL4SharedDataWithCaps" CAmkES connector for connecting dataport interfaces (https://github.com/seL4/global-components/issues/8):
connection seL4SharedDataWithCaps sharedMem(from vm0.dummy_port, to vm0.buff, to vm1.buff);
The "to" side of the connection is supposed to give capabilities to both vmm0 and vmm1 (workaround proposed in the link above). How to use those capabilities to map "buff" into Linux guest address space?
Ideally, I would like to access that "buff" from Linux kernel without VMM intervention.
Thank you in advance.
Best,
Everton
Hi,
I am doing a feasibility study to ascertain whether Linux can be deployed
to a seL4 kernel running on a Pi 4B with 8GB of memory. I have seen that
there is explicit support for the Pi 3B, and that Linux can be run in a
virtual machine on top of seL4. But I did not see explicit support for a Pi
4B and the ability to have the Pi run the Linux VM. Please let me know if
this would be possible.
Thanks,
Drew Humphrey
Hi sel4-dev,
I was looking at the sel4utils/vspace
<https://github.com/seL4/seL4_libs/tree/master/libsel4utils> library and
noticed a mismatch in the number of pages allocated as per the two data
structures which keep track of the address space. Below I have laid out my
test setup, steps to reproduce and finally the exact questions.
In my test setup(which is copied from sel4test system), the root
task(driver) starts another process(test app) with its own address space
using sel4utils_spawn_process_v.(inside basic_run_test). Then in the root
task we do a walk of the child task's address space structures maintained
by sel4utils/vspace library.
The 2 structures I am walking are:
- The linked list of reservations: source-code
<https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4util…>:
Here we traverse a linked list and count the number of pages which have
been allocated based on the size of each reservation.
- The tree which keeps the caps of pages mapped so far(sort of like the
shadow page table). source-code
<https://github.com/seL4/seL4_libs/blob/master/libsel4utils/include/sel4util…>.
Here we traverse the multi-level shadow page table hierarchy to count the
pages the library has mapped.
I find that the number of pages I get from the 2 walks are not equal. I
understand that neither of the above are reflective of the true state of
the address space as that is only known to the kernel. So, it is simply
possible that in some code path, the library inserts an entry in to one of
the structures and not the other. I have used Intel 32-bit platform to keep
the page table structure simple for this query.
Here is the code to walk the vspace(source code)
<https://github.com/sid-agrawal/seL4_libs/blob/0d37c61f89dc335a5905f5625be31…>
:
int sel4utils_walk_vspace(vspace_t *vspace, vka_t *vka) {
sel4utils_alloc_data_t *data = get_alloc_data(vspace);
int index = 0;
sel4utils_res_t *sel4_res = data->reservation_head;
printf("===========Start of interesting output================\n");
printf("VSPACE_NUM_LEVELS %d\n", VSPACE_NUM_LEVELS);
/* walk all the reservations */
printf("\nReservations from sel4utils_alloc_data->reservation_head:\n");
while (sel4_res != NULL) {
long int sz = (sel4_res->end - sel4_res->start ) / (4 * 1024);
printf("\t[%d] %p->%p %lu pages malloced(%u)\n", index,
sel4_res->start, sel4_res->end, sz, sel4_res->malloced);
index++;
sel4_res = sel4_res->next;
}
int num_empty = 0;
int num_reserved =0;
int num_used =0;
int i = 0;
/* Walk all the page tables */
printf("\n\nIntel-32 Page Table Hierarcy from
sel4utils_alloc_data->top_level->table \n");
if (data->top_level)
{
for (i = 0; i < BIT(VSPACE_LEVEL_BITS); i++)
{
if (data->top_level->table[i] == RESERVED)
{
num_reserved++;
}
else if (data->top_level->table[i] == EMPTY)
{
num_empty++;
}
else
{
num_used++;
vspace_bottom_level_t *bottom_table =
(vspace_bottom_level_t *)data->top_level->table[i];
int L2_num_empty = 0;
int L2_num_reserved = 0;
int L2_num_used = 0;
int ii = 0;
for (ii = 0; ii < BIT(VSPACE_LEVEL_BITS); ii++)
{
uintptr_t cap = bottom_table->cap[ii];
if (cap == RESERVED)
{
L2_num_reserved++;
}
else if (cap == EMPTY)
{
L2_num_empty++;
}
else
{
L2_num_used++;
}
}
printf("PDE-Index(%d) \n\t" \
"NUM-PTE: %5d Empty: %5d \tReserved: %5d \tUsed: %5d\n",
i, ii, L2_num_empty, L2_num_reserved, L2_num_used, ii);
}
}
printf("===========Start of interesting output================\n");
}
return index;
}
Test Environment:
- The docker environment was setup using instruction from Using Docker
for seL4 <https://docs.sel4.systems/projects/dockerfiles/>.
- Qemu on Ubuntu 20.04 on 64 bit Intel machine
Below is the steps to reproduce the issue:
# Setup the project using a manifest repo.
# The structure of the project is borrowed from sel4test.
# The manifest points two repo's which are not original sel4 repos:
# - seL4_libs: The new walker helper is here, based on fork of sel4/sel4_libs
# - sel4-gpi: The test code is here. This is new repo.
mkdir sel4-gpi-system
cd sel4-gpi-system
repo init -u https://github.com/sid-agrawal/sel4-gpi-manifest -b refs/tags/v3.0
repo sync
container # Jump to the docker sel4 dev environment, omit if you do not care
mkdir build
cd build
../init-build.sh -DPLATFORM=ia32 -DSIMULATION=TRUE
ninja && ./simulate
# To exit Qemu
Ctrl-A X
The output from the test code is:
===========Start of interesting output================
VSPACE_NUM_LEVELS 2
Reservations from sel4utils_alloc_data->reservation_head:
[0] 0x10001000->0x10012000 17 pages malloced(1)
Intel-32 Page Table Hierarcy from sel4utils_alloc_data->top_level->table
PDE-Index(32)
NUM-PTE: 1024 Empty: 637 Reserved: 0 Used: 387
PDE-Index(64)
NUM-PTE: 1024 Empty: 1005 Reserved: 1 Used: 18
===========Start of interesting output================
The first part of the output shows the size of the reservation in number of
4KB pages which is 17 pages. We see that the vspace has only 1 reservation,
which is 17 pages long and is malloced. This itself is a little odd; I was
expecting multiple reservations for code, stack, ro-data etc.
The second part of the output shows the page directory and table entries.
Here we see that the 2 PDE are in use with a total of 405(18 + 387) PTEs
used in total.
So, my query is, why is there is a discrepancy in the number of pages used?
- Does the library allocate a bunch of pages(387) which do not belong to
any reservation?
- As far as the single page difference of 17 Vs 18, I think that can be
explained by the driver sharing a page with the test-app.
Besides the above, I have a couple of more general questions about the user
space virtual memory libraries in seL4.
- Why does the library need to mimic the PT hierarchy in user space?
- I am trying to implement fork in the sel4utils, mainly as an exercise.
Is there a helper function to duplicate an address space(let's say without
any COW)?
Thanks for your time. If there is some additional info I should be
providing while raising question on this forum do let me know.
Best,
Sid
Dear seL4 devs and community.
I am attempting to integrate seL4 into a new project of mine. To begin
setting up this project, I used
https://docs.sel4.systems/projects/buildsystem/incorporating.html
as a reference to set up the structure of the repository (FWIW, I did
not use repo, however I do not believe this should impact the build system).
However, it appears these instructions may be outdated(?) or otherwise
incorrect.
I set up a file structure as shown under the heading "Kernel directory"
in the above webpage, taking sources from;
kernel/ -> https://github.com/sel4/sel4
projects/seL4_libs/ -> https://github.com/seL4/seL4_libs
tools/ -> https://github.com/seL4/seL4_tools
I symlinked default-CMakeLists.txt to CMakeLists.txt in the root
directory as well as init-build.sh to the root directory.
I created a build directory, and from within that directory, executed
../init-build.sh -DPLATFORM=X86_64 -DSIMULATION=TRUE, but this produced
the CMake error;
CMake Error at kernel/configs/seL4Config.cmake:174 (message):
Variable 'KernelArch' is not set.
Call Stack (most recent call first):
kernel/CMakeLists.txt:10 (include)
(I got the same result regardless of PLATFORM value).
I cannot tell where the issue lies. Any pointers would be appreciated.
Kind regards,
ST (fossy)
Abstract:
We are conducting a small embedded power systems security exercise at Charles Darwin University Control Systems Test Facility (CSTF) on the Laot System designed for protecting critical infrastructure (see https://trustworthy.systems/projects/TS/laot, https://eds.power.on.net/laot-pub).
The exercise will involve penetration testing with the targets being a generator controlled by a Comap controller and a small nuclear reactor simulator (see https://eds.power.on.net/little-moata/index).
These devices will for parts of the exercise be protected by the Laot system.
There will be no cost to participants. All material including reports will be provided to all participants at the end.
Keywords: seL4, Laot, MODBUS, Security, Protection of Critical Infrastructure, Hybrid Power Systems, AUUG
What: Laot is a seL4-based system for protecting critical infrastructure.
Why: The exercise is intended to test the system and provide a useful exercise for the penetration testing on industrial control systems.
When: Over the next 2-4 weeks.
How: Send an email or ring Phil he will give you an exercise brief and timings. Any general enquires are also welcome via the same means.
Where: Remote for participants but the lab is in Darwin, Northern Australia. Local Darwin participants will be provided appropriate Darwin food and drink.
Who: The 3 members of the Laot team are Gernot Heiser, Ben Leslie and Phil Maker.
What: the exercise will be conducted over a 72h period in order to document and describe vulnerabilities in a variety of systems.
Please read the Laot and little moata references above and contact Phil.
In terms of background you will need to know the usual kali penetration tools (nmap, ...) and have an idea about either C or MODBUS. We will provide example code and exercise instructions.
Phil Maker
web: https://eds.power.on.net/EDS
email: <philip.maker(a)gmail.com>
phoneemail: <philmakerphone(a)gmail.com> -- email to phone (fastest)
phone: +61 (0)447 630 229
I want to run cross-communicating CAmkES VMs on an embedded device. I see from https://github.com/seL4/camkes-vm-examples that my options are optiplex9020, cma34cr, and exynos5422.
Are there any other options? Which of these options are known to work properly with a recent seL4 image?
To reduce maintenance burden, we would like to remove seL4 support for the
KZM evaluation board, which is based on the freescale i.MX31 processor with
an ARM1136 core. Since this is the only ARMv6 platform supported by seL4,
this would also remove support for ARMv6.
We've previously sought feedback here, and in the seL4 discourse:
https://sel4.discourse.group/t/should-we-continue-to-support-armv6-and-kzm-…https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/thread/EQ27WY…
We've now prepared an RFC to begin the formal process to remove KZM support:
https://sel4.atlassian.net/browse/RFC-8
If you have concerns about this, please raise them as soon as possible! If
you support the change, please also let us know, since that helps us
establish consensus.
Hello,
I'm trying to learn from the "sel4webserver" app here:
https://docs.sel4.systems/projects/sel4webserver/.
I believe I've been able to configure my network the way described on that
page, but I'm failing to build because I'm missing the docsite dependencies
here: https://github.com/seL4/docs/blob/master/tools/Dockerfile
I build all my camkes apps using docker's `make user` with these files
here: https://github.com/seL4/seL4-CAmkES-L4v-dockerfiles.git
I'm sure there's a way to have a docker container with these camkes
dependencies as well as the docsite dependencies, but I'm not an expert
with docker.
Does anyone have any tips on how to make all these things play nice
together?
Cheers,
Michael Neises