Errors can arise in defining and evaluating computer security policy as well as in translating computer security policy into procedures.
The effect of such errors in policy upon the secure operation of information systems can impose unacceptable levels of risk from the perspective of procurers and users of information systems. Relying on computer security paradigms based solely on formal methods makes it difficult if not impossible to detect and/or reason about certain classes of threats to computer security and vulnerabilities of information systems to these threats, especially for those aspects of information systems that are more readily amenable to modeling via non-formal methods. We present a paradigm integrating formal and heuristic reasoning as a basis for testing for and debugging computer security policy. To illustrate our approach, and to support our arguments, we consider the problem of reasoning about the plans of an agent who may be trying to compromise the security of an information system.
Permission to copy without fee all or part of this matexiai is grantid, provided that the copies arc not made or distributed for direct ComerCial advmmgc, the ACM copyright notice and tbc tillr of the publication and its date appear. and notice is given that copying is by pemxisrion of the Association for Computing Machinery. To copy otherwise. or to republish, requires a fee and/or specific permission.