1. 12
  1. 5

    This is a cute hack. The topology of the natural numbers creates two problems, though. First, higher security levels have authority to access lower security levels. Second, it’s not possible to privilege-separate two programs under composition if they are at the same security level. Sealer/unsealer pairs, as in E, are a solution to both of these problems, but they require dependent types at a minimum, and their best uses come when they can be created at runtime.

    1. 1

      A demo for the expert system shell I wrote years ago was a proof system that showed that no reverse data flows were possible in a system.

      That was fun.

    2. 1

      The article references some of the wider research on information flow control (IFC). It’s important to note that these systems generally have a few problems if you try to use them in the real world:

      • Humans are, it turns out, really bad at labelling data for security. These systems prevent sensitive data from leaking, but that’s predicated on someone correctly identifying secret data. If you get this wrong, you have no security guarantees: it’s the fundamental axiom from which all of your security proofs are derived.
      • Taint explosion. Any value derived from a secret value is tainted and so you very quickly end up in a situation where everything needs to be tainted and now you’re back in the same world you are without IFC: assume everything is secret and try not to leak it.
      • Declassification is hard. IFC systems generally require explicit declassification. In some cases it’s obvious that these are in the right place: e.g. encrypt(secret, key) should return something non-secret, even though it’s derived from two secret values (the plaintext and the key), but is that actually a valid assumption? It depends on whether your crypto algorithm was correctly implemented and that’s much harder to statically prove (see: EverCrypt). For any other situation, it’s much harder to reason about whether you should declassify.
      • Indirect leakage is difficult to quantify. Branching on a boolean may leak data via side channels, branching on a compare of an integer will probably leak less. You can be conservative in your taint tracking and make taint explosion much worse (every instruction following a branch on a secret is tainted) or you can be conservative and move side channels out of your threat model. Neither is great.