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 <ger...@unsw.edu.au> wrote: > Folks, > > 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? > > Gernot > > > On 26 Oct 2021, at 05:29, Hugo V.C. <skydive...@gmail.com> wrote: > > > > 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, > > > > > > > > > > El lun, 25 oct 2021 a las 19:11, Michael Neises (< > neisesmich...@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. <skydive...@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 <neisesmich...@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. <skydive...@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 <neisesmich...@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 < > >>>>>> neisesmich...@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@sel4.systems > >>>>>> To unsubscribe send an email to devel-leave@sel4.systems > >>>>>> > >>>>> > > _______________________________________________ > > Devel mailing list -- devel@sel4.systems > > To unsubscribe send an email to devel-leave@sel4.systems > > _______________________________________________ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems > _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
