There are many directions to explore with this new model. An obvious next step is to implement the model by extending an existing language compiler, and developing working applications for examples like those in Section 2.
It should also be possible to augment the Java Virtual Machine [LY96] with annotations similar to those proposed in Section 5. The bytecode verifier would check both types and labels at the time that code is downloaded into the system.
The computational model described in Section 5 has a reasonable set of data types. However, it ought to support user-defined data abstractions, including both parametric and subtype polymorphism.
Formal proofs of the soundness of the model might add some confidence. In the absence of any use of the "declassify" operation, labels are located in a simple lattice that applies equally to all users, and previous results for the security of lattice-based information flow models apply to this model as well. However, because "declassify" is intended to allow information to flow across or down the lattice, standard security policies such as non-interference [GM84] are intentionally inapplicable.
Because integrity [Bib77] constraints have a natural lattice structure, supporting them may be an interesting extension to our label model; the label model can be augmented to allow each owner to establish an independent integrity policy, just as each owner now can establish an independent information flow policy.
We have assumed an entirely trusted execution environment, which means that the model described here does not work well in large, networked systems, where varying levels of trust exist among nodes in the network. Different principals may also place different levels of trust in the various nodes. A simple technique for dealing with distrusted nodes is to transmit opaque receipts or tokens for the data. However, more work is needed to adapt our model to this kind of system. It is also likely that the model of output channels should be extended to differentiate among the different kinds of outputs from the system.
We have not considered the possibility of covert channels that arise from timing channels and from asynchronous communication between threads, which can also be used to create timing channels. The technique of having a timing label for each basic block, as in Andrews and Reitman [AR80], may help with this problem, but more investigation is needed.
Next: Acknowledgments Up: A Model for Decentralized Previous: 8 Conclusions
Andrew C. Myers, Barbara Liskov