Title | Composing system integrity using I/O automata |
Publication Type | Conference Paper |
Year of Publication | 1994 |
Authors | Amoroso, E., Merritt, M. |
Conference Name | Tenth Annual Computer Security Applications Conference |
Keywords | Automata, automata theory, Automatic control, BIOS Security, closure properties, computer viruses, control systems, customer environment, data integrity, externally-controlled transitions, human factors, I/O automata, input output automata, integrity definitions, invalid initial states, invalid starts, Metrics, pubcrawl, resilience, Resiliency, Safety, Scalability, security, security of data, system design, system integrity, Taxonomy, transition control, valid states, vending machine |
Abstract | The I/O automata model of Lynch and Turtle (1987) is summarized and used to formalize several types of system integrity based on the control of transitions to invalid starts. Type-A integrity is exhibited by systems with no invalid initial states and that disallow transitions from valid reachable to invalid states. Type-B integrity is exhibited by systems that disallow externally-controlled transitions from valid reachable to invalid states, Type-C integrity is exhibited by systems that allow locally-controlled or externally-controlled transitions from reachable to invalid states. Strict-B integrity is exhibited by systems that are Type-B but not Type-A. Strict-C integrity is exhibited by systems that are Type-C but not Type-B. Basic results on the closure properties that hold under composition of systems exhibiting these types of integrity are presented in I/O automata-theoretic terms. Specifically, Type-A, Type-B, and Type-C integrity are shown to be composable, whereas Strict-B and Strict-C integrity are shown to not be generally composable. The integrity definitions and compositional results are illustrated using the familiar vending machine example specified as an I/O automaton and composed with a customer environment. The implications of the integrity definitions and compositional results on practical system design are discussed and a research plan for future work is outlined. |
DOI | 10.1109/CSAC.1994.367321 |
Citation Key | amoroso_composing_1994 |