2014-10-30 16:21 GMT+01:00 Tomasz Rola <rtomek@ceti.pl>:
Also, I myself would not use L4. No bad feelings about it but, sounds a bit too huge for this task, meybe? Since I don't know too much about all this stuff, I guess I'd start with C or Forth on bare metal. I had not enough time to make sure I could develop for it using Linux/BSD, since other OSes are no-no.
For me the reason for a kernel is existing drivers and a proven infrastructure. You want to make the protocol and data as non-native as possible, change it around as much as you can, to remove potential exploits. There's just too many exploits though :(... No way to protect against an exploited PDF, unless you want to reformat the PDF's (maybe into JPG?). You could theoretically do that on the fly with L4, but with bare-metal you'd be hurting yourself a lot. Which also brings us back to Eugen, Eugen, for what is USB flash Biosafety 4? What do you want to do with these drives? Just moving data in, without moving data out? Or just preventing some magical build-into-the-chipset exploits (like is possible with Firewire)? All of those could be brought with an L4-running device with USB and another protocol, allowing better connectivity, too. But depending on the threat model, less might be enough (or more!). I think an air-gap is supposed to be gapped both ways. one could create a purpose-specific data format, that can be re-interpreted by the software running on the L4 device. Then, when transferring a file, the L4 device will read the stuff from the USB, reinterpret it to ensure correct formatting, write it out to the other side in whatever way chosen. Depending on volume it might be feasible to transfer manually, just mash it into a (radiation isolated!) keyboard.