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
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
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
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>)
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
can be captured automatically by the host via matching the input
character stream from the console looking to match
<digest>.*</digest>. We use 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
via capturing the serial
shows the output where the benchmark results are just dumped to the