Very nice trick Kent! Thank you for sharing. That kind of information, from you guys the seL4 experts, is invaluable.
El mié, 3 nov 2021 a las 12:15, Kent Mcleod (<[email protected]>) escribió: > Hi Michael, > > Just trying to answer your question about how to get data from a > simulated system to a host system, the way we do it for sel4test and > sel4bench is to use the serial console and grep for magic escape > strings. It isn't foolproof but having something like: > printf("<digest>%s</digest>\n", digest); from the simulated machine > can be captured automatically by the host via matching the input > character stream from the console looking to match > <digest>.*</digest>. We use expect > (https://en.wikipedia.org/wiki/Expect) or the python wrapper pexpect > for scripting this and it's how we extract seL4test results and the > sel4bench benchmark results that are automatically posted to > https://sel4.systems/About/Performance/ via capturing the serial > stream. ( > https://github.com/seL4/sel4bench/runs/4064401581?check_suite_focus=true > shows the output where the benchmark results are just dumped to the > console). > > Kent. > > > > On Wed, Oct 27, 2021 at 6:02 PM Hugo V.C. <[email protected]> wrote: > > > > I really can understand Michael's frustration. As I pointed out many > times > > in the past, IMHO seL4 documentation is the weakest point of all the > > ecosysyem and a real life stop barrier for many early adopters that would > > love to familiarize with it. Many of those early adopters willl or will > not > > evangelize the rest of the World about using seL4 depending on their > "user > > experience". > > > > I'm aware that documentation can not cover every single scenario, anyway > > IMHO, the most common ones should be there very well documented. I'm also > > aware of the lack of resources for this task, anyway, I still think this > is > > a pending issue that, once improved, will boost seL4 adoption by several > > orders of magnitude. > > > > Let's not fear about "bad usage" of seL4. Let's fear no usage at all. > > > > Cheers, > > > > El mié., 27 oct. 2021 5:49, Gernot Heiser <[email protected]> escribió: > > > > > Thanks Michael. > > > > > > Just to note: While what I suggested is “easy” conceptually, that > doesn’t > > > mean our present framework make it easy to implement. I’m not the > CAmkES > > > expert, but am aware that it’s not the easiest thing to deal with. > > > > > > Gernot > > > > > > > On 27 Oct 2021, at 14:05, Michael Neises <[email protected]> > > > wrote: > > > > > > > > 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 <[email protected]> > > > 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. <[email protected]> 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 (< > > > [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] > > > > > > > > _______________________________________________ > > > > 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] > > > > > _______________________________________________ > > 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]
