Verifying Security

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verifying Security

Full text

Pdf (4.68 MB)

Source

ACM Computing Surveys (CSUR) archive
Volume 13 , Issue 3 (September 1981) table of contents

Pages: 279 - 339

Year of Publication: 1981

ISSN:0360-0300

Authors

Maureen Harris Cheheyl	The MITRE Corporation, Bedford, Massachusetts
Morrie Gasser	The MITRE Corporation, Bedford, Massachusetts
George A. Huff	The MITRE Corporation, Bedford, Massachusetts
Jonathan K. Millen	The MITRE Corporation, Bedford, Massachusetts

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 5, Downloads (12 Months): 49, Citation Count: 11

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/356850.356853 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	AFFI81	AFFIRM SYSTEM DOCUMENTATION. AF- FIRM Reference Manual, D.H. Thompson and R.W. Erickson (Ed.); AFFIRM Collected Papers, R.W. Enckson (Ed.); AFFIRM Type Library, S.L. Gerhart (Ed.); AFFIRM User's Guide, S. Lee and S.L. Gerhart (Ed.); AFFIRM Annotated Transcripts, R.L. Bates and S.L. Gerhart (Ed.); USC Information Sciences Institute, Marina Del Rey, Calff, Feb. 1981.
	ANDE72	ANDERSON, J.P. "Computer security technology planning study," Tech. Rep ESD-TR-73-51, vols. 1 and 2, James P. Anderson and Co., Fort Washington, Pa., Oct. 1972.
	ANDR80	Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980 [doi>10.1145/357084.357088]
	BALD79	BALDAUF, D.L. "ACCAT Guard overview," Tech. Rep. MTR-3891, MITRE Corporation, Bedford, Mass., Nov. 1979.
	BELL74	BELL, D.E., AND LAPADULA, L.J. "Secure computer systems," Tech. Rep. ESD- TR-73-278, vols. 1-3, MITRE Corporation, Bedford, Mass., Nov. 1973 and June 1974.
	BOYE78	BOYER, R.S., AND MOORE, J.S. "A forreal semanttcs for the SRI hierarchmal design methodology," Computer Science Lab., SRI International, Menlo Park, Cahf., Nov. 1978.
	BOYE79a	BOYER, R.S., AND MOORE, J S. A computational logic, Academic Press, New York, 1979.
	BOYE79b	BOYER, R.S., AND MOORE, J.S. "A theorem-prover for recurslve functions: a user's manual," Tech. Rep. CSL-91, Computer Science Lab., SRI International, Menlo Park, Calif., June 1979.
	BOYE80	BOYER, R.S, AND MOORE, J S. "A verification condition generator for Fortran," Tech. Rep. CSL-103, Computer Science Lab., SRI International, Menlo Park, Calif, June 1980.
	CHEH80	CHEHEYL, M.H., GASSER, M., HUFF, G. A., AND MILLEN, J.K. "Secure system specification and verification: survey of methodologies," Tech. Rep. MTR-3904, MITRE Corporation, Bedford, Mass., Feb. 1980.
	DENN76	Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
	DENN77	Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
	EGGE80	EGGERT, P.R "Overview of the 'Ina Jo' specification language," Tech. Rep. SP- 4082, System Development Corporation, Santa Monica, Calif., Oct. 1980.
	ELSP72	Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972 [doi>10.1145/356599.356602]
	ELSP79	ELSPAS, B., GREEN, M W., MORICONI, M.S., SHOSTAK, R.E "A Jovial ventier," Interim Rep., SRI International, Menlo Park, Calif., June 1979.
	FEIE80	FEIERTAG, R.J. "A technique for proving specifications are multilevel secure," Tech Rep. CSL-109, Computer Science Lab, SRI International, Menlo Park, Calif., Jan. 1980.
	FLOY67	FLOYD, R.W. "Assigning meanings to programs," Math. Aspects Comput. Sci 19(1967), 19-32; available from American Mathematical Soc., Providence, R.I.
	GERH79a	GERHART, S.L., AND WILE, D.S. "Preliminary report on the delta experiment," Spectfications of Reliable Software, IEEE Catalog 79 CH 1401-9C, April 1979, pp. 198-211.
	GERH79b	GERHART, S.L. "Observations on AF- FIRM," (prepared for the Air Force Summer Study on Computer Security), June 26, 1974).
	GOOD77	GooD, D.I. (Ed.) "Constructing verifiably reliable and secure communications processing systems," Tech. Rep. ICSCA- CMP-6, Univ Texas at Austin, Jan. 1977.
	GOOD78a	GOOD, D.I., COHEN, R.M., AND HUNTER, L.W "A report on the development of Gypsy," Tech. Rep. ICSCA-CMP-13, Univ. Texas at Austin, Oct. 1978
	GOOD78b	GOOD, D.I, COHEN, R.M., HOCH, C.G, HUNTER, L.W., AND HARE, D.F. "Report on the language Gypsy, version 2.0," Tech. Rep ICSCA-CMP-10, Univ. Texas at Austin, Sept. 1978.
	GOOD79a	GOOD, D.I., COHEN, R.M., HOCH, C.G, HUNTER, L.W, AND HARE, D.F "Gypsy 2.0 programming system 6 0 user's manual," Certifiable Minicomputer Project, Univ. Texas at Austin, May 1979.
	GOOD79b	GOOD, D.I., COHEN, R.M., HOCH, C.G., HUNTER, L.W, AND HARE, D.F. "Gypsy 2.0 programming system 6.0 implementation variances," Certifiable Minicomputer Project, Univ. Texas at Austin, May 1979.
	GOOD79c	Donald I. Good , Richard M. Cohen , James Keeton-Williams, Principles of proving concurrent programs in Gypsy, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.42-52, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567757]
	GRAH72	GRAHAM, R.M, AND DENNING, P.J. "Protection--principles and practice," in Proc AFIPS 1972 Spring Jt Computer Conf, AFIPS Press, Arhngton, Va., 1972, pp. 417-429.
	GUTT77	Jhon V. Guttag , Ellis Horowitz , David R. Musser, Some extensions to algebraic specifications, Proceedings of an ACM conference on Language design for reliable software, p.63-67, March 28-30, 1977, Raleigh, North Carolina
	GUTT78	John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
	HOAR69	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	KALU76	Richard Alan Karp , David C. Luckham, Verification of fairness in an implementation of monitors, Proceedings of the 2nd international conference on Software engineering, p.40-46, October 13-15, 1976, San Francisco, California, United States
	KEMM80	KEMMERER, R. "FDM--a specification and verification methodology," in Proc 3rd Seminar on the Department of Delense Computer Security Inittative Program, Nat. Bur. Stand (Gaithersburg, Md.), Nov 1980
	LAMP71	LAMPSON, B.W. "Protection," in Proc. 5th Annual Princeton Conf Informatton Sctence and Systems, Pnnceton, N.J, March 1971, pp. 437-443.
	LAMP73	Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
	LEVI79	LEVITT, K N., ROBINSON, L., AND SIL- VERBERG, B.A. "The HDM handbook," vols. 1-3, Computer Science Lab., SRI International, Menlo Park, Cahf., June 1979.
	LOCA80	LOCASSO, R., SCHEID, J., SCHORRE, V, AND EGGERT, P. "The Ina Jo specification language reference manual," TM- (L)-/6021/001/00, System Development Corporation, Santa Momca, Calif., June 1980.
	LOND77	LONDON, R L. "Perspectives on program verification," in Current Trends tn Programming Methodology, Vol. 2: Program Validation, R.T. Yeh, (Ed.), Prentice-Hall, Englewood Cliffs, N.J., 1977, pp 151-172.
	LUCK77	LUCKHAM, D.C. "Program verification and verification-oriented programming," in Informatton Processing 77, American Elsevier, N.Y., 1977, pp. 783-793.
	LUSU77	LUCKHAM, D.C., AND SUZUKI, N. "Automatic program verification IV. proof of termination within a weak logic of programs," Acta Inf 8 (1977), 21-36
	LUSU79	David C. Luckham , Norihisa Suzuki, Verification of Array, Record, and Pointer Operations in Pascal, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.226-244, Oct. 1979 [doi>10.1145/357073.357078]
	McCA79	McCAULEY, E.J., AND DRONGOWSKI, P.J. "KSOS--the design of a secure operating system," in Proc. 1979 AFIPS Nat Computer Conf., AFIPS Press, Arhngton, Va, pp. 345-353.
	MILL76	Jonathan K. Millen, Security Kernel validation in practice, Communications of the ACM, v.19 n.5, p.243-250, May 1976 [doi>10.1145/360051.360059]
	MILL79	MILLEN, J.K. "Operating system security verification," Tech. Rep. M79-223, MITRE Corporation, Bedford, Mass., Sept. 1979.
	MILL81	MILLEN, J K, "Information flow analysis of formal specifications," in Proc. IEEE 1981 Symp. Securtty and Privacy, April 1981.
	MORI77	MORICONI, M.S. "A system of incrementally designing and verifying programs," Tech. Rep. ICSCA-CMP-9, Univ. Texas at Austin, Dec. 1977.
	MORI80	MORICONI, M., SCHWARTZ, R.L. "Automatic construction of verification condition generators from Hoare logics," Tech. Rep CSL-125, Computer Science Lab., SRI International, Menlo Park, Calif., Nov. 1980.
	MUSS80	MUSSER, DR. "Abstract data type specification in the AFFIRM system," IEEE Trans. Softw Eng. SE-6, 1 (Jan. 1980), 24-32
	NEUM77	NEUMANN, P G, BOYER, R.S., FEIERTAG, R J , LEVITT, K N, AND ROBINSON, L. "A provably secure operating system: the system, its apphcatlons, and proofs," Stanford Research Institute, Menlo Park, Cahf., Feb. 1977.
	PARN72	D. L. Parnas, A technique for software module specification with examples, Communications of the ACM, v.15 n.5, p.330-336, May 1972 [doi>10.1145/355602.361309]
	POLA79	POLAK, W. "An exercise In automatic program verification," IEEE Trans Softw. Eng. SE-5, 5 (Sept. 1979), 453- 458
	ROBI77	Lawrence Robinson , Karl N. Levitt, Proof techniques for hierarchically structured programs, Communications of the ACM, v.20 n.4, p.271-283, April 1977 [doi>10.1145/359461.359483]
	SCHA80	SCHAEFER, M. "KVM/370. its evolution and status," in EASCON'80 Rec, Sept. 1980.
	SCHE73	SCHELL, R.R., DOWNEY, P J., AND PO- PEK, G.J. "Preliminary notes on the design of secure military computer systems," Tech. Rep MCI-73-1, USAF Electronic Systems Div, L.G Hanscom Field, Bedford, Mass., Jan. 1973
	SCHO80	SCHORRE, V., AND STEIN, J "The rateractive theorem prover (ITP) user manual," Tech Rep. TM-6889/000/01, System Development Corporation, Santa Monica, Calif., Nov 1980
	SNYD81	SNYDER, L "Formal models of capability-based protection systems," IEEE Trans. Computers C-30, 3 (March 1981), 172-181.
	THOM81	THOMPSON, D.H., SUNSHINE, C.A., ER- ICKSON, R.W., GERHART, S L., AND SCHWABE, D. "Specification and verification of communication protocols in AF- FIRM using state transition models," Tech. Rep. ISI/RR-81-88, USC Information Sciences Institute, Feb. 1981.
	VERK80	Workshop on formal verification: (VERkshop), ACM SIGSOFT Software Engineering Notes, v.5 n.3, p.4-47, July 1980 [doi>10.1145/1005913.1005914]
	WALK80	Bruce J. Walker , Richard A. Kemmerer , Gerald J. Popek, Specification and verification of the UCLA Unix security kernel, Communications of the ACM, v.23 n.2, p.118-131, Feb. 1980 [doi>10.1145/358818.358825]
	WALT74	WALTER, K G, OGDEN, W.F, ROUNDS, W.C., BRADSHAW, F.T., AMES, S R., AND SHUMWAY, D.G. "Primitive models for computer security," Tech. Rep. ESD- TR-74-117, Case Western Reserve Univ., Cleveland Ohio, Jan 1974; ASTIA Doc. 778 467.
	WEIS69	WEISSMAN, C. "Security controls in the ADEPT-50 time-sharing system," in Proc. AFIPS 1969 Fall Jt. Computer Conf, AFIPS Press, Arlington, Va, 1969, pp. 119-133
	WENS78	WENSLEY, J H., LAMPORT, L, GOLD- BERG, J., GREEN, M W., LEVITT, K.N, MELLIAR-SMITH, P.M., SHOSTAK, R.E., WEINSTOCK, C.B. "SIFT" design and analysts of a fault-tolerant computer from aircraft control," Proc. IEEE 66, 10 (Oct. 1978), 1240-1254

CITED BY 12

	Jonathan M. Silverman, Reflections on the verification of the security of an operating system kernel, ACM SIGOPS Operating Systems Review, v.17 n.5, p.143-154, October 1983
	Paul Eggert, Toward special-purpose program verification, ACM SIGSOFT Software Engineering Notes, v.15 n.4, p.25-29, Sep. 1990
	Armen Gabrielian , Matthew K. Franklin, Multilevel specification of real time systems, Communications of the ACM, v.34 n.5, p.50-60, May 1991
	Paul R Eggert , D Val Schorre, Logic enhancement: A method for extending logic programming languages, Proceedings of the 1982 ACM symposium on LISP and functional programming, p.74-80, August 15-18, 1982, Pittsburgh, Pennsylvania, United States
	A. Gabrielian , M. K. Franklin, Multi-level specification and verification of real-time software, Proceedings of the 12th international conference on Software engineering, p.52-62, March 26-30, 1990, Nice, France
	Rein Turn, Security and privacy requirements in computing, Proceedings of 1986 ACM Fall joint computer conference, p.1106-1114, November 1986, Dallas, Texas, United States
	J. Kljaich, Jr. , B. T. Smith , A. S. Wojcik, Formal Verification of Fault Tolerance Using Theorem-Proving Techniques, IEEE Transactions on Computers, v.38 n.3, p.366-376, March 1989
	Donald MacKenzie, The Automation of Proof: A Historical and Sociological Exploration, IEEE Annals of the History of Computing, v.17 n.3, p.7-29, September 1995
	Donald Mackenzie , Garrel Pottinger, Mathematics, Technology, and Trust: Formal Verification, Computer Security, and the U.S. Military, IEEE Annals of the History of Computing, v.19 n.3, p.41-59, July 1997
	Timothy Fraser , Nick L. Petroni, Jr. , William A. Arbaugh, Applying flow-sensitive CQUAL to verify MINIX authorization check placement: 3, Proceedings of the 2006 workshop on Programming languages and analysis for security, June 10-10, 2006, Ottawa, Ontario, Canada
	D. Craigen , S. Kromodimoeljo , I. Meisels , A. Neilson , B. Pase , M. Saaltink, m-EVES: A tool for verifying software, Proceedings of the 10th international conference on Software engineering, p.324-333, April 11-15, 1988, Singapore
	R. C. Summers, An overview of computer security, IBM Systems Journal, v.23 n.4, p.309-325, December1984