Secure microkernel in a KVM switch offers spy-grade app virtualization

Researchers at Australian think tank Data61 and the nation's Defence Science and Technology Group have cooked up application publishing for the paranoid, by baking an ARM CPU and secure microkernel into a KVM switch. As explained to El Reg by Toby Murray, on behalf of his fellow researcher from Data61’s Trustworthy Systems …

[Christian Berger]

What I don't understand is why that needs an OS kernel?

After all this can essentially be done by video mixing, something that TV studios did since the 1960s.

Essentially you'd sync all sources together, either via genlockable graphics cards, or via a separate framebuffer on your mixer. (no CPU intervention necessary, this can all be done in hardware). The framebuffer can even do things like scaling resolutions, or cropping video.

Then you define a "transparent" colour, as well as a priority list for all those layers. Every 8 or 16 Bit 1990s games console did that in hardware.

The only thing that actually needs a CPU to touch actual data is the system that determines the mouse position and distributes the mouse and keyboard events accross the individual systems. And that code is rather trivial. It only needs to translate the position information into absolute coordinates, ask the hardware what system is at a certain pixel, and forward it to that system.

[Bronek Kozicki]

Re: What I don't understand is why that needs an OS kernel?

You also need to direct the input to appropriate machine, and how do you know which machine that is? For this you need the concept of input focus and switching of that focus. This can be tricky and requires some OS-level smarts. Also, there is an old problem of compatibility with wide range of inputs - for example, WEY-TEC USB Deskswitch II does not work with Topre Realforce keyboards, even though both devices appear to be entirely standard/generic stuff. This is because "dumb" KVM is unable to negotiate keyboard layout with this particular model, something an OS will normally do with ease.

EDIT: Just found there is a very nice document explaining how this thing works, at http://people.eng.unimelb.edu.au/tobym/papers/cddc-acsac2016.pdf . It appears at least one of the authors is an avid El Reg reader , hence icon ->

[Christian Berger]

Re: What I don't understand is why that needs an OS kernel?

"You also need to direct the input to appropriate machine, and how do you know which machine that is?"

Actually that's what I've tried to explain in my OP. You can either use the mouse position, or have some sort of focus system, where you have, for example, a row of buttons on the KVM where you can select one of the systems to have all input. If you set your background to "transparent", you can even draw a border around it, or grey out all the other systems.

"WEY-TEC USB Deskswitch II does not work with Topre Realforce keyboards"

Most KVMs today on the market have horribly bad firmware, cobbled together by people who have no idea what they are doing. There are many KVM switches which essentially crash when you select an input with no video coming in.

[Pen-y-gors]

Re: What I don't understand is why that needs an OS kernel?

Sounds like a KVM version of those multiple windows you get on CCTV monitors. Could be handy though.

Or if you don't mind a bit of sharing, something like a couple of Teamviewer sessions (other software is available) open at the same time on the same monitor? Not 100% air-gapped though...

[Anonymous Coward]

Re: What I don't understand is why that needs an OS kernel?

"Then you define a "transparent" colour, as well as a priority list for all those layers. Every 8 or 16 Bit 1990s games console did that in hardware"

I don't know the real underlyings of 90's games consoles, but are you sure. I could understand if it was done in firmware, the OS or microcode but hardware?

With video overlay, how do you have copy/paste and how do you ensure that apps/documents with secure tags have rules bout copying? Without an OS how would you allow dynamic video scaling. How would you allow mouse pointer and keyboard input with no OS at all, however basic. Depends on the strict definition of an OS though.

MY question would be - these systems are no longer air gapped, they may only be bridged by a secure layer, but this would fail an air gapped spec. A manual KVM can retain the air gap but even a software controlled KVM would surely break it.

[Woza]

Re: What I don't understand is why that needs an OS kernel?

It's also important to realise that SeL4 is a *micro*kernel. When I looked into it a couple of months ago, it (i.e: the core, subject to the security proof) seemed to be little more than a scheduler and IPC mechanism. Things like file systems, drivers, etc would need to be implemented on top of SeL4. In other words, when saying "why does it need an OS kernel", bear in mind that we're not talking Linux levels of complexity / functionality here.

Caution Icon: I didn't spend very long investigating, and don't claim to be an expert.

[patrickstar]

Re: What I don't understand is why that needs an OS kernel?

These consoles typically didn't have an OS, firmware or microcode... at most just a small bootloader to check that the game cartridge was properly licensed.

And you have to remember that CPUs were very much slower back then, so the tradeoff for when things were worth doing in hardware was very different.

All of them had at least sprites implemented in hardware. And that implies having transparency and frequently also some sort of layer management (even if it's just a defined order the hardware sprites are drawn in).

[Anonymous Coward]

Re: What I don't understand is why that needs an OS kernel?

"All of them had at least sprites implemented in hardware. And that implies having transparency and frequently also some sort of layer management (even if it's just a defined order the hardware sprites are drawn in)."

We're talking 90's - even the Sega Megadrive was an 80's console and that had a 68000 CPU, a Z80, sound and video processors etc. You could load games from CD onto the Megadrive.

The Playstation was released in the 90s, as well as the N64 - although no longer 8/16 bit.

[patrickstar]

Re: What I don't understand is why that needs an OS kernel?

The MegaCD was an add-on. I'm not too familiar with its internals but I assume it had atleast some firmware to control the CD drive and loading enough data from the CD to boot.

The Megadrive/Genesis console itself certainly didn't have an OS, and the only firmware was for the copy protection (see Trademark Security System and the resulting legal case).

The actual game code simply accessed all hardware directly. Including programming the audio/video controllers which did the sort of work (sprite management, transparency, layering, etc) that the original question was about. I suppose the official SDK had some library routines for common tasks, but it's certainly nothing like an OS.

You can find commented disassemblies of some of the Sonic games for Megadrive/Genesis here: http://info.sonicretro.org/Disassemblies

Note the total absence of any sort of OS services being invoked. Note also that even very low-level stuff that would presumably be common across all games, like trap handlers, is handled by the game code itself.

There simply wasn't any need for an OS or even hardware abstraction, since the hardware was identical from the programmers viewpoint, and reasonably easy to work with (unlike modern GPUs for example).

I'm not intimately familiar with the Playstation but I would be very surprised if it too didn't have things like transparency support in hardware even though it has more of an "OS" (which IIRC is basically just a bootloader and system services).

[Charles 9]

Re: What I don't understand is why that needs an OS kernel?

The Sega/Mega CD had its own processors and an internal BIOS for handling the CD drive itself. The CD add-on for the TurboGrafx/PC Engine operated on similar principles, as do all CD-based consoles of the fifth generation. You could say these BIOS's were very rudimentary OS's in themselves but nothing like the more generalized internal OS's you see in the sixth generation and beyond.

[patrickstar]

Re: What I don't understand is why that needs an OS kernel?

Apparently the MegaCD had a grand total of 128KB firmware ROM. Not sure how much of it was actually used.

[Dan 55]

Re: What I don't understand is why that needs an OS kernel?

Well, the Amiga CD32 had a full Kickstart and extra libraries for the CD32 hardware.

Nintendo's approach was the opposite, years later the GameCube didn't really have an OS and the Wii barely had one, games still relied on static libraries compiled in by the devkit.

[Dan 55]

Re: What I don't understand is why that needs an OS kernel?

No firmware then, it was all ASIC hardware.

I can remember the BBC Domesday Project reserving one colour for the laser disc output for the Street View part, and that was the 80s. Here's is a video of the original hardware using it to show just photos and here's a video of the emulated version which shows the more Street View-like part.

If only they'd moved the program and data to CD-ROM in the 90s it wouldn't have been lost. I say lost but it was inaccessible for most people and still is. There's a web version but the National Disc is missing.

[Julz]

Old Tech

Sun had a secure version of the Sun Ray system that did this sort of thing yonks ago.

[Christian Berger]

BTW, verified Kernels mean only very specific things

A verified kernel might prevent your USB stack from overwriting other code, but it's not neccesarily going to prevent you from having parts of your USB stack overwrite other parts, and therefore eliminating the "data diode" on the USB ports.

Additionally this implementation encodes window positions in separate pixels which is both error prone (some graphics cards rescale/gamma-correct their framebuffers before sending it to the screen) and another interface and therefore attack vector.

In any case, it's what I suggested as a response to this talk here:

https://media.ccc.de/v/MRMCD2014_-_6037_-_de_-_tiefbaustelle_s21_-_201409071330_-_end-to-display_verschlusselung_zur_absicherung_von_industriespionage_-_sango

[Anonymous Coward]

Proof of correctness proves what, exactly?

"code that has been mathematically proven free of error"

A wise man once said "I have proved this program correct, but I have not tested it" (or something like that).

See e.g.

http://www-cs-faculty.stanford.edu/~knuth/faq.html (it's in there, honest).

Does proof of correctness say anything about fitness for purpose?

[sitta_europea]

Re: Proof of correctness proves what, exactly?

[quote]

Does proof of correctness say anything about fitness for purpose?

[/quote]

I don't think it does, but I think it says quite a lot about the people that came up with the sound-bite, and about the people who regurgitate it in the media.

If we haven't got a mathematical technique for calculating something as simple as a prime number, or for proving (or disproving) that P=NP, how can anyone even dream that we can mathematically prove the correctness of something as complex as a kernel?

And what use would it be anyway? There's no suggestion that any of the servers, device firmware or application code that this magically perfect kernel will cause to execute will be anything other than the usual cans of bug-ridden shite.

[Dave 126]

Re: Proof of correctness proves what, exactly?

SeL4 formally verified some time ago, and since tested:

https://en.m.wikipedia.org/wiki/L4_microkernel_family

https://www.quantamagazine.org/formal-verification-creates-hacker-proof-code-20160920/

[Paul Crawford]

Re: Proof of correctness proves what, exactly?

That proves the seL4 kernel is correct.

Not that the compiler(s) used are bug-free, or that the CPU/GPU/FPGA is bug-free in design. Also it does not cover things like the "rowhammer" attack on dynamic memory refresh/integrity.

Also in many cases (not sure about here) what you actually prove is the code matches the formal specifications given in some maths-like syntax. I'm not sure how you go about proving that specification did not overlook some use-case, but I imagine that is possible for a very limited set of permutations.

[John Smith 19]

Re: Proof of correctness proves what, exactly?

Quite a lot in terms of the kernel.

But what about the code running on top of the kernel?

The environment is only as secure as its weakest link, not its strongest.

Personally I think this misses the point. People pay for this level of isolation for a reason.

[Charles 9]

Re: Proof of correctness proves what, exactly?

You assume the kernel is a link in a chain, whereas you should see it as a gate where all activity goes through it. That alters the structure since weak links still have to pass through the strong gate first.

[Anonymous Coward]

Re: Proof of correctness proves what, exactly?

"you should see [the kernel] as a gate where all activity goes through it. That alters the structure since weak links still have to pass through the strong gate first."

To a very limited extent.

If one may refer to a door rather than a gate (gates should be for electronics, not software), then a door is only useful if what surrounds the door is harder to get through than the door. Otherwise it's just for decoration rather than any functional reason.

Classic recent example: all kinds of Intel processor security flummery and associated software security BS, while there is a zero-effort total-control vulnerability in basically every modern x86 processor's management processor (the AMT one, which seems to have gone quiet recently).

But long before that hit the fan, there were plenty of cases where stuff misbehaved, often in exploitable ways.

[Charles 9]

Re: Proof of correctness proves what, exactly?

"If one may refer to a door rather than a gate (gates should be for electronics, not software), then a door is only useful if what surrounds the door is harder to get through than the door. Otherwise it's just for decoration rather than any functional reason."

That's part of the formal specification. EVERYTHING has to go through the kernel. IOW, no tricks like DMA access. If everything is required to go through the formally-proven code in order to function, then it really is a gatekeeper (and I will call them gates because you associated gates with walls--big walls like once crossed England and still exist in China--where there was basically only one way in or out).

[Anonymous Coward]

Re: Proof of correctness proves what, exactly?

Not entirely quiet on the AMT vulnerability. Just a few days ago a hidden register was discovered that allows you to block AMT entirely, put in as a requirement by some agency or agencies apparently. No statement on who required it or why it was intentionally concealed that this "feature" could be turned off.

[Anonymous Coward]

Re: Proof of correctness proves what, exactly?

Does this class of "proof" prove the source matches the formal specification? Mostly, proofs like this seem to be derived from source code. Mostly, processors execute executable code (with some data).

What's the relationship between source and executable? Has that process ever been usefully proven correct, or has it been shown to be generally untrustworthy (which isn't the same as showing it broken). See e.g. another wise man and his "Reflections on Trusting Trust", and various related discussions which followed.

More to this than meets the eye - as Professor Ross Anderson recently discovered, at this kind of level, safety and security can be rather closely related. His background is security. Others have been coming at it from a safety point of view. It'd be nice to see them talking more to each other:

https://www.lightbluetouchpaper.org/2017/06/01/when-safety-and-security-become-one/

"What happens when your car starts getting monthly upgrades like your phone and your laptop? It’s starting to happen, and the changes will be profound. We’ll be able to improve car safety as we learn from accidents, and fixing a flaw won’t mean spending billions on a recall. But if you’re writing navigation code today that will go in the 2020 Landrover, how will you be able to ship safety and security patches in 2030? In 2040? In 2050? At present we struggle to keep software patched for three years; we have no idea how to do it for 30.

Our latest paper reports a project that Éireann Leverett, Richard Clayton and I undertook for the European Commission into what happens to safety in this brave new world. Europe is the world’s lead safety regulator for about a dozen industry sectors, of which we studied three: road transport, medical devices and the electricity industry.

Up till now, we’ve known how to make two kinds of fairly secure system. There’s the software in your phone or laptop which is complex and exposed to online attack, so has to be patched regularly as vulnerabilities are discovered. It’s typically abandoned after a few years as patching too many versions of software costs too much. The other kind is the software in safety-critical machinery which has tended to be stable, simple and thoroughly tested, and not exposed to the big bad Internet. As these two worlds collide, there will be some rather large waves.

(continues)"

Recommended reading (even if a little overdue).

[nijam]

Re: Proof of correctness proves what, exactly?

> the source matches the formal specification?

If the formal specification *isn't* the source code, it's a waste of ink.

[Charles 9]

Re: Proof of correctness proves what, exactly?

But the point becomes, how do you ensure that the object code is as formally secure as the source code since you now have a case of trusting the compiler and the old "Trusting Trust" problem. Not to mention, what about hardware-based exploits?

[frank ly]

"... no naughty cutting and pasting ..."

Except for eyeball to fingertip copy/paste activity.

[Anonymous Coward]

Sweet!

So I could be looking at pr0n in one window and the network-national socialists could never detect this from the company machine.

[MCMLXV]

I stopped reading...

... at "Australian think tank".

[Anonymous Coward]

application virtualization?

Sounds like anti-virtualization to me.

Virtualization: one PC appears to be multiple PCs

Anti-virtualization: multiple PCs appear to be one PC

[Syn3rg]

Defeating the purpose

- "Those air gaps provide hygiene so that organisations feel satisfied data can't move between applications."

- "... and even allow cut and paste between windows".

Aren't these statements mutually exclusive?

[Stevie]

Bah!

and even allow cut and paste between windows.

There goes your air-gap.

[oldcoder]

Still looks like it would be susceptible to a smart USB device....

Specially when some of the monitors around can be read from the USB ports.

[John Robson]

I used to do this...

With four machines on different security domains.

I took a simple KVM switch and used the monitor as the 'second' screen for the important machines, and the Keyboard and mouse were switched with this second monitor (which was on the left of one machine, and the right of the other two - one machine only needed a primary monitor, test lab access).

Stuff I needed visible all the time was left on the other screens, and the KVM did it's (very simple) job of redirecting mouse/keyboard commands, and selecting one of a handful of video sources perfectly.

To move files from one device to another we used either USB/CD drives which went through a network isolated virus scanner between insertions or later an automated network based version of the same.

It didn't need a full blown micro kernel installed custom fiddle switch - it just worked as good access to multiple machines. A great deal cheaper than the 'solution' here I am guessing as well...

[Outer mongolian custard monster from outer space (honest)]

Airgapped isolation, interesting. Sounds difficult to circumvent.

*click* takes smartphone shot of monitor.

[Anonymous Coward]

Ahem, how did you get the smartphone past the metal detector which was in turn guarded who was in turn watched over with security cameras?

[BobC]

After blitzing through the paper linked above, this looks mostly like a "virtual monitor" system combined with "smart" keyboard + mouse + clipboard sharing.

At its simplest, virtual monitors are commonly used in CCTV systems to map normally independent systems (each with its own monitor) onto a single monitor. This system goes a bit beyond that to 1) permit multiple desktops to overlap, and 2) extract individual windows from the desktops for display on the shared monitor (mainly to declutter the display to remove redundant desktop pixels, and adding an identification overlay).

Nothing that users of X-windows systems haven't been used to for well over 30 years. And, like X-windows, the trick is sending the window meta-data along with the content (be that pixels or graphics primitives). This information is normally sent out-of-band, such as via a separate stream, but this new system has only KVM-like connections, and so instead must use embedded pixel data to encode and convey the metadata. (BTW: This data could be vulnerable to a MITM attack or Tempest-like snooping.)

Sharing a single keyboard, mouse and clipboard across multiple PCs has been done for many years in many ways, with Synergy currently being the best-known example. The Synergy protocol is straightforward, as is the data routing. On each PC, a thin shim is used to route the single physical KM to the appropriate PC's KM input layer.

So, we are left just a pair of protocols needing to be processed, some contextual rules guiding the properties and restrictions of the overall functionality. Not really all that much functionality, though the ability to handle KM inputs and pixel-level video switching are needed, but that's mainly simple hardware with simple drivers.

Taken as a whole, an OS isn't really needed at all. Not even a kernel: This could easily be run on bare hardware. But the need for the protocols to handle security restrictions demands some of the code, specifically the clipboard code (and, perhaps a security classification overlay), be executed in a trusted and protected manner. Not much of a kernel is required (the minimum needed to provide protection and separation of one shared agent and one agent for each connected system), so a small and proven minimalist kernel would seem to be just the ticket.

[LaeMing]

Hmmmm. Is this sort of thing even /legal/ in Australia these days? It uses cryptography so must be about terism!