ComputingComputer ScienceComputer SystemsAlgorithmsFormal MethodsProgramming LanguagesAccess ControlComputability TheoryData TypesModel CheckingType CheckingType SystemsAccess TypesLanguage SafetySafety PropertiesStrong TypingType Safety
The typed access matrix (TAM) model is defined by introducing the notion of strong typing into the Harrison, Ruzzo, and Ullman model (HRU) (M. H. Harrison et al., 1978). It is shown that monotonic TAM (MTAM) has decidable, but NP-hard, safety for its acyclic creation cases. It is further shown that ternary MTAM has polynomial time safety analysis for its acyclic cases, even though it is, in general, equivalent to MTAM. Ternary MTAM thus has strong safety properties. The expressive power of ternary MTAM has been shown to be equivalent to MTAM in general. The results establish that strong typing is crucial to achieving a useful demarcation between decidable and undecidable safety, and ternary monotonic commands are critical for tractable safety analysis.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">></ETX>
19
A lattice model of secure information flow
Dorothy E. Denning · Communications of the ACM · 1976 · 1.9K citations · Full text
Butler Lampson · ACM SIGOPS Operating Systems Review · 1974 · 491 citations
A Linear Time Algorithm for Deciding Subject Security
R.J. Lipton, Lawrence Snyder · Journal of the ACM · 1977 · 199 citations · Full text
The schematic protection model
Ravinderpal Singh Sandhu · Journal of the ACM · 1988 · 132 citations · Full text