Using traces based on procedure calls to reason about composability

Information flow models are usually conceived in terms of requirements on system traces, while verification that a system satisfies information flow requirements is usually done in terms of a state machine specification. The necessary translation from one model to another may result in a loss of understandability and expressiveness. J. McLean (JACM, Vol.31, no.3, pp.600-627, July 1984) showed how a language based on traces of procedure calls may be used to reason about security, and how one may prove that a program satisfies a specification written in that language. The language that he uses, however, does not easily lend itself to specification of composition of communicating processes. The present work modifies the language so that it is possible to specify the composition of systems. Several different information flow properties analogous to properties that have been defined for other systems, along with their composability, are defined and discussed