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. () 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 () 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.