Gernot and all,
No, you have it all right. It's only that I'm frustrated because I cannot see the implementation of what everyone so offhandedly calls easy. I can see how to grant R/O access to a part of the user-level address space, but I don't see how to grant R/O access to a useful address space. I've asked about it here before, and I spent quite a long time bringing kernel modules to the virtualized-linux space in an effort to realize this end. In my inexperience, I took it personally when I was told what I spent so long creating was worthless for this effort, but in a lasting way I realize knowledge has value in its own right. Hugo is obviously well-experienced and knowledgeable, and I respect his opinion highly.
I'm sure I will come back with a more appropriately worded question after going back to the source, or maybe I will surprise you with some amusing solution.
Sincerely, Michael Neises
On Tue, Oct 26, 2021 at 12:07 PM Gernot Heiser firstname.lastname@example.org wrote:
I’m not sure what triggered that reaction of Michael’s quoted by Hugo below, but it must have been something off-list. Certainly the discussion I saw on the list was perfectly polite and constructive, let’s keep it that way please.
In terms of the technical issues, I can only agree with Hugo: I fail to see how the guest measuring itself can give you any integrity guarantee. If you assume the guest to be compromised (and why else would you want to measure it) then you have to also assume it to be arbitrarily malicious, and thus it could just fake the measurement and return a known “good value” that has nothing to do with the correct measurement.
To ensure integrity, the measurement has to be done outside the guest. And doing that should not be hard: Have a separate measurement component that has R/O access to all of the guest’s address space, and it can perform the measurement in a tamper-proof fashion.
Am I missing something?
On 26 Oct 2021, at 05:29, Hugo V.C. email@example.com wrote:
Adding the full list to the thread again (we missed them at some
"I appreciate the complete lack of partial credit, and I consider you
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...).
El lun, 25 oct 2021 a las 19:11, Michael Neises (<
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
quite easy to restrict them all.
I appreciate the complete lack of partial credit, and I consider you
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
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. firstname.lastname@example.org wrote:
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.
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
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
example Linux) will have with the outside World. Do you have NTP
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
control interaction with the outside Word?
Let's go a step ahead in the offensive mindset. Even in the case you
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
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
In embedded World, integrity checks always need something
really inmutable (i.e. CPU fuses). You need to check/anchor from the
trustable source you have. That's why in embedded devices there are
"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
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.
El lun., 25 oct. 2021 2:34, Michael Neises email@example.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,
looked around for persistent storage to use, and my solution has so
been to recompile the entire seL4 image in order to insert new data.
even when I "touch" files in the Linux virtual machine, they are
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
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
image I used to boot myself." Namely, I've been trying to jump
these virtual network hoops because I couldn't figure out a way to
persistent changes to the image. So, as I said, I had taken it for
that a seL4 image was immutable in this way, but I recognize your
that maybe it is not. My argument has been that the seL4 image is
onto an SD card, and I can forbid access to that SD card, which means
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
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. firstname.lastname@example.org
"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
integrity mechanism in the kernel code that checked its own
also the integrity of all loaded kernel modules (that were doing
checks of the file system). Once initial modules were loaded no more
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
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
user space command execution to trigger the kernel vuln) gave me the persistence I wanted for my kernel level vulnerability in that
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,
there's room for persistent intrusion no matter the runtime checks
on the kernel or the file system. There have been plenty of even more elaborated attacks/tricks on heavily siloed and isolated and
systems that have been carried out in the computing history. In
are the interesting ones... :-)
Hopes this helps.
El dom., 24 oct. 2021 19:46, Michael Neises <email@example.com
> 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
> 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
> 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
> 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
> 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
> (which I'm under the impression was created for this explicit
> 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
> 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 < > firstname.lastname@example.org> > 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
> 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
>> networking. I'm under the impression that the FileServer changes
> not >> persistent through reboot, and even if they were, to change the
> 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
> 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
>> 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
> 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
>> 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
> 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 -- email@example.com > To unsubscribe send an email to firstname.lastname@example.org >
Devel mailing list -- email@example.com To unsubscribe send an email to firstname.lastname@example.org
Devel mailing list -- email@example.com To unsubscribe send an email to firstname.lastname@example.org