@article{barton:b5000,
  title = {Discussion: The Burroughs {B 5000} in Retrospect}, 
  author = {R. S. Barton and H. Berce and G. A. Collins and B. A. Creech and D. M. Dahm and
        B. A. Dent and V. J. Ford and B. A. Galler and J. E. S. Hale and E. A. Hauck and
        J. T. Hootman and P. D. King and N. L. Kreuder and W. R. Lonergan and D.
        MacDonald and F. B. MacKenzie and C. Oliphint and R. Pearson and R. F. Rosin and
        L. D. Turner and R. Waychoff}, 
  journal = {Annals of the History of Computing}, 
  volume = {9}, 
  number = {1}, 
  year = {1987}, 
  month = {January}, 
  pages = {37--92}, 
  doi = {10.1109/MAHC.1987.10006}, 
  www_section = {Hardware}, 
  issn = {0164-1239}, 
}

@techreport{bell:seccompsys,
  title = {Secure Computer System: Unified Exposition and {Multics} Interpretation}, 
  author = {D.E. Bell and L.J. La Padula}, 
  institution = {The Mitre Corporation}, 
  number = {ESD-TR-75-306}, 
  year = {1976}, 
  month = {March}, 
  address = {Bedford, Massachusetts}, 
  www_section = {Theory}, 
}

@inproceedings{boebert:inability,
  title = {On the inability of an unmodified capability machine to enforce the *-property}, 
  author = {E. Boebert, W}, 
  booktitle = {Proceedings of the 7th DOD/NBS Computer Security Conference}, 
  year = {1984}, 
  month = {September}, 
  www_html_url = {http://zesty.ca/capmyths/boebert.html}, 
  www_section = {Theory}, 
}

@article{carter:mmachine94,
  title = {Hardware Support for Fast Capability-based Addressing}, 
  author = {Carter, Nicholas P. and Keckler, Stephen W. and Dally, William J.}, 
  journal = {SIGPLAN Not}, 
  volume = {29}, 
  number = {11}, 
  year = {1994}, 
  month = {November}, 
  address = {New York, NY, USA}, 
  pages = {319--327}, 
  publisher = {ACM}, 
  www_pdf_url = {https://www.cs.utexas.edu/users/skeckler/pubs/asplos94.pdf}, 
  issn = {0362-1340}, 
  www_section = {Hardware}, 
  doi = {10.1145/195470.195579}, 
}

@inproceedings{chisnall:cpdp11,
  title = {Beyond the {PDP}-11: Architectural support for a memory-safe C abstract
        machine}, 
  author = {David Chisnall and Colin Rothwell and Brooks Davis and Robert Watson and
        Jonathan Woodruff and Simon Moore and Peter G. Neumann and Michael Roe}, 
  booktitle = {Proceedings of the Fifteenth Edition of ASPLOS on Architectural Support for
        Programming Languages and Operating Systems}, 
  year = {2014}, 
  address = {New York, NY, USA}, 
  location = {Istanbul, Turkey}, 
  publisher = {ACM}, 
  series = {ASPLOS XX}, 
  www_pdf_url = {https://www.cl.cam.ac.uk/~dc552/papers/asplos15-memory-safe-c.pdf}, 
  keywords = {C, memory safety, memory models, code generation}, 
  www_section = {Hardware / CHERI}, 
}

@inproceedings{cohen:hydraprotect,
  title = {Protection of the {Hydra} Operating System}, 
  author = {E. Cohen and D. Jefferson}, 
  booktitle = {Proceedings of the Fifth ACM Symposium on Operating Systems Principles}, 
  year = {1975}, 
  pages = {141--160}, 
  www_section = {Operating Systems / HYDRA}, 
}

@inproceedings{davis2019:cheriabi,
  title = {{CheriABI}: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege
        in the {POSIX} {C} Run-time Environment}, 
  author = {Brooks Davis and Robert N. M. Watson and Alexander Richardson and Peter Neumann
        and Simon Moore and John Baldwin and David Chisnall and Jessica Clarke and
        Nathaniel Wesley Filardo and Khilan Gudka and Alexandre Joannou and Ben Laurie
        and A. Theodore Markettos and Ed Maste and Alfredo Mazzinghi and Edward Tomasz
        Napierala and Robert Norton and Michael Roe and Peter Sewell and Stacey Son and
        Jonathan Woodruff}, 
  booktitle = {Proceedings of the 24nd ACM International Conference on Architectural
        Support for Programming Languages and Operating Systems (ASPLOS 2019)}, 
  year = {2019}, 
  month = {April}, 
  www_pdf_url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/201904-asplos-cheriabi.pdf},
  www_section = {Operating Systems}, 
}

@book{denning:cap,
  title = {The {Cambridge} {CAP} {Computer} and {Its} {Operating} {System}}, 
  author = {Wilkes, Maurice Vincent and Needham, Roger Michael and Denning, Peter J.}, 
  number = {6}, 
  year = {1979}, 
  editor = {Peter J. Denning}, 
  publisher = {Elsevier North Holland}, 
  series = {Operating and {Programming} {Systems} {Series}}, 
  isbn = {0-444-00357-6}, 
  www_section = {Hardware / CAP, Operating Systems}, 
  www_tags = {selected}, 
  www_pdf_url = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/cap.pdf},
}

@article{dennis:multiprogram,
  title = {Programming Semantics for Multiprogrammed Computations}, 
  author = {Dennis, Jack B. and Van Horn, Earl C.}, 
  journal = {Commun. ACM}, 
  volume = {9}, 
  number = {3}, 
  year = {1966}, 
  month = {March}, 
  address = {New York, NY, USA}, 
  pages = {143--155}, 
  publisher = {Association for Computing Machinery}, 
  issn = {0001-0782}, 
  doi = {10.1145/365230.365252}, 
  www_section = {Theory}, 
}

@phdthesis{doerrie:confidence,
  title = {Confidence in {Confinement}: {An} {Axiom}-free, {Mechanized} {Verification} of
        {Confinement} in {Capability}-based {Systems}}, 
  author = {Doerrie, M. Scott}, 
  year = {2015}, 
  shorttitle = {Confidence in {Confinement}}, 
  www_section = {Theory}, 
  www_pdf_url = {http://www.doerrie.us/assets/doerrie-dissertation-jhu.pdf}, 
}

@inproceedings{drossopoulou:cappolicies,
  title = {The {Need} for {Capability} {Policies}}, 
  author = {Drossopoulou, Sophia and Noble, James}, 
  booktitle = {Proceedings of the 15th {Workshop} on {Formal} {Techniques} for {Java}-like
        {Programs}}, 
  year = {2013}, 
  address = {New York, NY, USA}, 
  pages = {6:1--6:7}, 
  publisher = {ACM}, 
  series = {{FTfJP} '13}, 
  doi = {10.1145/2489804.2489811}, 
  isbn = {978-1-4503-2042-9}, 
  abstract = {The object-capability model is one of the industry standards adopted for the
        implementation of security policies for web-based software. Object-capabilities
        in various forms are supported by programming languages such as E, Joe-E,
        Newspeak, Grace, and the newer versions of Javascript. Unfortunately, code
        written using capabilities tends to concentrate on the low-level mechanism rather
        than the high-level policy. In this position paper, we argue that current
        specification methodologies cannot adequately capture all aspects of the
        capability policies required to support object-capability systems. We outline
        informally the features that such security policies should support, and we
        demonstrate (also informally) how we can reason that examples satisfy the
        capability policies}, 
  www_section = {Theory}, 
  keywords = {security, Java, Grace, JavaScript, object-capability security}, 
}

@inproceedings{fabry:caseforcapabilities,
  title = {The case for capability based computers (Extended Abstract)}, 
  author = {Fabry, R. S.}, 
  booktitle = {Proceedings of the Fourth ACM Symposium on Operating System Principles
        1973}, 
  year = {1973}, 
  address = {New York, NY, USA}, 
  publisher = {ACM}, 
  doi = {10.1145/800009.808060}, 
  www_section = {Hardware}, 
}

@article{hardy1988,
  title = {The Confused Deputy (or why capabilities might have been invented)}, 
  author = {Norman Hardy}, 
  journal = {{ACM SIGOPS} Operating Systems Review}, 
  volume = {22}, 
  number = {4}, 
  year = {1988}, 
  month = {October}, 
  www_tags = {selected}, 
  www_section = {Theory}, 
}

@inproceedings{hille:semperos,
  title = {SemperOS: A Distributed Capability System}, 
  author = {Matthias Hille and Nils Asmussen and Pramod Bhatotia and Hermann H{\"a}rtig}, 
  booktitle = {Proceedings of 2019 {USENIX} Annual Technical Conference ({USENIX} {ATC}
        19)}, 
  year = {2019}, 
  month = {July}, 
  address = {Renton, WA}, 
  pages = {709--722}, 
  publisher = {{USENIX} Association}, 
  isbn = {978-1-939133-03-8}, 
  url = {https://www.usenix.org/conference/atc19/presentation/hille}, 
  www_section = {Operating Systems}, 
  abstract = {Capabilities provide an efficient and secure mechanism for fine-grained
        resource management and protection. However, as the modern hardware architectures
        continue to evolve with large numbers of non-coherent and heterogeneous cores, we
        focus on the following research question: can capability systems scale to modern
        hardware architectures? In this work, we present a scalable capability system to
        drive future systems with many non-coherent heterogeneous cores. More
        specifically, we have designed a distributed capability system based on a HW/SW
        co-designed capability system. We analyzed the pitfalls of distributed capability
        operations running concurrently and built the protocols in accordance with the
        insights. We have incorporated these distributed capability management protocols
        in a new microkernel-based OS called SemperOS. Our OS operates the system by
        means of multiple microkernels, which employ distributed capabilities to provide
        an efficient and secure mechanism for fine-grained access to system resources. In
        the evaluation we investigated the scalability of our algorithms and run
        applications (Nginx, LevelDB, SQLite, PostMark, etc.), which are heavily
        dependent on the OS services of SemperOS. The results indicate that there is no
        inherent scalability limitation for capability systems. Our evaluation shows that
        we achieve a parallel efficiency of 70\% to 78\% when examining a system with 576
        cores executing 512 application instances while using 11\% of the system's cores
        for OS services}, 
  www_pdf_url = {https://www.usenix.org/system/files/atc19-hille.pdf}, 
}

@inproceedings{jones74,
  title = {Towards the Design of Secure Systems}, 
  author = {Anita Katherine Jones and William A. Wulf}, 
  booktitle = {Proceedings of the International Workshop on Protection in Operating
        Systems}, 
  organization = {Institut de Recherche d'Informatique}, 
  year = {1974}, 
  month = {August}, 
  address = {Rocquencourt, Le Chesnay, France}, 
  pages = {121--135}, 
  key = {Jones}, 
  www_section = {Theory}, 
}

@article{jones:caparchrevisit,
  title = {Capability Architecture Revisited}, 
  author = {Jones, Anita K.}, 
  journal = {SIGOPS Operating Systems Review}, 
  volume = {14}, 
  number = {3}, 
  year = {1980}, 
  month = {July}, 
  address = {New York, NY, USA}, 
  publisher = {Association for Computing Machinery}, 
  issn = {0163-5980}, 
  doi = {10.1145/850697.850702}, 
  www_section = {Theory, Hardware}, 
}

@article{jones:flexdevmulticomp,
  title = {Flexible Software Development for Multiple Computer Systems}, 
  author = {Anita K. Jones and Karsten Schwan}, 
  journal = {IEEE Transactions on Software Engineering}, 
  year = {1968}, 
  month = {March}, 
  www_section = {Theory}, 
}

@inproceedings{jones:narrowinggap,
  title = {The Narrowing Gap Between Language Systems and Operating Systems}, 
  author = {Anita K. Jones}, 
  booktitle = {Proceedings of the 7th Information Processing {IFIP} Congress}, 
  year = {1977}, 
  month = {August}, 
  location = {Toronto, Canada}, 
  pages = {869--873}, 
  editor = {Bruce Gilchrist}, 
  publisher = {North-Holland}, 
  www_section = {Theory}, 
  day = {8-12}, 
}

@incollection{jones:objectmodel,
  title = {The object model: A conceptual tool for structuring software}, 
  author = {Jones, Anita K.}, 
  booktitle = {Operating Systems: An Advanced Course}, 
  year = {1978}, 
  address = {Berlin, Heidelberg}, 
  pages = {7--16}, 
  editor = {R. Bayer and R. M. Graham and G. Seegm{\"u}ller}, 
  publisher = {Springer Berlin Heidelberg}, 
  doi = {10.1007/3-540-08755-9_2}, 
  isbn = {978-3-540-35880-0}, 
  www_section = {Theory}, 
}

@phdthesis{jones:protection,
  title = {Protection in {Programmed} {Systems}}, 
  author = {Jones, Anita Katherine}, 
  school = {Carnegie Mellon University}, 
  year = {1973}, 
  month = {June}, 
  type = {{PhD}}, 
  www_tags = {selected}, 
  language = {en}, 
  abstract = {This dissertation investigates the control of access to objects within
        programmed systems. The vehicle for this study is a model of protection that
        isolates a small set of mechanisms needed to provide access centre!, leaving the
        policy for invoking these mechanisms to vary naturally with applications.
        Emphasis is placed on access control required for parameters that accompany a
        process crossing between execution environments; and a new concept called
        amplification is defined. The model is shown to provide structure and terminology
        sufficient for describing and comparing diverse protection systems, for
        expressing and proving boundary conditions that characterize the manipulation of
        objects within environments independent of the code executed, and for partially
        ordering protection systems according to the services they provide. In addition,
        the dissertation introduces the concept of a centralized protection facility
        capable of providing access control for user defined objects and accesses}, 
  www_section = {Theory}, 
}

@inproceedings{jones:specifyresourceconcurrent,
  title = {The Specification of Resource Allocation for a Concurrent Program}, 
  author = {Anita K. Jones and Karsten Schwan}, 
  journal = {IEEE Software}, 
  booktitle = {}, 
  year = {1986}, 
  month = {May}, 
  www_section = {Theory}, 
}

@inproceedings{jones:staros,
  title = {{StarOS}, a Multiprocessor Operating System for the Support of Task Forces}, 
  author = {Jones, Anita K. and Chansler, Robert J. and Durham, Ivor and Schwans, Karsten
        and Vegdahl, Steven R.}, 
  booktitle = {Proceedings of the Seventh ACM Symposium on Operating Systems Principles}, 
  year = {1979}, 
  address = {New York, NY, USA}, 
  location = {Pacific Grove, California, USA}, 
  publisher = {Association for Computing Machinery}, 
  series = {SOSP '79}, 
  doi = {10.1145/800215.806579}, 
  isbn = {0897910095}, 
  abstract = {StarOS is a message-based, object-oriented, multiprocessor operating system,
        specifically designed to support task forces, large collections of concurrently
        executing processes that cooperate to accomplish a single purpose. StarOS has
        been implemented at Carnegie-Mellon University for the 50 processor Cm*
        multi-microprocessor computer}, 
  www_section = {Operating Systems}, 
}

@article{jones:towardsdesignsecure,
  title = {Towards the design of secure systems}, 
  author = {Jones, Anita K. and Wulf, William A.}, 
  journal = {Software: Practice and Experience}, 
  volume = {5}, 
  number = {4}, 
  year = {1975}, 
  doi = {https://doi.org/10.1002/spe.4380050403}, 
  keywords = {Protection, Security policy, HYDRA, Capability, Operating system design}, 
  abstract = {Abstract Within a programmed system, we may distinguish between different
        kinds of information in order to control the use of each kind by separate
        security policies, where each policy is tailored to the sensitivity and desired
        dissemination of that one kind of information. This paper analyses the
        implications of implementing security policies and describes mechanisms which can
        be used as the basis for constructing operating systems with the desired security
        attributes}, 
  www_section = {Theory}, 
}

@phdthesis{karger:improvingcap,
  title = {Improving {Security} and {Performance} for {Capability} {Systems}}, 
  author = {Paul Ashley Karger}, 
  institution = {University of Cambridge, Computer Laboratory}, 
  number = {149}, 
  year = {1988}, 
  month = {October}, 
  type = {Technical {Report}}, 
  abstract = {This dissertation examines two major limitations of capability systems: an
        inability to support security policies that enforce confinement and a reputation
        for relatively poor performance when compared with non-capability systems. The
        dissertation examines why conventional capability systems cannot enforce
        confinement and proposes a new secure capability architecture, called SCAP, in
        which confinement can be enforced. SCAP is based on the earlier Cambridge
        Capability System, CAP. The dissertation shows how a non-discretionary security
        policy can be implemented on the new architecture, and how the new architecture
        can also be used to improve traceability of access and revocation of access. The
        dissertation also examines how capability systems are vulnerable to discretionary
        Trojan horse attacks and proposes a defence based on rules built into the
        command-language interpreter. System-wide garbage collection, commonly used in
        most capability systems, is examined in the light of the non-discretionary
        security policies and found to be fundamentally insecure. The dissertation
        proposes alternative approaches to storage management to provide at least some of
        the benefits of system-wide garbage collection, but without the accompanying
        security problems. Performance of capability systems is improved by two ma jor
        techniques. First, the doctrine of programming generality is addressed as one ma
        jor cause of poor performance. Protection domains should be allocated only for
        genuine security reasons, rather than at every subroutine boundary. Compilers can
        better enforce modularity and good programming style without adding the expense
        of security enforcement to every subroutine call. Second, the ideas of reduced
        instruction set computers (RISC) can be applied to capability systems to simplify
        the operations required. The dissertation identifies a minimum set of hardware
        functions needed to obtain good performance for a capability system. This set is
        much smaller than previous research had indicated necessary. A prototype
        implementation of some of the capability features is described. The prototype was
        implemented on a re-microprogrammed VAX-11/730 computer. The dissertation
        examines the performance and software compatibility implications of the new
        capability architecture, both in the context of conventional computers, such as
        the VAX, and in the context of RISC processors}, 
  www_pdf_url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-149.pdf}, 
  www_section = {Theory, Hardware / CAP, Operating Systems}, 
}

@inproceedings{lampson69,
  title = {Dynamic Protection Structures}, 
  author = {B.W. Lampson}, 
  booktitle = {Proceedings of the November 18-20, 1969, fall joint computer conference;
        AFIPS '69 (Fall)}, 
  year = {1969}, 
  month = {November}, 
  doi = {10.1145/1478559.1478563}, 
  www_pdf_url = {http://bwlampson.site/06-DynamicProtect/06-DynamicProtect.pdf}, 
  www_section = {Theory}, 
}

@inproceedings{lampson71,
  title = {Protection}, 
  author = {B.W. Lampson}, 
  booktitle = {Proceedings of the Fifth Princeton Symposium on Info. Sci. and Systems}, 
  year = {1971}, 
  month = {March}, 
  note = {Reprinted in ACM Operating Systems Review, Vol. 8 (1), January 1974}, 
  www_section = {Theory}, 
}

@article{lampson73,
  title = {A Note on the Confinement Problem}, 
  author = {B.W. Lampson}, 
  journal = {Communications of the ACM}, 
  volume = {16}, 
  number = {10}, 
  year = {1973}, 
  month = {October}, 
  pages = {613--615}, 
  key = {Lampson}, 
  www_section = {Theory}, 
}

@book{levy:capsystems,
  title = {Capability-{Based} {Computer} {Systems}}, 
  author = {{Henry M. Levy}}, 
  year = {1984}, 
  publisher = {Digital Press}, 
  www_important = {1}, 
  www_section = {Surveys}, 
  www_website_url = {https://homes.cs.washington.edu/~levy/capabook/}, 
  www_tags = {selected}, 
  www_remarks = {Levy reviews systems up through the mid-1980s, including the Cambridge
        CAP, HYDRA, StarOS, IBM's System/38, and Intel's iAPX 432. The book is out of
        print but the website hosts PDF copies of each chapter.}, 
}

@article{mayer:b5000later,
  title = {The Architecture of the Burroughs {B5000}: 20 Years Later and Still Ahead of the
        Times?}, 
  author = {Mayer, Alastair J. W.}, 
  journal = {SIGARCH Comput. Archit. News}, 
  volume = {10}, 
  number = {4}, 
  year = {1982}, 
  month = {June}, 
  address = {New York, NY, USA}, 
  pages = {3--10}, 
  publisher = {ACM}, 
  issn = {0163-5964}, 
  www_section = {Hardware}, 
  doi = {10.1145/641542.641543}, 
}

@inproceedings{mettler:joee,
  title = {{Class properties for security review in an object-capability subset of Java}}, 
  author = {Mettler, Adrian and Wagner, David}, 
  booktitle = {Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and
        Analysis for Security '10}, 
  year = {2010}, 
  address = {New York, NY, USA}, 
  location = {Toronto, Canada}, 
  pages = {1--7}, 
  publisher = {ACM}, 
  doi = {10.1145/1814217.1814224}, 
  isbn = {978-1-60558-827-8}, 
  www_section = {Programming Languages}, 
}

@techreport{miller:capmyths,
  title = {Capability {Myths} {Demolished}}, 
  author = {Miller, Mark S and Yee, Ka-Ping and Shapiro, Jonathan}, 
  institution = {Johns Hopkins University}, 
  year = {2003}, 
  www_tags = {selected}, 
  language = {en}, 
  abstract = {We address three common misconceptions about capability-based systems: the
        Equivalence Myth (access control list systems and capability systems are formally
        equivalent), the Confinement Myth (capability systems cannot enforce
        confinement), and the Irrevocability Myth (capability-based access cannot be
        revoked). The Equivalence Myth obscures the benefits of capabilities as compared
        to access control lists, while the Confinement Myth and the Irrevocability Myth
        lead people to see problems with capabilities that do not actually exist}, 
  www_section = {Theory}, 
  www_pdf_url = {http://srl.cs.jhu.edu/pubs/SRL2003-02.pdf}, 
}

@inproceedings{miller:paradigmregained,
  title = {Paradigm {Regained}: {Abstraction} {Mechanisms} for {Access} {Control}}, 
  author = {Miller, Mark S. and Shapiro, Jonathan S.}, 
  booktitle = {Proceedings of Advances in {Computing} {Science} -- {ASIAN} 2003}, 
  year = {2003}, 
  address = {Berlin, Heidelberg}, 
  pages = {224--242}, 
  editor = {Vijay A. Saraswat}, 
  publisher = {Springer Berlin Heidelberg}, 
  isbn = {978-3-540-40965-6}, 
  abstract = {Access control systems must be evaluated in part on how well they enable one
        to distribute the access rights needed for cooperation, while simultaneously
        limiting the propagation of rights which would create vulnerabilities. Analysis
        to date implicitly assumes access is controlled only by manipulating a system's
        protection state -- the arrangement of the access graph. Because of the
        limitations of this analysis, capability systems have been "proven" unable to
        enforce some basic policies: revocation, confinement, and the *-properties
        (explained in the text)}, 
  www_section = {Theory}, 
  www_website_url = {http://www.erights.org/talks/asian03/}, 
  www_tags = {selected}, 
  www_pdf_url = {http://www.erights.org/talks/asian03/paradigm-revised.pdf}, 
}

@inproceedings{neumann:caprevisit,
  title = {Capabilities Revisited: A Holistic Approach to Bottom-to-Top Assurance of
        Trustworthy Systems}, 
  author = {Peter G. Neumann and Robert N. M. Watson}, 
  booktitle = {Proceedings of the Fourth Layered Assurance Workshop}, 
  organization = {U.S. Air Force Cryptographic Modernization Office and AFRL}, 
  year = {2010}, 
  month = {December}, 
  address = {Austin, Texas}, 
  www_pdf_url = {http://www.csl.sri.com/neumann/law10.pdf}, 
  www_section = {Hardware / CHERI, Theory}, 
}

@techreport{neumann:psos75,
  title = {A Provably Secure Operating System}, 
  author = {P.G. Neumann and L. Robinson and K.N. Levitt and R.S. Boyer and A.R. Saxena}, 
  institution = {Computer Science Laboratory SRI International, Menlo Park, California}, 
  year = {1975}, 
  month = {June}, 
  www_section = {Operating Systems / PSOS}, 
}

@techreport{neumann:psos77,
  title = {A Provably Secure Operating System: The System, Its Applications, and Proofs}, 
  author = {P.G. Neumann and R.S. Boyer and R.J. Feiertag and K.N. Levitt and L. Robinson}, 
  institution = {Computer Science Laboratory SRI International, Menlo Park, California}, 
  year = {1977}, 
  month = {February}, 
  www_section = {Operating Systems / PSOS}, 
}

@inproceedings{neumann:psos79,
  title = {The Foundations of a {Provably Secure Operating System} ({PSOS})}, 
  author = {R. J. Feiertag and P. G. Neumann}, 
  booktitle = {Proceedings of the National Computer Conference}, 
  year = {1979}, 
  pages = {329--334}, 
  key = {Feiertag}, 
  publisher = {AFIPS Press}, 
  www_tags = {selected}, 
  www_section = {Operating Systems / PSOS}, 
  www_pdf_url = {http://www.csl.sri.com/neumann/psos.pdf}, 
}

@techreport{neumann:psos80,
  title = {{A Provably Secure Operating System}: The System, Its Applications, and Proofs}, 
  author = {P. G. Neumann and R.S. Boyer and R.J. Feiertag and K.N. Levitt and L.
        Robinson}, 
  institution = {Computer Science Laboratory, SRI International, Menlo Park, California}, 
  year = {1980}, 
  month = {May}, 
  note = {2nd edition, Report CSL-116}, 
  www_section = {Operating Systems / PSOS}, 
}

@inproceedings{rajunas:keykos,
  title = {Security in {K}ey{KOS}}, 
  author = {S.A. Rajunas and N. Hardy and A.C. Bomberger and W.S. Frantz and C.R. Landau}, 
  booktitle = {Proceedings of the 1986 IEEE Sympsium on Security and Privacy}, 
  year = {1986}, 
  month = {April}, 
  www_section = {Operating Systems}, 
}

@phdthesis{redell:naming,
  title = {Naming and {Protection} in {Extendible} {Operating} {Systems}}, 
  author = {Redell, David D}, 
  school = {Massachusetts Institute of Technology}, 
  year = {1974}, 
  www_tags = {selected}, 
  language = {en}, 
  abstract = {The properties of capability-based extendible operating systems are
        described, and various aspects of such systems are discussed, with emphasis on
        the conflict between free distribution of access privileges and later revocation
        of those privileges. The discussion culminates in a set of goals for a new
        capability scheme. A new {\textless}Jc.sign is then proposed, which provides both
        type extension and revocation through the definition of generalized sealing of
        capabilities. The implementation of this design is discussed in sufficient detail
        to demonstrate that it would be workable and acceptably economical. The utility
        of the proposed capability mechanism is demonstrated by describing two facilities
        implementable in terms of it. These are: (a) revocable parameters for calls
        between mutually suspicious subsystems, and (b) directories providing a civilized
        medium for the storage and distribution of revocable capabilities}, 
  www_section = {Theory}, 
}

@article{saltzer:protection,
  title = {The protection of information in computer systems}, 
  author = {Saltzer, J.H. and Schroeder, M.D.}, 
  journal = {Proceedings of the IEEE}, 
  volume = {63}, 
  number = {9}, 
  year = {1975}, 
  pages = {1278--1308}, 
  doi = {10.1109/PROC.1975.9939}, 
  language = {en}, 
  abstract = {This tutorial paper explores the mechanics of protecting computer-stored
        information from unauthorized use or modification. It concentrates on those
        architectural structures--whether hardware or software--that are necessary to
        support information protection. The paper develops in three main sections.
        Section I describes desired functions, design principles, and examples of
        elementary protection and authentication mechanisms. Any reader familiar with
        computers should find the first section to be reasonably accessible. Section II
        requires some familiarity with descriptor-based computer architecture. It
        examines in depth the principles of modern protection architectures and the
        relation between capability systems and access control list systems, and ends
        with a brief analysis of protected subsystems and protected objects. The reader
        who is dismayed by either the prerequisites or the level of detail in the second
        section may wish to skip to Section III, which reviews the state of the art and
        current research projects and provides suggestions for further reading}, 
  issn = {0018-9219}, 
  www_section = {Theory}, 
}

@techreport{shapiro:coyotosspec,
  title = {Coyotos Microkernel Specification}, 
  author = {Jonathan S. Shapiro and Jonathan W. Adams}, 
  institution = {Johns Hopkins University}, 
  year = {2007}, 
  month = {September}, 
  subtitle = {Version 0.6+}, 
  www_html_url = {https://web.archive.org/web/20160904092954/http://www.coyotos.org:80/docs/ukernel/spec.html},
  www_section = {Operating Systems}, 
}

@article{shapiro:eros02,
  title = {{EROS:} A Principle-Driven Operating System from the Ground Up}, 
  author = {J.S. Shapiro and N. Hardy}, 
  journal = {IEEE Software}, 
  volume = {19}, 
  number = {1}, 
  year = {2002}, 
  month = {January}, 
  pages = {26--33}, 
  www_section = {Operating Systems / EROS}, 
}

@inproceedings{shapiro:eros99,
  title = {{EROS}: {A} {Fast} {Capability} {System}}, 
  author = {Shapiro, Jonathan S. and Smith, Jonathan M. and Farber, David J.}, 
  booktitle = {Proceedings of the {Seventeenth} {ACM} {Symposium} on {Operating} {Systems}
        {Principles}}, 
  year = {1999}, 
  address = {New York, NY, USA}, 
  pages = {170--185}, 
  publisher = {ACM}, 
  series = {{SOSP} '99}, 
  doi = {10.1145/319151.319163}, 
  isbn = {978-1-58113-140-6}, 
  shorttitle = {{EROS}}, 
  abstract = {EROS is a capability-based operating system for commodity processors which
        uses a single level storage model. The single level store's persistence is
        transparent to applications. The performance consequences of support for
        transparent persistence and capability-based architectures are generally believed
        to be negative. Surprisingly, the basic operations of EROS (such as IPC) are
        generally comparable in cost to similar operations in conventional systems. This
        is demonstrated with a set of microbenchmark measurements of semantically similar
        operations in Linux.The EROS system achieves its performance by coupling
        well-chosen abstract objects with caching techniques for those objects. The
        objects (processes, nodes, and pages) are well-supported by conventional
        hardware, reducing the overhead of capabilities. Software-managed caching
        techniques for these objects reduce the cost of persistence. The resulting
        performance suggests that composing protected subsystems may be less costly than
        commonly believed}, 
  www_section = {Operating Systems / EROS}, 
}

@inproceedings{shapiro:towardsverified,
  title = {Towards a verified, general-purpose operating system kernel}, 
  author = {Jonathan Shapiro and Michael Scott Doerrie and Eric Northup and Mark Miller}, 
  booktitle = {Proceedings of the NICTA Invitational Workshop on Operating System
        Verification}, 
  year = {2004}, 
  pages = {1--19}, 
  www_section = {Operating Systems}, 
  www_pdf_url = {http://www.cs.jhu.edu/~swaroop/osverify-2004.pdf}, 
}

@article{skorstengaard:stktokens,
  title = {{StkTokens}: Enforcing Well-bracketed Control Flow and Stack Encapsulation using
        Linear Capabilities}, 
  author = {Skorstengaard, Lau and Devriese, Dominique and Birkedal, Lars}, 
  journal = {Proc. ACM Programming Languages}, 
  volume = {3}, 
  number = {POPL}, 
  year = {2019}, 
  month = {January}, 
  address = {New York, NY, USA}, 
  publisher = {ACM}, 
  www_section = {Theory}, 
}

@techreport{ucam-cl-tr-891,
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set
        Architecture (Version 5)}}, 
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe,
        Michael and Anderson, Jonathan and Chisnall, David and Davis, Brooks and Joannou,
        Alexandre and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and Norton,
        Robert and Son, Stacey and Xia, Hongyan}, 
  institution = {University of Cambridge, Computer Laboratory}, 
  number = {UCAM-CL-TR-891}, 
  year = {2016}, 
  month = {June}, 
  www_section = {Hardware / CHERI}, 
  www_pdf_url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-891.pdf}, 
}

@incollection{watson2017:cheri-deployability,
  title = {{Balancing Disruption and Deployability in the CHERI Instruction-Set
        Architecture (ISA)}}, 
  author = {Robert N. M. Watson and Peter G Neumann and Simon W. Moore}, 
  booktitle = {New Solutions for Cybersecurity}, 
  year = {2018}, 
  chapter = {5}, 
  editor = {H. Shrobe and D. L. Shrier and A. Pentland}, 
  publisher = {MIT Press/Connection Science}, 
  www_pdf_url = {https://www.cl.cam.ac.uk/research/security/ctsrd/pdfs/2017mit-cybersecurity-cheri-web.pdf},
  www_section = {Hardware / CHERI}, 
}

@inproceedings{watson:capsicum,
  title = {Capsicum: {P}ractical capabilities for {U}nix}, 
  author = {Robert N.~M. Watson and J. Anderson and B. Laurie and K. Kennaway}, 
  booktitle = {Proceedings of the 19th USENIX Security Symposium}, 
  year = {2010}, 
  month = {August}, 
  publisher = {USENIX}, 
  www_section = {Operating Systems}, 
}

@techreport{watson:cheriisav6,
  title = {Capability {Hardware} {Enhanced} {RISC} {Instructions}: {CHERI}
        {Instruction}-{Set} {Architecture} ({Version} 6)}, 
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe,
        Michael and Anderson, Jonathan and Baldwin, John and Chisnall, David and Davis,
        Brooks and Joannou, Alexandre and Laurie, Ben and Moore, Simon W. and Murdoch,
        Steven J. and Norton, Robert and Son, Stacey and Xia, Hongyan}, 
  institution = {University of Cambridge, Computer Laboratory}, 
  number = {UCAM-CL-TR-907}, 
  year = {2017}, 
  month = {April}, 
  www_section = {Hardware / CHERI}, 
  www_pdf_url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-907.pdf}, 
}

@techreport{watson:cheriisav7,
  title = {{Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set
        Architecture (Version 7)}}, 
  author = {Watson, Robert N. M. and Neumann, Peter G. and Woodruff, Jonathan and Roe,
        Michael and Almatary, Hesham and Anderson, Jonathan and Baldwin, John and
        Chisnall, David and Davis, Brooks and Filardo, Nathaniel Wesley and Joannou,
        Alexandre and Laurie, Ben and Moore, Simon W. and Murdoch, Steven J. and
        Nienhuis, Kyndylan and Norton, Robert and Richardson, Alex and Rugg, Peter and
        Sewell, Peter and Son, Stacey and Xia, Hongyan}, 
  institution = {University of Cambridge, Computer Laboratory}, 
  number = {UCAM-CL-TR-927}, 
  year = {2018}, 
  month = {October}, 
  www_tags = {selected}, 
  url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-927.pdf}, 
  www_section = {Hardware / CHERI}, 
  www_pdf_url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-907.pdf}, 
}

@article{woodruff2019:chericoncentrate,
  title = {{CHERI} Concentrate: Practical Compressed Capabilities}, 
  author = {Woodruff, Jonathan and Joannou, Alexandre and Xia, Hongyan and Fox, Anthony and
        Norton, Robert and Bauereiss, Thomas and Chisnall, David and Davis, Brooks and
        Gudka, Khilan and Filardo, Nathaniel W. and Markettos, A. Theodore and Roe,
        Michael and Neumann, Peter G. and Watson, Robert N. M. and Moore, Simon W.}, 
  journal = {IEEE Transactions on Computers}, 
  year = {2019}, 
  publisher = {IEEE}, 
  doi = {10.1109/TC.2019.2914037}, 
  www_section = {Theory, Hardware / CHERI}, 
}

@article{wulf:hydra,
  title = {{HYDRA: the kernel of a multiprocessor operating system}}, 
  author = {Wulf, W. and Cohen, E. and Corwin, W. and Anita Jones and Levin, R. and
        Pierson, C. and Pollack, F.}, 
  journal = {Communications of the ACM}, 
  volume = {17}, 
  number = {6}, 
  year = {1974}, 
  address = {New York, NY, USA}, 
  pages = {337--345}, 
  publisher = {ACM}, 
  issn = {0001-0782}, 
  www_section = {Operating Systems / HYDRA}, 
  doi = {10.1145/355616.364017}, 
}

@book{wulf:hydrabook,
  title = {{HYDRA/C.mmp} An Experimental Computer System}, 
  author = {William A. Wulf and Roy Levin and Samuel P. Harbinson}, 
  year = {1981}, 
  publisher = {McGraw-Hill}, 
  isbn = {978-0070721203}, 
  www_section = {Operating Systems / HYDRA}, 
  www_tags = {selected}, 
}