27 Oct
2021
27 Oct
'21
4:58 p.m.
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 <gernot(a)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
_______________________________________________
Devel mailing list -- devel(a)sel4.systems
To unsubscribe send an email to devel-leave(a)sel4.systems
_______________________________________________
Devel mailing list -- devel(a)sel4.systems
To unsubscribe send an email to devel-leave(a)sel4.systems
On 27 Oct 2021, at 14:05, Michael Neises
<neisesmichael(a)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 <gernot(a)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. <skydivebcn(a)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 (<
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
>>>>
>>>
_______________________________________________
Devel mailing list -- devel(a)sel4.systems
To unsubscribe send an email to devel-leave(a)sel4.systems