- Devel - lists.sel4.systems

Re: Runtime Measurement Hiccup
by Hugo V.C. 05 Nov '21

05 Nov '21

Hi Michael! Adding the full list to the thread again (we missed them at some point...). "I appreciate the complete lack of partial credit, and I consider you find my work to be a waste." I don't think anyone thinks your work is a waste. Personally, I just gave my opinion about the architecture, but of course the final decision is yours, as it is your baby :) Maybe someone on the list can answer you with a more specific example you require (even if they already gave some hints...). Cheers, … [View More] El lun, 25 oct 2021 a las 19:11, Michael Neises (<neisesmichael(a)gmail.com>) escribió: > Hugo (and Everyone), > > Thank you for the reminders. > > I believe it's trivial to provide or restrict caps to any IO device. So, > yes, I believe with the board's reference manual it should theoretically be > quite easy to restrict them all. > > I appreciate the complete lack of partial credit, and I consider you find > my work to be a waste. So with that in mind I'll ask once more: > > Has anyone on the planet ever performed such an independent measurement of > a virtual machine, or is seL4 really as unusable as indicated? > > I don't want to spend any amount of time barking up a tree that doesn't > exist. > > Cheers, > Michael Neises > > > > > > On Mon, Oct 25, 2021, 01:02 Hugo V.C. <skydivebcn(a)gmail.com> wrote: > >> Hi Michael, >> >> as I commented, it depends on the runtime environment. The scenario I >> described, even if challenging, it is just one of many you could face. Let >> me explain myself. >> >> Really, it is irrelevant if the full Linux (or whatever OS) VM is >> "inmutable". At some point you need to load code into memory and run it. >> Then, only formal verified code (like seL4) is reasonably secure. Being >> pedant, anything else simply it is not. >> Why? >> >> The reason is you will never be sure what interactions the VM OS (in your >> example Linux) will have with the outside World. Do you have NTP client...? >> HTTP clients...(wget)? DNS clients...? Are you absolutely sure you know >> every line of this VM OS (Linux) and can guarantee there will be no out of >> control interaction with the outside Word? >> >> Let's go a step ahead in the offensive mindset. Even in the case you are >> building a siloed "air gap" machine (no networking), do you have full >> awareness of all the I/O mechanisms of the device so you can guarantee >> there will be no interaction with the outside World...? >> >> For that reasons code is formally verified. That is the only way to be >> sure things are reasonably secure. >> >> If we accept the last statement as true, any integrity check done from >> inside of unverified code, is, by definition, not trustable. But of course >> you can do it. >> >> On the other side, what I don't get is, if you consider (for whatever >> reason) your guest OS is inmutable... then why you want to check integrity >> from inside...? >> >> In embedded World, integrity checks always need something (theoretically) >> really inmutable (i.e. CPU fuses). You need to check/anchor from the most >> trustable source you have. That's why in embedded devices there are those >> "funny" boot sequences with chain of trust where different parts of the >> system (from most simple to most complex) are used to verify the next step >> in the boot chain. >> >> Having said that, of course you can do integrity checks from inside the >> VM itself, but IMHO will be a waste of trusted computing power of seL4 >> platform. >> >> Please excuse me in advance if I misunderstood your message. >> >> A very interesting topic. >> >> Cheers, >> >> >> El lun., 25 oct. 2021 2:34, Michael Neises <neisesmichael(a)gmail.com> >> escribió: >> >>> Hugo and Everyone, >>> >>> Thanks for the response. This is something I've worried about as well. >>> >>> I've been under the impression that once I compile a seL4 image, that >>> image should be static no matter how many times I boot it. That is, I've >>> looked around for persistent storage to use, and my solution has so far >>> been to recompile the entire seL4 image in order to insert new data. So >>> even when I "touch" files in the Linux virtual machine, they are completely >>> forgotten when I reboot the system. For a time I thought of this as an >>> impediment, but I soon came to realize it as a benefit. So I suppose I >>> should clarify that when I said "Linux kernel" in that quote, I really >>> meant this particular Linux image which is prepared at compile-time and >>> virtualized by seL4 at runtime. >>> >>> For the last several months, I've been operating under the assumption >>> that there is no way for me, even as a developer, to "manipulate the seL4 >>> image I used to boot myself." Namely, I've been trying to jump through all >>> these virtual network hoops because I couldn't figure out a way to make >>> persistent changes to the image. So, as I said, I had taken it for granted >>> that a seL4 image was immutable in this way, but I recognize your point >>> that maybe it is not. My argument has been that the seL4 image is loaded >>> onto an SD card, and I can forbid access to that SD card, which means the >>> image should be guaranteed to be untouchable except maybe by the seL4 >>> kernel itself. >>> >>> I believe seL4's proofs uphold my argument regarding "capabilities" to >>> the SD card, but I admit a slim understanding of seL4's "caps." I will be >>> happy as always to be edified. >>> >>> Cheers and Good Evening to you, >>> Michael Neises >>> >>> On Sun, Oct 24, 2021 at 4:32 PM Hugo V.C. <skydivebcn(a)gmail.com> wrote: >>> >>>> Hi Michael, >>>> >>>> "Please correct me if I am wrong, but I think if the very first thing >>>> the Linux kernel does is measure itself, before it is even connected >>>> to a network, then there is simply no attack surface" >>>> >>>> My 5 cents: it is not so simple... it depends on the specfic run time >>>> environment. >>>> Anyway, just as an example, some years ago I was challenged with a >>>> similar scenario: an appliance running Linux firmware with an embedded >>>> integrity mechanism in the kernel code that checked its own integrity and >>>> also the integrity of all loaded kernel modules (that were doing integrity >>>> checks of the file system). Once initial modules were loaded no more were >>>> allowed to be loaded. >>>> Anyway, the running kernel was very outdated, so I was able to find a >>>> vulnerability that allowed me to inject my own data/code in the kernel >>>> space. The problem was persistence: most of the file system was read >>>> only... with the exception of some config files in the compact flash >>>> storage... a second bug in the parsing of the config files (that allowed >>>> user space command execution to trigger the kernel vuln) gave me the >>>> persistence I wanted for my kernel level vulnerability in that "inmutable" >>>> system. Game over. >>>> >>>> So, it really depends on your environment. As long you have I/O data >>>> operation were an attacker can interact to some persistent storage, then >>>> there's room for persistent intrusion no matter the runtime checks you do >>>> on the kernel or the file system. There have been plenty of even more >>>> elaborated attacks/tricks on heavily siloed and isolated and "inmutable" >>>> systems that have been carried out in the computing history. In fact, those >>>> are the interesting ones... :-) >>>> >>>> Hopes this helps. >>>> >>>> >>>> El dom., 24 oct. 2021 19:46, Michael Neises <neisesmichael(a)gmail.com> >>>> escribió: >>>> >>>>> Hello seL4 developers, >>>>> >>>>> Thank you for the replies. >>>>> >>>>> For the sake of clarity, the system works like this: >>>>> At compile time, some expected digest values are made available only >>>>> to a >>>>> distinct CAmkES component. At the time of first-Linux-boot, a kernel >>>>> module >>>>> takes several measurements of the other kernel modules present >>>>> (including >>>>> itself). It reports these digests outwards to CAmkES, where they are >>>>> compared against the expected values. It is the "pre-compile-time >>>>> provisioning of these expected digests" in which I am interested. At >>>>> this >>>>> time, I can simulate the system and compute these digests, but the >>>>> only way >>>>> I have to extract them is to copy them by hand off the screen. To be >>>>> totally explicit, I want to extract these values in order to re-compile >>>>> them into a system that knows its expected digest values. I want to >>>>> have an >>>>> initial simulation where I extract these digests, so that in the >>>>> subsequent compilation and simulations, the system is aware what values >>>>> these digests are required to take. >>>>> >>>>> Please correct me if I am wrong, but I think if the very first thing >>>>> the >>>>> Linux kernel does is measure itself, before it is even connected to a >>>>> network, then there is simply no attack surface. Of course I'm very >>>>> happy >>>>> to be wrong, but I don't see who the attacker is in this situation. >>>>> Certainly, there remains an open question of how to extend these >>>>> measurements meaningfully into the space where there is a viable attack >>>>> surface (after enabling a network adapter), but I consider that >>>>> question to >>>>> be beside the point for now (some future work). If there is some way >>>>> for me >>>>> to inspect the run-time data of the Linux system without relying >>>>> somewhat >>>>> on a tool inside the Linux instance, I would very much like to know >>>>> about >>>>> it. My strategy follows the same path as the vm-introspect example app >>>>> (which I'm under the impression was created for this explicit purpose), >>>>> which itself trusts implicitly the Linux instance. Again, to be >>>>> entirely >>>>> explicit, there does not appear to be any information anywhere on a >>>>> way to >>>>> meaningfully inspect a virtualized Linux system without trusting it >>>>> even >>>>> the slightest bit. I would be elated to be corrected; if someone can >>>>> show >>>>> me how to scrape (from the seL4 side exclusively) all the bits from a >>>>> virtual Linux system and reassemble those bits into >>>>> semantically-valuable >>>>> information, I'm sure you will not hear from me for several months >>>>> while I >>>>> rebuild everything I have. At this time that does not appear to be >>>>> possible. >>>>> >>>>> Cheers, >>>>> Michael Neises >>>>> >>>>> On Tue, Oct 19, 2021 at 3:46 PM Michael Neises < >>>>> neisesmichael(a)gmail.com> >>>>> wrote: >>>>> >>>>> > Hello seL4 developers, >>>>> > >>>>> > I want to be able to retrieve data from seL4's virtual Linux >>>>> machine, in >>>>> > order to store it in a persistent way. Namely, I want to be able to >>>>> > simulate a seL4 kernel, boot its Linux virtual machine, compute some >>>>> hash >>>>> > digests, and then export those hash digests. These digests are >>>>> valuable >>>>> > because they represent the "clean room" runtime-state of the linux >>>>> machine. >>>>> > Currently I can export these digests by way of hand-eye >>>>> coordination, but I >>>>> > consider this unusable as a piece of software. >>>>> > >>>>> > To date I've taken two main approaches: CAmkES FileServer or virtual >>>>> > networking. I'm under the impression that the FileServer changes are >>>>> not >>>>> > persistent through reboot, and even if they were, to change the boot >>>>> image >>>>> > after compile-time would seem to fly in the face of seL4's >>>>> principles. >>>>> > Virtual networking seems to promise I can host my digests on a >>>>> webpage that >>>>> > is visible to my "root host" machine; that is, the simulated seL4's >>>>> linux >>>>> > instance hosts a site available on my 192.168.x.x network. I know >>>>> there is >>>>> > a seL4webserver app as part of the seL4 repositories which claims to >>>>> do >>>>> > this, but unfortunately its prose is unhelpful and it doesn't seem >>>>> to work >>>>> > even when it compiles and simulates. >>>>> > >>>>> > I've taken two distinct strategies to investigate the virtual network >>>>> > approach. First, I tried to get it to work on my normal stack: >>>>> Windows 10 >>>>> > using WSL2 using a Docker container to simulate the seL4 image. The >>>>> problem >>>>> > with this approach is that it appears I'm required to blindly thread >>>>> 3 or 4 >>>>> > needles all at once, without getting feedback more descriptive than >>>>> "you >>>>> > didn't do it." In other words, there does not appear to be a partial >>>>> > success available, and without ICMP ping, I honestly have no idea >>>>> how to >>>>> > debug these "virtual" networks. >>>>> > >>>>> > Next, I tried simplifying my stack by installing the dependencies >>>>> natively >>>>> > on a Debian 10 machine, which should bypass several layers of the >>>>> virtual >>>>> > network I was suggesting in my first strategy. Unfortunately, I met >>>>> with >>>>> > the same "AttributeError: module 'yaml' has no attribute >>>>> 'FullLoader'" >>>>> > error that inspired me to begin using Docker several years ago. Of >>>>> course I >>>>> > should note that "pip/pip2/pip3 install pyyaml" all report that >>>>> pyyaml is >>>>> > already installed, so I would be in debt to anyone who has an idea >>>>> about >>>>> > that error. >>>>> > >>>>> > To conclude, I find virtual networks opaque, and I would be grateful >>>>> for >>>>> > any guidance. If you have a different idea how I might achieve my >>>>> goal, I >>>>> > would be similarly effusive in my thanks. >>>>> > >>>>> > Cheers, >>>>> > Michael Neises >>>>> > >>>>> _______________________________________________ >>>>> Devel mailing list -- devel(a)sel4.systems >>>>> To unsubscribe send an email to devel-leave(a)sel4.systems >>>>> >>>> [View Less]

4 7

Pine64 PinePhone with seL4: any prior attempts?
by Isaac Beckett 02 Nov '21

02 Nov '21

Hello! I recently received a PinePhone for my birthday, and it finally arrived a few weeks later. It’s been fun to tinker with so far, although I haven’t yet replaced the Linux distro it came with yet, which I plan to do soon. But thinking about my options for that made me wonder, has anyone attempted to run seL4, even just a test program, on one of these before? It’s an aarch64 device using a quad-core Allwinner A64 SOC, so four Cortex CPU cores and an Arm Mali GPU. I don’t have any … [View More]

3 2

CAmkES: dataports larger than 4k
by Fabrizio Bertocci 31 Oct '21

31 Oct '21

Is it possible to use dataports that are larger than 4k? I tried with both typed dataports and "Buf" dataport but I can't find a way to do it. In the hello-camkes-2 tutorial, I tried to add a configuration for my dataports in the main assembly file to increase its size like this: // Typed dataport name: 'd_image' // Buf dataport name: 'd' configuration { echo.d_size=65536; // Buf dataport echo.d_image_size=65536; // Typed dataport } unfortunately that doesn't seem to do … [View More]

2 1

Runtime Measurement Hiccup
by Michael Neises 24 Oct '21

24 Oct '21

Hello seL4 developers, I want to be able to retrieve data from seL4's virtual Linux machine, in order to store it in a persistent way. Namely, I want to be able to simulate a seL4 kernel, boot its Linux virtual machine, compute some hash digests, and then export those hash digests. These digests are valuable because they represent the "clean room" runtime-state of the linux machine. Currently I can export these digests by way of hand-eye coordination, but I consider this unusable as a piece of … [View More]software. To date I've taken two main approaches: CAmkES FileServer or virtual networking. I'm under the impression that the FileServer changes are not persistent through reboot, and even if they were, to change the boot image after compile-time would seem to fly in the face of seL4's principles. Virtual networking seems to promise I can host my digests on a webpage that is visible to my "root host" machine; that is, the simulated seL4's linux instance hosts a site available on my 192.168.x.x network. I know there is a seL4webserver app as part of the seL4 repositories which claims to do this, but unfortunately its prose is unhelpful and it doesn't seem to work even when it compiles and simulates. I've taken two distinct strategies to investigate the virtual network approach. First, I tried to get it to work on my normal stack: Windows 10 using WSL2 using a Docker container to simulate the seL4 image. The problem with this approach is that it appears I'm required to blindly thread 3 or 4 needles all at once, without getting feedback more descriptive than "you didn't do it." In other words, there does not appear to be a partial success available, and without ICMP ping, I honestly have no idea how to debug these "virtual" networks. Next, I tried simplifying my stack by installing the dependencies natively on a Debian 10 machine, which should bypass several layers of the virtual network I was suggesting in my first strategy. Unfortunately, I met with the same "AttributeError: module 'yaml' has no attribute 'FullLoader'" error that inspired me to begin using Docker several years ago. Of course I should note that "pip/pip2/pip3 install pyyaml" all report that pyyaml is already installed, so I would be in debt to anyone who has an idea about that error. To conclude, I find virtual networks opaque, and I would be grateful for any guidance. If you have a different idea how I might achieve my goal, I would be similarly effusive in my thanks. Cheers, Michael Neises [View Less]

4 6

Verified platform (Sabre lite)
by ouvl 14 Oct '21

14 Oct '21

Good afternoon. The only verified platform is Sabre lite (Platform Sabre lite, System-on-chip i.MX6). There is a link for the board on the website https://docs.sel4.systems/Hardware/sabreLite.html, but the link https://boundarydevices.com/product/sabre-lite-imx6-sbc/ is not working. On the same site https://boundarydevices.com, board https://boundarydevices.com/product/bd-sl-i-mx6/ is displayed. There are different boards with iMX6 processor, and processors, for example, i.MX 6 ULL, i.MX 6 … [View More]

1 0

Inter-VM communication on seL4
by everton＠ssrc.tii.ae 29 Sep '21

29 Sep '21

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 … [View More]

2 1

ethernet pass-through using CAmkES VM on x86
by meshkat os 29 Sep '21

29 Sep '21

hi I am new to camkes VM on x86. I want to connect the guest to the host via the ethernet network. and I used this ( https://docs.sel4.systems/projects/camkes-vm/) tutorial to create pass-through in minimal example x86. run in qemu on ubuntu 17.10. but the guest os doesn't create an ethernet interface. I also tested zmq example this is qemu options: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,enforce,+… [View More]vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 and minimal.camkes configs: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0) 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; vm0_config.pci_devices_iospace = 1; vm0_config.ioports = [ {"start":0x4080, "end":0x4090, "pci_device":0x1f, "name":"SATA"}, {"start":0x4090, "end":0x40a0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b0, "end":0x40b8, "pci_device":0x1f, "name":"SATA"}, {"start":0x40b8, "end":0x40c0, "pci_device":0x1f, "name":"SATA"}, {"start":0x40c8, "end":0x40cc, "pci_device":0x1f, "name":"SATA"}, {"start":0x40cc, "end":0x40d0, "pci_device":0x1f, "name":"SATA"}, {"start":0x3000, "end":0x3020, "pci_device":0, "name":"Ethernet5"}, ]; vm0_config.pci_devices = [ { "name":"SATA", "bus":0, "dev":0x1f, "fun":2, "irq":"SATA", "memory":[], }, { "name":"Ethernet5", "bus":5, "dev":0, "fun":0, "irq":"Ethernet5", "memory":[ {"paddr":0xc0500000, "size":0x20000, "page_bits":12}, {"paddr":0xc0520000, "size":0x4000, "page_bits":12}, ], }, ]; vm0_config.irqs = [ {"name":"SATA", "source":19, "level_trig":1, "active_low":1, "dest":11}, {"name":"Ethernet5", "source":0x11, "level_trig":1, "active_low":1, "dest":10}, ]; } thanks [View Less]

4 4

seL4 Raspberry Pi 4B Support
by Drew Humphrey 29 Sep '21

29 Sep '21

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

4 3

Mismatch in number of pages allocated
by Sid Agrawal 28 Sep '21

28 Sep '21

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 … [View More]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 [View Less]

1 0

"Incorporating into your project"
by fosslinux 27 Sep '21

27 Sep '21

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 … [View More]

2 2