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@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@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@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@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@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@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
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@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@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@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@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@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@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@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
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@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@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@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@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@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@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@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@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
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@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@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@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@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@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@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@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@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@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
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@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@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@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@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@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@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@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@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@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@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
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@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@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@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@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@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@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@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@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@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@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@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
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@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@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@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@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@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@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@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@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@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@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@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@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
BTW, regarding to the nice trick suggested by Kent (using expect language to interact with console) just wanted to show you this expect script I wrote on 2007 (page 210 of https://www.pentest.es/checkpoint_hack.pdf) to exploit a vulnerability via interactive SSH shell in a very hardened device at that time (Check Point Secure Platform) which was an EAL4+ certified appliance with a locked down custom Linux, and patched kernel (Exec-Shield) with a painful set of memory protections, ASCII Armor, etc + a creative protection in their custom interactive shell (called CPSHELL) that only allowed a restricted set of ASCII chars... It took me 6 months to figure out how to bypass every single protection of that target, and chain all the different bypass techniques into a fully functional exploit. It was hard but I did it and I'm pretty sure anyone with somewhat creative offensive mind (there are thousands out there) would have achieved the same, after or before.
Two things I want to highlight here is:
1) Anyone that is tempted to build "insecure" software solutions (Linux/non_verified_code) on top of secure solutions (seL4) must assume for the global design of the architecture that the "insecure" solution (Linux/non_verified_code) should be considered already broken. If you don't do this and expect other low level layers of security to solve root security issues, things may go horribly wrong. This is what happened in the case of Check Point Secure Platform, at that time, all the security was relying in the low level, multiple layers of the OS protections, but the source code of the vendor specific command line tools were full of security bugs... So, let's not expect seL4 host to solve the security problems of the guests (Linux, etc). seL4 can guarantee isolation of guests and it's own security, but as long there's an interaction with the guest (i.e. via console) there's lot of room for exploitation of the guest.
2) Going a step ahead, console interaction is just the most simple, but there are other ways to interact with guests as they are not physically isolated entities of the Universe.... I mean, if we consider chain supply attacks as a real possibility (i.e. an open source tool integrated into a Linux guest on top of seL4) we should be aware that it is not difficult to create a covert channel attack to extract information from the "isolated" guest... So even without any I/O available, the guest can play with multiple physical low level hardware details and physical environment variables to create a funny reliable stealth communication channel.
I was just thinking loud but hope it helps someone else to have a wide vision of low level security. Expect scripting interaction with console suggestion by Kent reminded me about this old exploit I wrote and then I extrapolated it to any interaction in our beloved seL4 environments.
Have a nice day.
El mié, 3 nov 2021 a las 13:00, Hugo V.C. (skydivebcn@gmail.com) escribió:
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@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@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@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@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@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@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@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@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@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@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@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@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
-
Gernot Heiser -
Hugo V.C. -
Kent Mcleod -
Michael Neises