* All your IFCException are Belong to Us
  Hritcu, Catalin; Greenberg, Michael; Karel, Ben; Pierce, Benjamin C.; Morrisett, Greg
** Summary
   Title is reference to http://knowyourmeme.com/memes/all-your-base-are-belong-to-us
   This paper presents a system for enforcing flow control that does not terminate on information flow control exceptions (IFCExceptions). Labels are public (eliminating leaks through this channel), and associated with values, not with variables. Variable-based labels would allow 'x:=(if h then true else false)' since no assignment happens within the parens where the leak happens, and the PC would be lowered at the join point. This allows for better composability of expressions, but the more important difference is public labels. Each label implicitly has a label of bot, and when this would be elevated for any reason, this is treated as an information flow violation. In this way, computation on labels is allowed, except when it could potentially cause a leak.
   The attack scenario in this paper is what the authors call a poison pill: the attacker-supplied input is a low-security container with high-security data inside, and the server is designed to unpack that value, which it can only do in a secure context, but this would normally cause an IFCException when outputting information based on its content. More realistically, some of the secret data would be internal to the program, and a bug would cause the IFCException, and therefore a leak.
   Instead of throwing exceptions, expressions that would leak evaluate to Not a Value (NaV), which serve the same purpose, but must be dealt with in the same or higher security context than the one they were created in. These NaVs are either passed around as-is (lax/lazy) or they cause their containers to become NaVs (strict), language implementation choice.
   Semantics defined for 4 equivalent languages (lambda[], lambda[]NaV, lambda[]throw, lambda[]throw+d).
   lambda[] rules - whenever a value is used (destructed) the label of pc is tainted
   - BBrk rule for x[t]- whatever the contents of x, the contents in memory are labeled with that value,
     and the pc is tainted with the label of x. If the label of t's evaluation is less than x, then success. Otherwise, stuck program
   - All rules have a pc on the left and right, right pc always greater or equal to left pc
   - Some expressions always labeled at bot: BConst, BSum, BAbs, BLabelOf, BGetPC
   - BApp, BMatch - same as lambda, but with pc elevation
   - BTagOf - runtime tag check. Interesting: tag of value has same label of value itself, because if control flow is based on tags, then they contain information about value
   - BBOp - Looks up arguments, and result is has the join of the 2 labels, tagOf does type checking of arguments, with potential stuck program
  lambda[] NaV
   - D() - delayed exceptions for cases that were stuck program before (type errors)
   - NAppE - when calling a non-function, result is D()
   - NTagOfE - There is no tag of D()
   - NBOpE* - binary operation operatands invalid
   - BLabelOf extended to NLabelOf (doesn't care if D or V)
** Questions
   Q: Why not just throw exceptions?
   A: Exceptions always carry information from where they were thrown, and if caught in a lower context, that is a leak.
   A: Allowing exceptions to be thrown everywhere complicates the CFG
   Q: Why is the last example OK?
   A: Because labels are public, and knowing that there has been a label violation is OK.
   Q: Similar to linear continuations?
   A: Yes, collapses control channels into data channels. Good because control channels are harder to reason about than data channels
   Q: Mike: is motivation for dynamic monitors false? Dynamic monitors allow programmers to make mistakes, and then try to mitigate the resulting behavior, when static analysis would forbid it in the first place
   A: Kris: dynamic works better for OSes
   A: Mike: use static for internals, dynamic for communication channels
   A: Both: hybrid is the way to go
** Criticisms
   lambda[] is still error-sensitive, and can get stuck
   lambda[]NaV can be shown to have strong progress, but livelock still possible
   Language equivalence not proven, just shown likely through random testing
   Implementation, but no performance numbers
** Ideas
   Kris: write with static contracts and blow them away with JIT
* Implicit Flows: Can’t Live With ‘Em, Can’t Live Without ‘Em
  King, Dave; Hicks, B; Hicks, Michael; Jaeger, Trent
** Summary
   Tracking implicit flows statically leads to a *lot* of false positives, especially when there are null pointers and/or unchecked exceptions
** Ideas
   Rely more on programmer annotations
   Change the semantics of Java to change the kinds of flows and reduce false positives
   Allow global system declassifier for flows with high false positive rate
   Use different programming models, possibly with automatic translation