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