Janice Glasgow
Skip Abstract Section
Abstract
A formal framework called Security Logic (SL) is developed for specifying and reasoning about security policies and for verifying that system designs adhere to such policies. Included in this modal logic framework are definitions of knowledge, permission, and obligation. Permission is used to specify secrecy policies and obligation to specify integrity policies. The combination of policies is addressed and examples based on policies from the current literature are given.
- 1 ASHEROFT, E. A., ANn JAGANNATHAN, R. Operator nets. In IFIP TC-IO Conference on F~fth Generation Computer Architectures. North-Holland, Amsterdam, 1985. Google Scholar
- 2 BEN-ARI, M., MANNA, Z., AND PNUELI, A. The temporal logic of branching time. In 8th Annual ACM Sympostum on Principles of Programming Languages, ACM, New York, 1981, 164-176. Google Scholar
- 3 BURROWS, M., AB~I, M., ~x'~D NEED~M, R. A logic of authenticatmn. ACM Trans. Comput. Syst. 8, i (1990), 18-36. Google Scholar
- 4 BIB& K. J. Integrity considerations for secure computer systems. Tech. Rep. TR-3153, MITRE Corp., April 1977.Google Scholar
- 5 BELL, D. E., AND LAPADULA, L.J. Secure computer systems: Mathematical foundations and model. Tech. Rep., MITRE Corp., Bedford, Mass., 1974.Google Scholar
- 6 BURROWS, M., NEEDHXM, R., AND ABAm, M. Authentication: A practical study in belief and action. In Proceedings of the 2nd Conference on Theoretical Aspects of Reasoning About Knowledge (Pacific Grove, Calif., 1988). ACM, New York, 1988, 325 342. Google Scholar
- 7 COMMUNICATIONS SECURITY ESTABLISHMENT, DND. Canadian Trusted Computer Product Evaluation Criteria Workshop (Ottawa, Ont., Aug. 1988).Google Scholar
- 8 CLARK, D. n., AND WILSON, D. R. A comparison of commercial and military computer security policies. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987). IEEE, New York, 1987, 184-194.Google Scholar
- 9 DENNING, D. E.A lattice model of secure information flow. Corrzmun. ACM 19, 5 (May 1976), 236-243. Google Scholar
- 10 EMERSON, E. A., AND HALPERN, J.Y. "Sometimes" and "not never" revisited. In 9th Annual ACM Symposium on Prznciples of Programming Languages. ACM, New York, 1982, 127-139.Google Scholar
- 11 GASSER, M. Building a Secure Computer System. Van Nostrand, New York, 1988. Google Scholar
- 12 GOGUEN, J. A., AND MESEGUER, J. SecuriW policies and security models. In IEEE Symposium on Securzty and Privacy (Oakland, Calif., April 1982). IEEE, New York, 1982, 11-20.Google Scholar
- 13 GLASGOW. J. I., AND MACEWEN, G.H. The development and proof of a formal specification for a multilevel secure system. ACM Trans. Comput. Syst. 5, 2 (May 1987), 151 184. Google Scholar
- 14 GLASGOW, J. I., AND MACEWEN, G. H. Reasoning about knowledge in multilevel secure distributed systems. In Proceedings of the IEEE Symposium on Securtty and Privacy (Oakland, Calif., 1988). IEEE, New York, 1988, 122-128.Google Scholar
- 15 GLASGOW, J. I., AND MACEWEN, G.H. Obligation as the basis of integrity specification. In Proceedings of the IEEE Symposium on Securzty and Privacy (Oakland, Calif.,), IEEE, New York, 1982-91.Google Scholar
- 16 GLASGOW, J. I., AND MACEWEN, G.H. Obligation as the basis of integrity specification. In Proceedings of the Computer Security Foundattons Workshop (Franconia, N.H.). MITRE Corp., 1988-91.Google Scholar
- 17 GLASGOW, J. I., AND MACEWEN, G.H. Obligation as the basis of integrity specification. In Proceedings of the Computer Security Foundattons Workshop (Franconia, N. H., June 1989). MITRE Corp., 1989, 64-70.Google Scholar
- 18 GLASGOW, J. I., AND MACEWEN, G.H. An operator net model for distributed systems. J. Distrtbuted Syst. 3, 4 (Sept. 1989), 196-209.Google Scholar
- 19 GLASGOW, J. I., ANn MACEWEN, G.H. A logic for reasoning about security. In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1990). IEEE, New York, 1990.Google Scholar
- 20 GLASGOW, J. I., MACEWEN, G. H., AND PANANGADEN, P. Reasoning about knowledge and permission in secure distributed systems. In Proceedtngs of the Computer Security Foundations Workshop (Franconia, N.H., 1988). IEEE, New York, 1988, 139 146. Also appears in IEEE Cipher.Google Scholar
- 21 GLASGOW, J. I., MACEWEN, G. H., AND PANANGADEN, P. Security by permission in databases. In Database Security H: Status and Prospects. Elsevier North-Holland, Amsterdam, 1988, 197-205.Google Scholar
- 22 GUTTMAN, J. D., AND NADEL, M. E. What needs security? In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1988), 34-57.Google Scholar
- 23 HALPERN, J. Reasoning about knowledge. In Annual Reviews of Computer Science, Annual Reviews Inc., 1987, 21-35.Google Scholar
- 24 HINTAKKA, J. Knowledge and Belief. Cornell University Press, 1962.Google Scholar
- 25 HALPERN, J. Y., AND MOSES, Y. Knowledge and common knowledge in a distributed environment. In Proceedings of the 3rd ACM Conference on Distrtbuted Computing. 1984, 50-61. Google Scholar
- 26 JOHNSON, D. M., ANn THA~R, F.J. Stating security requirements with tolerable sets. ACM Trans. Comput. Syst. 6, 3 (Aug. 1988), 284-295. Google Scholar
- 27 JOHNSON, D. M., AND THAYER, F.J. Security and the composition of machines. In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1988), 72 89.Google Scholar
- 28 KmPKE, S. Semantical considerations of modal logic. Acta Philosophica Fennica 16 (1963), 83 94.Google Scholar
- 29 LAMPORT, L. Sometimes is sometimes not never. In Proceedings of 7th Annual ACM Symposium on Principles of Programming Languages, ACM, New York, 1980, 174-185. Google Scholar
- 30 LANDWEHR, C.E. Formal models for computer security. ACM Comput. Surv. 13, 3 (Sept. 1981), 247-278. Google Scholar
- 31 LUNT, T. F. ET AL. The Seaview formal security policy model. Tech. Rep., SRI International, Computer Science Lab., Menlo Park, Calif, Feb. 1989.Google Scholar
- 32 LUNT, T. F. ET AL. The Seaview security model. IEEE Trans. Softw. Eng. SE-16, 6 (June 1990). Google Scholar
- 33 MECULLOUGH, A. D. Specifications for multi-level security and a hook-up property. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987), IEEE, New York, 1987, 161-166.Google Scholar
- 34 MCCULLOUGH, A. D. Covert channels and degrees of insecurity. In Proceedings of the Computer Security Foundations Workshop (Franconia, N.H., June 1988), i 33.Google Scholar
- 35 MCCULLOUGH, A. D. Non-interference and the composability of security properties. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1988), IEEE, New York, 1988, 177-186.Google Scholar
- 36 MCLEAN, J. Reasoning about security models. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987), IEEE, New York, 1987, 123-131.Google Scholar
- 37 MCLEAN, J. The algebra of security. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1988), IEEE, New York, 1988, 2-7.Google Scholar
- 38 MOSER, L. A logic of knowledge and belief for reasoning about computer security. In Proceedings of the Computer Security Foundattons Workshop H (Franconia, N.H., 1989), 57-63.Google Scholar
- 39 MAcEWEN, G. H., POON, V. W. W., AND GLASGOW, J.I. A model for multilevel security based on operator nets. In Proceedings of IEEE Symposium on Security and Privacy (Oakland, Calif., April 1987), IEEE, New York, 1987, 150-160.Google Scholar
- 40 NATIONAL COMPUTER SECURITY CENTER. Workshop on Integrity Policy in Computer Information Systems (Waltham, Mass., Oct. 1987).Google Scholar
- 41 Proceedings of the Natzonal Computer Security Conference, Dept. of Defense, 1984-88.Google Scholar
- 42 PNUELI, A. The temporal logic of concurrent programs. Theor. Comput. Sc~. 13 (1981), 45 60.Google Scholar
- 43 PRIOR, A. Tzme and Modality. Oxford University Press, 1957.Google Scholar
- 44 RANGAN, P.V. An axiomatic basis of trust in distributed systems. In Proceedings of the 1988 IEEE Computer Society Symposium on Security and Prwacy (Oakland, Calif., 1988), 204-211.Google Scholar
- 45 RUSHBY, J.M. Design and verification of secure systems. ACM SIGOPS 15, 5 (Dec. 1981), 12-21. Google Scholar
- 46 SUTHERLAND, A. D. A model of information. In Procee&ngs of 9th Natwnal Computer Security Conference (Gaithersburg, Md., Sept. 1986), Dept. of Defense, 175-183.Google Scholar
Index Terms
- A logic for reasoning about security
Recommendations
A secure framework for publishing virtual community contracts
The notion of Virtual Community (VC) is today an important paradigm to enable dynamic and large-scale collaboration activities over the web. In many of those activities, security is an important key requirement that to date has not been widely ...
Ponder2: A Policy System for Autonomous Pervasive Environments
ICAS '09: Proceedings of the 2009 Fifth International Conference on Autonomic and Autonomous SystemsPolicies form an important part of management and can be an effective means of implementing self-adaptation in pervasive systems. Most policy-based systems focus on large-scale networks and distributed systems. Consequently, they are often fragmented, ...
Confidentiality Policies and Their Enforcement for Controlled Query Evaluation
ESORICS '02: Proceedings of the 7th European Symposium on Research in Computer SecurityAn important goal of security in information systems is confidentiality. A confidentiality policy specifies which users should be forbidden to acquire what kind of information, and a controlled query evaluation should enforce such a policy even if users ...
Comments