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 (<neisesmichael(a)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. <skydivebcn(a)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 <neisesmichael(a)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. <skydivebcn(a)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 <neisesmichael(a)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 <
>>>>> neisesmichael(a)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(a)sel4.systems
>>>>> To unsubscribe send an email to devel-leave(a)sel4.systems
>>>>>
>>>>
