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 (<kent.mcleod72(a)gmail.com>)
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. <skydivebcn(a)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 <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
>
> > 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
>
> _______________________________________________
> 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
_______________________________________________
Devel mailing list -- devel(a)sel4.systems
To unsubscribe send an email to devel-leave(a)sel4.systems