There has been much work on information flow control and on the static analysis of security guarantees. The lattice model of information flow comes from the early work of Bell and LaPadula[BL75] and Denning [Den76]. More recent work on information flow policies has examined complex aggregation policies for commercial applications [CW87, BN89, Fol91]. We have not addressed policies that capture conflicts of interest, though our fine-grained tracking of ownership information seems applicable. Many of these information control models use dynamic labels rather than static labels and therefore cannot be checked statically. IX [MR92] is a good example of a practical information flow control system that takes this approach. Our propagation of ownership information is also reminiscent of models of access control that merge ACLs at run time [MMN90].
Static analysis of security guarantees also has a long history. It has been applied to information flow [DD77, AR80] and to access control [JL78, RSC92]. There has recently been more interest in provably-secure programming languages, treating information flow checks in the domain of type checking [VSI96, Vol97]. Also, integrity constraints [Bib77] have been treated as type checking [PO95].
We have avoided considering covert channels arising from time measurement and thread communication. A scheme for statically analyzing thread communication has been proposed [AR80]; essentially, a second basic block label is added with different propagation rules. This second label is used to restrict communication with other threads. The same technique would remove timing channels, and could be applied to our scheme. It is not clear how well this scheme works in practice; it seems likely to restrict timing and communication quite severely. Static side-effect and region analysis [JG91], which aims to infer all possible side-effects caused by a piece of code, may be able to capture effects like timing channels.
Andrew C. Myers, Barbara Liskov