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. <skydive...@gmail.com> 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 <ger...@unsw.edu.au> 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 <neisesmich...@gmail.com>
> > 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 <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
> >
> _______________________________________________
> 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
