2014-10-30 16:21 GMT+01:00 Tomasz Rola <[1]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.

References

   1. mailto:rtomek@ceti.pl