aferr
commented
4 years ago The point of this comment is to just point out another issue.
Including both conjunctions and disjunctions in the syntax of labels in the most obvious way makes "flowsTo" undecidable (see appendix). This presents a problem for proving security properties because most IFC proofs commonly split into cases on whether some proposition of the form (labelX flowsTo labelY) is true. Most pen-and-paper proofs are written in classical logic, so splitting into cases this way is always allowed. The IFC proofs for Oak are in coq, so splitting into cases is only possible if "flowsTo" is decidable.
Maybe one way to resolve this would be to restrict the syntax of labels so that conjunctions are permitted, but checking flowsTo is always decidable. Though I'm not sure what this syntax would be. In the initial version of Jif, I think the surface syntax allowed joins, and meets could appear as a result of label inference, and this was decidable. If we can map checking flowsto into horn clauses, then flowsTo reduces to HORNSAT, which is decidable and solvable in linear time. (Though I don't see a way to support conjunctions/disjunctions in a way that maps to horn clauses).
Appendix: Why do disjunctions make flowsTo undecidable? It maps to the SAT problem - flowsTo is analogous to "implies" (the lattice over propositions) and the goal would be to check if the proposition "X ->Y" is satisfiable where X and Y are arbitrary propositions.
This will make the Oak IFC more similar to the FLAM model, in which principals can be connected by conjunctions as well as disjunctions.
It will probably require integrating a SAT solver in the Oak Runtime to allow for normalization and comparison ("flows to" operator) of labels.
cc @daviddrysdale @aferr