Title :
Unwinding forward correctability
Author :
Millen, Jonathan K.
Author_Institution :
Mitre Corp., Bedford, MA, USA
Abstract :
A state-machine formulation is given for forward correctability in event systems, to provide a type of unwinding result for this information flow security property. We show also how regular-expression notation provides an easy mechanical tool for verifying forward correctability for small systems, which is necessary for the effective presentation of examples and exercises
Keywords :
finite state machines; security of data; event systems; forward correctability; information flow; regular-expression notation; security of data; security property; state-machine formulation; unwinding result; Access control; Application software; Combinatorial mathematics; Information analysis; Information security; Kernel; Lattices; Logic design; Operating systems; Software tools;
Conference_Titel :
Computer Security Foundations Workshop VII, 1994. CSFW 7. Proceedings
Conference_Location :
Franconia, NH
Print_ISBN :
0-8186-6230-1
DOI :
10.1109/CSFW.1994.315952
