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. &lt;skydivebcn(a)gmail.com&gt; 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 &lt;neisesmichael(a)gmail.com&gt; > 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. &lt;skydivebcn(a)gmail.com&gt; 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 &lt;neisesmichael(a)gmail.com&gt; >>> 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&gt; >>>> 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 >>>> >>>