Formal Models for Computer Security

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.

	AMES78	AMES, S R., AND OESTREICHER, D. R "Design of a message processing system for a multilevel secure environment," m Proc AFIPS Nat Computer Conf., vol. 47, AFIPS Press, Arhngton, Va, 1978, pp. 765-771.
	AMES80	AMES, S R, AND KEETON-WILLIAMS, J. G "Demonstrating security for trusted apphcatlons on a security kernel," MITRE Corp, Bedford, Mass., April 1980
	ANDE72	ANDERSON, J P. "Computer security techno\|ogy planning study," ESD-TR- 73-51, vol 1, ESD/AFSC, Hanscom AFB, Bedford, Mass., Oct. 1972 (NTIS AD-758 2O6)
	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]
	BELL73a	BELL, D E, AND LAPADULA, L J. "Secure computer systems" Mathematical foundations," ESD-TR-73-278, vol. 1, ESD/AFSC, Hanscom AFB, Bedford, Mass., Nov. 1973 (MTR-2547, vol. 1, MITRE Corp., Bedford, Mass.)
	BELL73b	BELL, D. E., AND LAPADULA, L. J "Secure computer systems' A mathematmal model," ESD-TR-73-278, vol. 2, ESD/AFSC, Hanscom AFB, Bedford, Mass., Nov. 1973 (MTR-2547, vol 2, MITRE Corp., Bedford, Mass.}.
	BELL74a	BELL, D. E. "Secure computer systems: A refinement of the mathematmal model," ESD-TR-73-278, vol. 3, ESD/ AFSC, Hanscom AFB, Bedford, Mass, April 1974 (MTR 2547, vol. 3, MITRE Corp., Bedford, Mass.}.
	BELL74b	BELL, D. E, AND LAPADULA, L. J. "Secure computer systems. Mathematical foundations and model," M74-244, MITRE Corp, Bedford, Mass., Oct, 1974.
	BELL75	BELL, D. E., AND LAPADULA, L. J, "Secure computer system. Unified exposition and multms interpretatmn," MTR-2997, MITRE Corp., Bedford, Mass., July 1975.
	BIBA77	BIBA, K. J. "Integrity considerations for secure computer systems," ESD-TR- 76-372, ESD/AFSC, Hanscom AFB, Bedford, Mass., April 1977 (MITRE MTR-3153, NTIS AD A039324)
	BIRK70	BIRKHOFF, G., AND BARTER, T. C. Modern Applied Algebra, McGraw-Hill, New York, 1970, p. 260.
	BISH79	Matt Bishop , Lawrence Snyder, The transfer of information and authority in a protection system, Proceedings of the seventh ACM symposium on Operating systems principles, p.45-54, December 10-12, 1979, Pacific Grove, California, United States [doi>10.1145/800215.806569]
	BONN80	BONNEAU, C. H "Secure commumcations processor kernel software, detailed specification, part I, rev. D," Honeywell Inc, Aviomcs Diwsion, St. Petersburg, Fla., 1980.
	BONY78	BONYUN, D. "A new model of computer security with integrity and aggregation considerations," I. P. Sharp Assoc, Ottawa, Ont., Canada, March 1978
	BOYE79	BOYER, R. S., AND MOORE, J. S. "A theorem-prover for recursive functions A user's manual," Tech. Rep. CSL-91, SRI International, MeMo Park, Calif, June 1979.
	COHE77	Ellis Choen, Information transmission in computational systems, Proceedings of the sixth ACM symposium on Operating systems principles, p.133-139, November 16-18, 1977, West Lafayette, Indiana, United States
	COHE78	COHEN, E. "Information transmmmon in sequential programs," in Foundatmns of secure computatmn, R. A. DeMillo, D. P, Dobkin, A. K Jones, and R. J. Lipton (Eds.), Academic Press, New York, 1978, pp. 297-336.
	DEMI77	DEMILLO, R. A., DOBKIN, D, AND LIP- TON, R.J. "Even databases that lie can be compromised," IEEE Trans Softw. Eng. SE-4, 1 (Jan. 1977), 74-75.
	DENN71	Peter J. Denning, Third Generation Computer Systems, ACM Computing Surveys (CSUR), v.3 n.4, p.175-216, Dec. 1971 [doi>10.1145/356593.356595]
	DENN75	Dorothy Elizabeth Robling Denning, Secure information flow in computer systems., 1975
	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]
	DENN79a	Dorothy E. Denning , Peter J. Denning , Mayer D. Schwartz, The tracker: a threat to statistical database security, ACM Transactions on Database Systems (TODS), v.4 n.1, p.76-96, March 1979 [doi>10.1145/320064.320069]
	DENN79b	Dorothy E. Denning , Peter J. Denning, Data Security, ACM Computing Surveys (CSUR), v.11 n.3, p.227-249, Sept. 1979 [doi>10.1145/356778.356782]
	DOBK79	David Dobkin , Anita K. Jones , Richard J. Lipton, Secure databases: protection against user influence, ACM Transactions on Database Systems (TODS), v.4 n.1, p.97-106, March 1979 [doi>10.1145/320064.320068]
	FEIE77	R. J. Feiertag , K. N. Levitt , L. Robinson, Proving multilevel security of a system design, Proceedings of the sixth ACM symposium on Operating systems principles, p.57-65, November 16-18, 1977, West Lafayette, Indiana, United States
	FEIE79	FEIERTAG, R. J, AND NEUMANN, P G. "The foundations of a provably secure operating system (PSOS)," in Proc AF- IPS Nat. Computer Conf., vol. 48, AFIPS Press, Arlington, Va, 1979, pp. 329-334.
	FENT74	FENTON, J. S. "Memoryless subsystems," Comput. J 17, 2 (May 1974), 143- 147.
	FURT78a	FURTEK, F C. "A validation technique for computer security based on the theory of constraints," ESD-TR-78-182, ESD/AFSC, Hanscom AFB, Bedford, Mass., Dec 1978 (MITRE MTR-3661, NTIS ADA065111).
	FURT78b	FURTEK, F C. "Constraints and compromise," in Foundations of secure computatmn, R. A. DeMillo, D. P Dobkin, A K. Jones, and R. J. Lipton (Eds.), Academic Press, New York, 1978, pp. 189-204.
	FURT79	FURTEK, F C. "Doing without values," Proc. 9th Int. Syrup. Multiple-Valued Logic, April 1979, pp. 114-120 (IEEE Cat. no. CH1408-4C).
	FURT80	FURTEK, F C. "Specification and verification of real-time, distributed systems using the theory of constraints," Tech Rep. P-1027, Charles Stark Draper Laboratory, Cambridge, Mass., April 1980.
	GNOS80	"GNOSIS External Specifications," Tymshare, Cupertino, Calif., 1980
	GOLD79	GOLD, B. D, LINDE, R. R., PEELER, R. J, SCHAEFER, M., SCHEID, J. F., AND WARD, P D. "A security retrofit of VM/370," m Proc. AFIPS Nat. Computer Conf., vol. 48, AFIPS Press, Arlington, Va., 1979, pp 335-342
	GRAH72	GRAHAM, G S., AND DENNING, P. J. "Protectlon--Pnnciples and practice," in Proc 1972 AFIPS Spr~ng Jt Computer Conf, vol. 40, AFIPS Press, Arhngton, Va, pp. 417-429.
	GROH76	GROHN, M.j. "A model of a protected data management system," ESD-TR-76- 289, ESD/AFSC, Hanscom AFB, Bedford, Mass, June i976 (I P. Sharp, Ottawa, Canada NTIS ADA 035256).
	HARR76	Michael A. Harrison , Walter L. Ruzzo , Jeffrey D. Ullman, Protection in operating systems, Communications of the ACM, v.19 n.8, p.461-471, Aug. 1976 [doi>10.1145/360303.360333]
	HINK75	HINKE, T. H., AND SCHAEFER, M. "Secure data management system," RADC-TR-75-266, Rome Air Dev. Center, AFSC, GriffiNS AFB, N Y., Nov 1975 (NTIS AD A019201)
	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]
	JONE75	Anita K. Jones , Richard J. Lipton, The enforcement of security policies for computation, Proceedings of the fifth ACM symposium on Operating systems principles, p.197-206, November 19-21, 1975, Austin, Texas, United States
	JONE76	JONES, A. K., LIPTON, R. J, AND SNY- DER, L. "A linear time algorithm for deciding subJect-object secumty," Proc 17th Ann Foundatmns Computer Sct Conf., Houston, Tex., 1976, pp. 33-41.
	JONE78a	JONES, A K. "Protection mechamsm models: Their usefulness," m Foundatmns of secure computatmn, R A. DeMiUo, D. P Dobkin, A. K. Jones, and R. J Lipton (Eds.), Academm Press, New York, I978, pp, 237-254.
	JONE78b	JONES, A. K., AND LIPTON, R.J. "The enforcement of security policies for computation," J. Compt. Syst. Sc~, 17, 1 (Aug. 1978), 35-55.
	KEMM79	Richard Allen Kemmerer, Formal verification of the ucla security kernel: abstract model, mapping functions, theorem generation, and proofs., 1979
	KSOS78	"KSOS Verification Plan," WDL- TR7809, Ford Aerospace and Communications Corp, Western Development Lab. Div., Palo Alto, Calif., and SRI International, Menlo Park, Cahf, 1978.
	LAMP71	LAMPSON, B W. "Protectmn," m Proc. 5th Princeton Syrup. Informatwn Sciences and Systems (March 1971), pp 437-443, reprinted m A CM SIGOPS Operating Syst Rev 8, 1 (Jan 1974), 18-24.
	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]
	LAND80	LANDWEHR, C E. "Assertions for verification of multilevel secure military message systems," contribution to Workshop on Formal Verification, SRI International, Menlo Park, Calif., April 1980; reprinted in A CM Softw Eng. Notes 5, 3 (July 1980), 46-47
	LIPT77	R. J. Lipton , L. Snyder, A Linear Time Algorithm for Deciding Subject Security, Journal of the ACM (JACM), v.24 n.3, p.455-464, July 1977 [doi>10.1145/322017.322025]
	MCCA79	MCCAULEY, E. J., AND DRONGOWSKI, P.J. "KSOS: The design of a secure operating system," in Proc. AFIPS Nat Computer Conf., vol 48, AFIPS Press, Arlington, Va., 1979, 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]
	MILL78a	MILLEN, J. K "An example of a formal flow violation," in Proc IEEE Computer Soc. 2nd Int. Computer Software and Apphcatmns Conf, Nov 1978, pp. 204- 208
	MILL78b	MILLEN, J.K. "Constraints and multilevel security," m Foundatwns of Secure Computatmn, R A. DeMfllo, D. P. Dobkin, A. K. Jones, and R. J. Lipton (Eds.), Academm Press, New York, 1978, pp 205-222.
	MILL78c	MILLEN, J. K "Causal system security," ESD-TR-78-17t, ESD/AFSC, Hanscom AFB, Bedford, Mass., Oct. 1978 (MITRE MTR-3614).
	NEUM77	NEUMANN, P. G., BOYER, R. S., FEIER- TAG, R J., LEVITT, K. N., AND ROBIN- SON, L "A provably secure operating system. The system, its applications, and proofs," SRI International, Menlo Park, Calif., Feb. 1977.
	OPNA79	OPNAVINST 5239.1, Department of the Navy, Chmf of Naval Operations, Op- 942E, April 2, 1979.
	ORGA72	Elliott I. Organick, The Multics System: An Examination of Its Structure, The MIT Press, 1972
	PARN74	PARNAS0 D L., AND PRICE, W. R. "Using memory access control as the only protection mechanism," in Proc. Int Workshop Protection tn Operating Systems, IRIA/LABORIA, Rocquencourt, France, Aug, 1974, 177-181.
	POPE73	POPEK, G.J. "Access control models," ESD-TR-73-106 ESD/AFSC, L. G Hanscom Field, Bedford, Mass, Feb 1973 (NTIS AD-761 807).
	POPE75	Gerald J. Popek , Charles S. Kline, A verifiable protection system, Proceedings of the international conference on Reliable software, p.294-304, April 21-23, 1975, Los Angeles, California
	POPE78a	Gerald J. Popek , David A. Farber, A model for verification of data security in operating systems, Communications of the ACM, v.21 n.9, p.737-749, Sept. 1978 [doi>10.1145/359588.359597]
	POPE78b	POPEK, G J., KLINE, C. S., AND WAL- TON, E, J. "UCLA Secure Unix," UCLA Tech Rep. (Draft), Feb. 1978.
	POPE79	POPEK, G. J., KAMPE, M., KLINE, C. S, STOUGHTON, A, URBAN, M., AND WAL- TON, E J. "UCLA secure Unix," in Proc. AFIPS Nat. Computer Conf., vol. 48, AFIPS Press, Arhngton, Va., 1979, pp 355-364.
	PRIC73	William Robert Price, Implications of a virtual memory mechanism for implementing protection in a family of operating systems, 1973
	REIT79	Richard P. Reitman, A mechanism for information control in parallel systems, Proceedings of the seventh ACM symposium on Operating systems principles, p.55-63, December 10-12, 1979, Pacific Grove, California, United States [doi>10.1145/800215.806570]
	ROUB77	ROUBINE, 0., AND ROBINSON, L "SPECIAL reference manual," 3rd ed, SRI International, Menlo Park, Calif., 1977.
	SCHE73	SCHELL, R. R., DOWNEY, P. J, AND POPES, G.J. "Preliminary notes on the design of secure military computer systems," MCI-73-1, ESD/AFSC, Hanscom AFB, Bedford, Mass., Jan. 1973
	SCHI75	SCHILLER, W L. "The design and specification of a security kernel for the PDP- 11/45," ESD-TR-75-69, MITRE Corp., Bedford, Mass, March 1975.
	SCHR77	Michael D. Schroeder , David D. Clark , Jerome H. Saltzer, The Multics kernel design project, Proceedings of the sixth ACM symposium on Operating systems principles, p.43-56, November 16-18, 1977, West Lafayette, Indiana, United States
	SCHW79	M. D. Schwartz , D. E. Denning , P. J. Denning, Linear queries in statistical databases, ACM Transactions on Database Systems (TODS), v.4 n.2, p.156-167, June 1979 [doi>10.1145/320071.320073]
	SNYD77	Lawrence Snyder, On the synthesis and analysis of protection systems, Proceedings of the sixth ACM symposium on Operating systems principles, p.141-150, November 16-18, 1977, West Lafayette, Indiana, United States
	SNYD79	SNYDER, L. "Formal models of capability-based protectmn systems," Tech Rep 151, Dept. Computer Scmnce, Yale Univ., New Haven, Conn, April 1979.
	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. "Primmve models for computer security," ESD- TR-4-117, AF/ESD, Hanscom AFB, Bedford, Mass., Jan., 1974 (NTIS AD- 778 467).
	WALT75a	K. G. Walter , S. I. Schaen , W. F. Ogden , W. C. Rounds , D. G. Shumway , D. D. Schaeffer , K. J. Biba , F. T. Bradshaw , S. R. Ames , J. M. Gilligan, Structured specification of a Security Kernel, Proceedings of the international conference on Reliable software, p.285-293, April 21-23, 1975, Los Angeles, California
	WALT75b	WALTER, K. G, OGDEN, W. V., GILLI- GAN, J. M., SCHAEFFER, D. D, SCHAEN, S I., AND SHUMWAY, D. G. "Inmal structured specifications for an uncompromlsable computer security system," ESD-TR-75-82, ESD/AFSC, Hanscom AFB, Bedford, Mass., July 1975 (NTIS AD-A022 490).
	WEIS69	WEISSMAN, C. "Security controls in the ADEPT-50 time sharing system," Proc. 1969 AFIPS Fall Jt Computer Conf., vol. 35, AFIPS Press, Arlington, Va., pp. 119-133.
	WILS79	WILSON, S H., KALLANDER, J. W., THOMAS, N M, III, KLITZKIE, L. C., AND BUNCH, J. R., JR. "Military message expemment quick look report," NRL Memorandum Rep. 3992, Naval Research Lab., Washington, D.C., April 1979, p. 10.
	WITH79	WITHINGTON, P.T. "The trusted function m secure decentrahzed processing," MITRE MTR-3892, MITRE Corp., Bedford, Mass, Sept. 1979.
	YONK76	YONKE, M. D "The XIVUS environment XIVUS working paper no. 1," USC/Information Sciences Institute, Marina del Rey, Calif., April 1976.