Safety analysis for the extended schematic protection model

It is argued that the access matrix model of M.H. Harrison, W.L. Ruzzo and J.D. Ullman (HRU) (1976) has extremely weak safety properties; safety analysis is undecidable for most policies of practical interest. An alternate formulation of the HRU model is presented that gives strong safety properties. This alternative formulation is called the extended schematic protection model (ESPM). ESPM is derived from the schematic protection model (SPM) by extending the creation operation to allow multiple parents for a child, as opposed to the conventional create operation of SPM, which has a single parent for a child. It is shown that, despite its equivalence to HRU, ESPM, retains a tractable safety analysis for a large class of protection schemes that are of practical interest