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 (<[email protected]>) 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. <[email protected]> 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 <[email protected]> >> 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. <[email protected]> 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 <[email protected]> >>>> 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 < >>>>> [email protected]> >>>>> 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 -- [email protected] >>>>> To unsubscribe send an email to [email protected] >>>>> >>>> _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
