{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:31Z","timestamp":1761611131861,"version":"3.28.0"},"reference-count":50,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/csac.2003.1254326","type":"proceedings-article","created":{"date-parts":[[2004,7,8]],"date-time":"2004-07-08T20:05:44Z","timestamp":1089317144000},"page":"208-216","source":"Crossref","is-referenced-by-count":13,"title":["PSOS revisited"],"prefix":"10.1109","author":[{"given":"P.G.","family":"Neumann","sequence":"first","affiliation":[]},{"given":"R.J.","family":"Feiertag","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"journal-title":"Naming and protection in extendible operating systems","year":"1974","author":"redell","key":"ref39"},{"key":"ref38","doi-asserted-by":"crossref","DOI":"10.1109\/SP.1986.10000","article-title":"Security in KeyKOS","author":"rajunas","year":"1986","journal-title":"Proc 1986 IEEE Symp on Security and Privacy"},{"key":"ref33","article-title":"A Provably Secure Operating System: The system, its applications, and proofs","author":"neumann","year":"1980","journal-title":"Technical Report Computer Science Laboratory SRI International"},{"key":"ref32","article-title":"Principled assuredly trustworthy composable architectures","author":"neumann","year":"0","journal-title":"Technical report Computer Science Laboratory SRI International Menlo Park California 2003 Final report SRI Project 11459"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/DISCEX.2003.1194962"},{"key":"ref30","article-title":"Design verification of SIFT","author":"moser","year":"1987","journal-title":"Contractor Report 4097 NASA Langley Research Center"},{"key":"ref37","first-page":"146","article-title":"An overview of the Kernelized Secure Operating System (KSOS)","author":"perrine","year":"1984","journal-title":"Proceedings of the Seventh DoD\/NBS Computer Security Initiative Conference"},{"key":"ref36","article-title":"GASSP: Generally Accepted Systems Security Principles","author":"ozier","year":"1997","journal-title":"Technical report International Information Security Foundation"},{"key":"ref35","article-title":"Theory interpretations in PVS","author":"owre","year":"2001","journal-title":"Technical Report SRI SRI-CSL-01–01 Computer Science Laboratory SRI International"},{"journal-title":"The Multics System An Examination of its Structure","year":"1972","author":"organick","key":"ref34"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1982.1676059"},{"key":"ref27","first-page":"345","article-title":"KSOS: The design of a secure operating system","volume":"48","author":"mccauley","year":"1979","journal-title":"AFIPS Conference Proceedings"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243130"},{"key":"ref2","first-page":"365","article-title":"KSOS: Development methodology for a secure operating system","volume":"48","author":"berson","year":"1979","journal-title":"AFIPS Conference Proceedings"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/48012.48041"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1986.10001"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1984.10001"},{"key":"ref21","article-title":"Improving Security and Performance for Capability Systems","author":"karger","year":"1988","journal-title":"Technical Report No 149"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/362375.362389"},{"key":"ref23","article-title":"On reliable and extendible operating systems","author":"lampson","year":"1969","journal-title":"NATO"},{"key":"ref26","article-title":"Operating system structures to support security and reliable software","volume":"5","author":"linden","year":"1973","journal-title":"ACM Computing Surveys"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360074"},{"key":"ref50","first-page":"142","article-title":"Proving a computer system secure","volume":"6","author":"young","year":"1985","journal-title":"Computer Network Security"},{"key":"ref10","article-title":"A mechanically verified compiling specification for a realistic compiler","author":"dold","year":"2002","journal-title":"Technical report UIB 03–02 Universitat Ulm Fakultät für Informatik"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/361011.361070"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/359461.359483"},{"key":"ref12","article-title":"A technique for proving specifications are multilevel secure","author":"feiertag","year":"1980","journal-title":"Technical Report CSL-109 Computer Science Laboratory SRI International"},{"key":"ref13","first-page":"329","article-title":"The foundations of a Provably Secure Operating System (PSOS)","author":"feiertag","year":"1979","journal-title":"In Proceedings of the National Computer Conference"},{"key":"ref14","article-title":"An overview of the LOCK FTLS","author":"fine","year":"1988","journal-title":"Honeywell Technical Report"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1984.10019"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1989.36277"},{"key":"ref18","article-title":"Top level security properties for the LOCK system","author":"haigh","year":"1988","journal-title":"Honeywell Technical Report"},{"key":"ref19","first-page":"232","article-title":"Extending the noninterference model of MLS for SAT","author":"haigh","year":"1986","journal-title":"IEEE Computer Society"},{"key":"ref4","article-title":"A practical alternative to hierarchical integrity policies","author":"boebert","year":"1985","journal-title":"Proceedings of the Eighth DoD\/NBS Computer Security Initiative Conference"},{"key":"ref3","article-title":"Integrity considerations for secure computer systems","author":"biba","year":"1975","journal-title":"Technical Report MTR-3153 MITRE Corporation Bedford MA"},{"key":"ref6","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1145\/114669.114686","article-title":"On building systems that will fail (1990 Turing Award Lecture, with a following interview by Karen Frenkel","volume":"34","author":"corbat\u00f3","year":"1991","journal-title":"Communications of the ACM"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1145\/323627.323645"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/1463891.1463915"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/363095.363139"},{"journal-title":"The Cambridge CAP Computer and Its Operating System","year":"1979","author":"wilkes","key":"ref49"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/363095.363143"},{"journal-title":"Fortress Rochester The Inside Story of the IBM iSeries","year":"2001","author":"soltis","key":"ref46"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/52.976938"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1978.11114"},{"journal-title":"Mechanical Verification of Compiler Correctness","year":"1998","author":"stringer-calvert","key":"ref47"},{"key":"ref42","article-title":"The HDM Handbook","author":"robinson","year":"1979","journal-title":"Computer Science Laboratory SRI International"},{"key":"ref41","first-page":"61","article-title":"A formal methodology for the design of operating system software","author":"robinson","year":"1977","journal-title":"Current Trends in Programming Methodology"},{"key":"ref44","first-page":"129","article-title":"LOCKing computers securely","author":"saydjari","year":"1987","journal-title":"10th National Computer Security Conf"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1975.9939"}],"event":{"name":"19th Annual Computer Security Applications Conference, 2003.","location":"Las Vegas, Nevada, USA"},"container-title":["19th Annual Computer Security Applications Conference, 2003. Proceedings."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/8882\/28060\/01254326.pdf?arnumber=1254326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T08:39:27Z","timestamp":1497602367000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1254326\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":50,"URL":"https:\/\/doi.org\/10.1109\/csac.2003.1254326","relation":{},"subject":[]}}