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(a)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(a)gmail.com>)
escribió:
Hi Michael,
Just trying to answer your question about how to get data from a
simulated system to a host system, the way we do it for sel4test and
sel4bench is to use the serial console and grep for magic escape
strings. It isn't foolproof but having something like:
printf("<digest>%s</digest>\n", digest); from the simulated machine
can be captured automatically by the host via matching the input
character stream from the console looking to match
<digest>.*</digest>. We use expect
(https://en.wikipedia.org/wiki/Expect) or the python wrapper pexpect
for scripting this and it's how we extract seL4test results and the
sel4bench benchmark results that are automatically posted to
https://sel4.systems/About/Performance/ via capturing the serial
stream. (
https://github.com/seL4/sel4bench/runs/4064401581?check_suite_focus=true
shows the output where the benchmark results are just dumped to the
console).
Kent.
Greetings
I'm recently conducting research on WCET analysis of seL4-based systems. Graph-to-graph seems to be a good starting point. However the toolset doesn't seem to be fully working in my setup.
My setup: x86, 16GB RAM, Windows10 WSL Ubuntu 20.04
Goal: To replicate the static WCET analysis decribed in the paper [Sewell et al. 2016], using graph-to-graph and graph-refine/seL4-example build.
Steps taken:
- repo setup with "verification-manifest"
- fetched 2 versions: defalut (10/21/2021), and 12.1.0
- followed READMEs: preparing isabelle, HOL4, standalone c-parser, and their dependencies (according to graph-refine/seL4-example/readme)
- L4V_ARCH=ARM
- [./run_tests] in l4v
- [make tar] in graph-refine/seL4-example
- [python graph-refine.py <targetdir> all]
Results (default version) :
---------------------------
- seL4-example [make tar]: all things seem normal except
- Graph spec failed in _start for pos 0xe0000008.
- Graph spec failed in _start for pos 0xe0000008.
- l4v run_tests: 43/51 passed
- HaskellKernel STUCK (probably due to internet access issue for my region), CParserTest Failed
- graph-refine: KeyError: 'kernel_devices'
- This one is interesting. The seL4 code fetched with this "default" manifest contains a "kernel_device_frames", which I think is called "kernel_devices" in previous versions of seL4 kernel code. In kernel.elf.rodata they seem to be associated with the same block of assembly code.
Results (12.1.0):
---------------------------
- seL4-example [make tar]: same as default, graph spec fails
- l4v run_tests: 29/51 passed
- HaskellKernel STUCK as usual, CParserTest Failed, CBaseRefine TIMEOUT, AInvs TIMEOUT, a lot others SKIPPED due to dependency
- graph-refine: There's no KeyError now because "kernel_devices" is present in this version of seL4 code, but I got this instead:
###=======================================
### Doing stack analysis for 'cap_get_capPtr'. (48 of 575)
### Traceback (most recent call last):
### File "graph-refine.py", line 31, in <module>
### args = target_objects.load_target_args ()
### ...
### ...
### File "stack_logic.py", line 223, in get_ptr_offsets
### assert not fail_early, (v, ptr)
### AssertionError: ((3758178040, Expr ('Var', Type ('Word', 32), name = 'r13')), 'r13_after_3758178040_3758178040=i+0')
###=====================================
Here are my questions:
- Are these issues common, or is my setup & installations just wrong? Any way to resolve these issues? (big questions, and hence the long email, and hence I'm here asking the experts)
- Is solver.py currently broken? (dug up some clues in seL4-example/Makefile)
- for graph-to-graph, phantom_preempt.py seems required in the convert_loop_bounds step: Any guide on how to write this file, e.g. format, content?
- To replicate the WCET experiment in the 2016 paper, should I download the specific version of the verification repo of that time?
- static vs. measurement-based WCET analysis: Going forward, on more advanced ARM archs (e.g., Armv8), is static WCET analysis still worth it (or even feasible)? Is hybrid approach the way to go? Is the TS team still working on WCET tools for seL4 on ARM systems? (saw papers from the team many years ago discussing the combination of static cache analysis and probabilistic measurement)
Regards,
Jack
There've been a few messages stuck in the queue recently because
they're too large for the list.
Please remember when sending to the Devel(a)sel4.systems list
-- trim what you're replying to, to just the relevant bits
-- reply in-line (no top-posting)
-- send only plain text (not screen shots or HTML). Serial port
output can be pasted in-line.
This will maximise your chance of getting email through on first
attempt.
--
Dr Peter Chubb https://trustworthy.systems/
Trustworthy Systems Group CSE, UNSW
Hi Michael!
Adding the full list to the thread again (we missed them at some point...).
"I appreciate the complete lack of partial credit, and I consider you find
my work to be a waste."
I don't think anyone thinks your work is a waste. Personally, I just gave
my opinion about the architecture, but of course the final decision is
yours, as it is your baby :)
Maybe someone on the list can answer you with a more specific example you
require (even if they already gave some hints...).
Cheers,
El lun, 25 oct 2021 a las 19:11, Michael Neises (<neisesmichael(a)gmail.com>)
escribió:
> Hugo (and Everyone),
>
> Thank you for the reminders.
>
> I believe it's trivial to provide or restrict caps to any IO device. So,
> yes, I believe with the board's reference manual it should theoretically be
> quite easy to restrict them all.
>
> I appreciate the complete lack of partial credit, and I consider you find
> my work to be a waste. So with that in mind I'll ask once more:
>
> Has anyone on the planet ever performed such an independent measurement of
> a virtual machine, or is seL4 really as unusable as indicated?
>
> I don't want to spend any amount of time barking up a tree that doesn't
> exist.
>
> Cheers,
> Michael Neises
>
>
>
>
>
> On Mon, Oct 25, 2021, 01:02 Hugo V.C. <skydivebcn(a)gmail.com> wrote:
>
>> Hi Michael,
>>
>> as I commented, it depends on the runtime environment. The scenario I
>> described, even if challenging, it is just one of many you could face. Let
>> me explain myself.
>>
>> Really, it is irrelevant if the full Linux (or whatever OS) VM is
>> "inmutable". At some point you need to load code into memory and run it.
>> Then, only formal verified code (like seL4) is reasonably secure. Being
>> pedant, anything else simply it is not.
>> Why?
>>
>> The reason is you will never be sure what interactions the VM OS (in your
>> example Linux) will have with the outside World. Do you have NTP client...?
>> HTTP clients...(wget)? DNS clients...? Are you absolutely sure you know
>> every line of this VM OS (Linux) and can guarantee there will be no out of
>> control interaction with the outside Word?
>>
>> Let's go a step ahead in the offensive mindset. Even in the case you are
>> building a siloed "air gap" machine (no networking), do you have full
>> awareness of all the I/O mechanisms of the device so you can guarantee
>> there will be no interaction with the outside World...?
>>
>> For that reasons code is formally verified. That is the only way to be
>> sure things are reasonably secure.
>>
>> If we accept the last statement as true, any integrity check done from
>> inside of unverified code, is, by definition, not trustable. But of course
>> you can do it.
>>
>> On the other side, what I don't get is, if you consider (for whatever
>> reason) your guest OS is inmutable... then why you want to check integrity
>> from inside...?
>>
>> In embedded World, integrity checks always need something (theoretically)
>> really inmutable (i.e. CPU fuses). You need to check/anchor from the most
>> trustable source you have. That's why in embedded devices there are those
>> "funny" boot sequences with chain of trust where different parts of the
>> system (from most simple to most complex) are used to verify the next step
>> in the boot chain.
>>
>> Having said that, of course you can do integrity checks from inside the
>> VM itself, but IMHO will be a waste of trusted computing power of seL4
>> platform.
>>
>> Please excuse me in advance if I misunderstood your message.
>>
>> A very interesting topic.
>>
>> Cheers,
>>
>>
>> El lun., 25 oct. 2021 2:34, Michael Neises <neisesmichael(a)gmail.com>
>> escribió:
>>
>>> Hugo and Everyone,
>>>
>>> Thanks for the response. This is something I've worried about as well.
>>>
>>> I've been under the impression that once I compile a seL4 image, that
>>> image should be static no matter how many times I boot it. That is, I've
>>> looked around for persistent storage to use, and my solution has so far
>>> been to recompile the entire seL4 image in order to insert new data. So
>>> even when I "touch" files in the Linux virtual machine, they are completely
>>> forgotten when I reboot the system. For a time I thought of this as an
>>> impediment, but I soon came to realize it as a benefit. So I suppose I
>>> should clarify that when I said "Linux kernel" in that quote, I really
>>> meant this particular Linux image which is prepared at compile-time and
>>> virtualized by seL4 at runtime.
>>>
>>> For the last several months, I've been operating under the assumption
>>> that there is no way for me, even as a developer, to "manipulate the seL4
>>> image I used to boot myself." Namely, I've been trying to jump through all
>>> these virtual network hoops because I couldn't figure out a way to make
>>> persistent changes to the image. So, as I said, I had taken it for granted
>>> that a seL4 image was immutable in this way, but I recognize your point
>>> that maybe it is not. My argument has been that the seL4 image is loaded
>>> onto an SD card, and I can forbid access to that SD card, which means the
>>> image should be guaranteed to be untouchable except maybe by the seL4
>>> kernel itself.
>>>
>>> I believe seL4's proofs uphold my argument regarding "capabilities" to
>>> the SD card, but I admit a slim understanding of seL4's "caps." I will be
>>> happy as always to be edified.
>>>
>>> Cheers and Good Evening to you,
>>> Michael Neises
>>>
>>> On Sun, Oct 24, 2021 at 4:32 PM Hugo V.C. <skydivebcn(a)gmail.com> wrote:
>>>
>>>> Hi Michael,
>>>>
>>>> "Please correct me if I am wrong, but I think if the very first thing
>>>> the Linux kernel does is measure itself, before it is even connected
>>>> to a network, then there is simply no attack surface"
>>>>
>>>> My 5 cents: it is not so simple... it depends on the specfic run time
>>>> environment.
>>>> Anyway, just as an example, some years ago I was challenged with a
>>>> similar scenario: an appliance running Linux firmware with an embedded
>>>> integrity mechanism in the kernel code that checked its own integrity and
>>>> also the integrity of all loaded kernel modules (that were doing integrity
>>>> checks of the file system). Once initial modules were loaded no more were
>>>> allowed to be loaded.
>>>> Anyway, the running kernel was very outdated, so I was able to find a
>>>> vulnerability that allowed me to inject my own data/code in the kernel
>>>> space. The problem was persistence: most of the file system was read
>>>> only... with the exception of some config files in the compact flash
>>>> storage... a second bug in the parsing of the config files (that allowed
>>>> user space command execution to trigger the kernel vuln) gave me the
>>>> persistence I wanted for my kernel level vulnerability in that "inmutable"
>>>> system. Game over.
>>>>
>>>> So, it really depends on your environment. As long you have I/O data
>>>> operation were an attacker can interact to some persistent storage, then
>>>> there's room for persistent intrusion no matter the runtime checks you do
>>>> on the kernel or the file system. There have been plenty of even more
>>>> elaborated attacks/tricks on heavily siloed and isolated and "inmutable"
>>>> systems that have been carried out in the computing history. In fact, those
>>>> are the interesting ones... :-)
>>>>
>>>> Hopes this helps.
>>>>
>>>>
>>>> El dom., 24 oct. 2021 19:46, Michael Neises <neisesmichael(a)gmail.com>
>>>> escribió:
>>>>
>>>>> Hello seL4 developers,
>>>>>
>>>>> Thank you for the replies.
>>>>>
>>>>> For the sake of clarity, the system works like this:
>>>>> At compile time, some expected digest values are made available only
>>>>> to a
>>>>> distinct CAmkES component. At the time of first-Linux-boot, a kernel
>>>>> module
>>>>> takes several measurements of the other kernel modules present
>>>>> (including
>>>>> itself). It reports these digests outwards to CAmkES, where they are
>>>>> compared against the expected values. It is the "pre-compile-time
>>>>> provisioning of these expected digests" in which I am interested. At
>>>>> this
>>>>> time, I can simulate the system and compute these digests, but the
>>>>> only way
>>>>> I have to extract them is to copy them by hand off the screen. To be
>>>>> totally explicit, I want to extract these values in order to re-compile
>>>>> them into a system that knows its expected digest values. I want to
>>>>> have an
>>>>> initial simulation where I extract these digests, so that in the
>>>>> subsequent compilation and simulations, the system is aware what values
>>>>> these digests are required to take.
>>>>>
>>>>> Please correct me if I am wrong, but I think if the very first thing
>>>>> the
>>>>> Linux kernel does is measure itself, before it is even connected to a
>>>>> network, then there is simply no attack surface. Of course I'm very
>>>>> happy
>>>>> to be wrong, but I don't see who the attacker is in this situation.
>>>>> Certainly, there remains an open question of how to extend these
>>>>> measurements meaningfully into the space where there is a viable attack
>>>>> surface (after enabling a network adapter), but I consider that
>>>>> question to
>>>>> be beside the point for now (some future work). If there is some way
>>>>> for me
>>>>> to inspect the run-time data of the Linux system without relying
>>>>> somewhat
>>>>> on a tool inside the Linux instance, I would very much like to know
>>>>> about
>>>>> it. My strategy follows the same path as the vm-introspect example app
>>>>> (which I'm under the impression was created for this explicit purpose),
>>>>> which itself trusts implicitly the Linux instance. Again, to be
>>>>> entirely
>>>>> explicit, there does not appear to be any information anywhere on a
>>>>> way to
>>>>> meaningfully inspect a virtualized Linux system without trusting it
>>>>> even
>>>>> the slightest bit. I would be elated to be corrected; if someone can
>>>>> show
>>>>> me how to scrape (from the seL4 side exclusively) all the bits from a
>>>>> virtual Linux system and reassemble those bits into
>>>>> semantically-valuable
>>>>> information, I'm sure you will not hear from me for several months
>>>>> while I
>>>>> rebuild everything I have. At this time that does not appear to be
>>>>> possible.
>>>>>
>>>>> Cheers,
>>>>> Michael Neises
>>>>>
>>>>> On Tue, Oct 19, 2021 at 3:46 PM Michael Neises <
>>>>> neisesmichael(a)gmail.com>
>>>>> wrote:
>>>>>
>>>>> > Hello seL4 developers,
>>>>> >
>>>>> > I want to be able to retrieve data from seL4's virtual Linux
>>>>> machine, in
>>>>> > order to store it in a persistent way. Namely, I want to be able to
>>>>> > simulate a seL4 kernel, boot its Linux virtual machine, compute some
>>>>> hash
>>>>> > digests, and then export those hash digests. These digests are
>>>>> valuable
>>>>> > because they represent the "clean room" runtime-state of the linux
>>>>> machine.
>>>>> > Currently I can export these digests by way of hand-eye
>>>>> coordination, but I
>>>>> > consider this unusable as a piece of software.
>>>>> >
>>>>> > To date I've taken two main approaches: CAmkES FileServer or virtual
>>>>> > networking. I'm under the impression that the FileServer changes are
>>>>> not
>>>>> > persistent through reboot, and even if they were, to change the boot
>>>>> image
>>>>> > after compile-time would seem to fly in the face of seL4's
>>>>> principles.
>>>>> > Virtual networking seems to promise I can host my digests on a
>>>>> webpage that
>>>>> > is visible to my "root host" machine; that is, the simulated seL4's
>>>>> linux
>>>>> > instance hosts a site available on my 192.168.x.x network. I know
>>>>> there is
>>>>> > a seL4webserver app as part of the seL4 repositories which claims to
>>>>> do
>>>>> > this, but unfortunately its prose is unhelpful and it doesn't seem
>>>>> to work
>>>>> > even when it compiles and simulates.
>>>>> >
>>>>> > I've taken two distinct strategies to investigate the virtual network
>>>>> > approach. First, I tried to get it to work on my normal stack:
>>>>> Windows 10
>>>>> > using WSL2 using a Docker container to simulate the seL4 image. The
>>>>> problem
>>>>> > with this approach is that it appears I'm required to blindly thread
>>>>> 3 or 4
>>>>> > needles all at once, without getting feedback more descriptive than
>>>>> "you
>>>>> > didn't do it." In other words, there does not appear to be a partial
>>>>> > success available, and without ICMP ping, I honestly have no idea
>>>>> how to
>>>>> > debug these "virtual" networks.
>>>>> >
>>>>> > Next, I tried simplifying my stack by installing the dependencies
>>>>> natively
>>>>> > on a Debian 10 machine, which should bypass several layers of the
>>>>> virtual
>>>>> > network I was suggesting in my first strategy. Unfortunately, I met
>>>>> with
>>>>> > the same "AttributeError: module 'yaml' has no attribute
>>>>> 'FullLoader'"
>>>>> > error that inspired me to begin using Docker several years ago. Of
>>>>> course I
>>>>> > should note that "pip/pip2/pip3 install pyyaml" all report that
>>>>> pyyaml is
>>>>> > already installed, so I would be in debt to anyone who has an idea
>>>>> about
>>>>> > that error.
>>>>> >
>>>>> > To conclude, I find virtual networks opaque, and I would be grateful
>>>>> for
>>>>> > any guidance. If you have a different idea how I might achieve my
>>>>> goal, I
>>>>> > would be similarly effusive in my thanks.
>>>>> >
>>>>> > Cheers,
>>>>> > Michael Neises
>>>>> >
>>>>> _______________________________________________
>>>>> Devel mailing list -- devel(a)sel4.systems
>>>>> To unsubscribe send an email to devel-leave(a)sel4.systems
>>>>>
>>>>
Hello! I recently received a PinePhone for my birthday, and it finally arrived a few weeks later. It’s been fun to tinker with so far, although I haven’t yet replaced the Linux distro it came with yet, which I plan to do soon.
But thinking about my options for that made me wonder, has anyone attempted to run seL4, even just a test program, on one of these before? It’s an aarch64 device using a quad-core Allwinner A64 SOC, so four Cortex CPU cores and an Arm Mali GPU.
I don’t have any experience bringing up an OS in new hardware. It runs Linux fine, and while the included software setup is a bit sluggish, I’m pretty sure that’s just from Plasma mobile being very resource hungry.
So, I’m curious, has anyone experimented with this in the past? I think this platform could be very useful, personally I’m hoping that as hobbyist type phones like this become more mature, that people will have more choices for software to run on it.
