* A Language for automatically enforcing privacy policies
  Yang, Jean; Yessenov, Kuat; Solar-Lezama, Armando
** Summary
   This paper presents a lambda_J language that allows security policies to be specified separately from the core functionality of the program.
   How programs are written:
   1. Create data structures
   2. Create views for high/low confidentiality view for each field
   3. Create policy to decide confidentiality of each field given context, etc
   4. Write the program
   Conjecture: two levels are enough for any program, as the lattice (or any other security pattern) can be enforced by policies
   Intersection of policies are worked out with constraint solver (Z3), defaulting to top (high confidentiality value) when ambiguous
** Questions
   Q: Mike: Is this static or dynamic?
   A: hybrid, because it has a runtime component (dynamic) but also explores all branches (static)
   Q: State space explosion?
   A: Kris: not branching symbolically at every branch, just where levels matter, and there isn't much
   A: Mike: when branching on symbolic value, symbolically evaluate both sides to get 'if sig then v_t else v_f'
            It would seem this kind of branching doesn't happen much, but no way to reason about this
** Criticisms
   Aseem: not sure how easy the separate-policy language is to work with
   Kris: the security guarantee is not too strong. If you get to a point where consistency is checked, either it will be consistent or the program will halt
** Ideas
   Authors are working on ways to analyze these separate security policies
* Faceted execution of policy-agnostic programs
  Austin, Thomas H.; Yang, Jean; Flanagan, Cormac; Solar-Lezama, Armando
** Summary
   This realizes the Jeeves language of the last paper using faceted values, which allows for greater pruning of the symbolic execution space.
   It turns out that Yang 2012 and Austin 2012 were presented in the same session, and the audience asked how the two were related, and this is it
   Advantage over declassification policies: Can set conditional policy once, and runtime checker enforces for each channel
   Compared to original faceted values paper:
   - Expression evaluation rules are same (F-split, F-left, F-right)
   - F-label is new (creates new dynamic labels, and maps keys to new policies that are uncondintionally true)
   - F-restrict is new (looks into policy, evaluates the new, and combines for a new policy)
   - Fixed typos
   - Application rules same
   - Print rule is new, takes context/channel ({e_1}) and value ({e_2}), gathers all keys that appear in all, and find a pc such that
     a value facet that satisfies all the constraints can be satisfied
     Does '{k_1 ... k_n} includes all labels in V_f, V_c, V_p' create a circular dependency? Mike will ask
   Has a much better defined security guarantee:
   - Projection theorem with strong language behind it
   - Noninterference relationship comes from that and powerset lattice of keys
** Questions
   Q: Is this just an engineering paper?
   A: Yes, but world is better off for having it published
** Criticisms
   The paper is not self-contained (relies hevily on previous papers: Yang 2012, Austin 2012)
   Some don't like that the example is the same, Mike likes being able to directly compare syntax
   Symbolic execution can't run forever
** Ideas
   go to a print statement and have it list sample outputs
   example driven refinement