Skip to content
/ awesome-ocap Public
forked from dckc/awesome-ocap

Awesome Object Capabilities and Capability Security

License

Unlicense license
0 stars 25 forks Branches Tags Activity
Star
Notifications You must be signed in to change notification settings

kephas/awesome-ocap

BranchesTags
 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

52 Commits
CONTRIBUTING.md
CONTRIBUTING.md
 
 
LICENSE
LICENSE
 
 
README.md
README.md
 
 

Repository files navigation

Awesome Object Capabilities and Capability-based Security

Awesome

Capability-based security enables the concise composition of powerful patterns of cooperation without vulnerability. What Are Capabilities? explains in detail.

Contents

Applications and Services

Libraries and Frameworks

Programming Languages

  • Pony is an open-source, object-oriented, actor-model, capabilities-secure, high performance programming language.

  • Monte is a nascent dynamic programming language reminiscent of Python and E. It is based upon The Principle of Least Authority (POLA), which governs interactions between objects, and a capability-based object model, which grants certain essential safety guarantees to all objects.

    • bootstrapped from rpython (pypy toolchain) and libuv and libsodium using (primarily) the nix build system.
    • Docker images: montelang

Operating Systems

  • CloudABI is a runtime environment for Unix-like systems that introduces dependency injection to full Unix applications. Instead of allowing applications to open arbitrary files on disk and connect to arbitrary systems on the network, you as a user exactly inject those resources that the application should access.

  • Capsicum Capsicum is a lightweight OS capability and sandbox framework that extends the POSIX API, providing several new OS primitives to support object-capability security on UNIX-like operating systems

    • Capsicum Go support Ben Laurie 19 Jul 2017
    • Capsicum for FreeBSD
    • Capsicum for Linux
    • Watson, R. N. M. 2013 Capsicum year in review. Light Blue Touchpaper, 20 December, 2013. Robert Watson reviews Capsicum events from 2013: work funded by the FreeBSD Foundation and Google on FreeBSD 10.0, Casper in FreeBSD 11, David Drysdale's port of Capsicum to Linux at Google, Summer of Code students, joint work with the University of Wisconsin on Capsicum, and future funded Capsicum work.

  • genode is a novel OS architecture that is able to master the complexity of code and policy -- the most fundamental security problem shared by modern general-purpose operating systems -- by applying a strict organizational structure to all software components including device drivers, system services, and applications.

    • Road Map for 2018 Jan 17, 2018

      2018 will be the year of Sculpt.

    • Genode OS Framework release 17.11 Nov 30, 2017

      Most of the many improvements of version 17.11 are geared towards the practical use of Genode as day-to-day OS. They include a reworked GUI stack, new user-input features, and the packaging of many components. The new version also revises the boot concept on x86, updates the seL4 kernel, and enhances Genode's user-level networking facilities.

    • Genode OS Framework release 17.08 Aug 30, 2017

      Version 17.08 enables hardware-accelerated graphics on Intel-Gen8 GPUs and expands Genode's seL4-kernel support to the ARM and 64-bit x86 architectures. Further topics are UEFI boot, VFS enhancements such as a new FatFS plugin, and the use of Genode as Xen DomU.

    • Genode OS Framework release 16.08 Aug 31, 2016

  • Fuchsia is a real-time operating system in development by Google since Aug 2016. It's based on a microkernel, Magenta, with a capability security model.

  • seL4 is the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement; it is available as open source.

    • Getting started with seL4, CAmkES, and L4v: Dependencies MAY 19, 2017
    • seL4 on the Raspberry Pi 3 FEBRUARY 8, 2017
    • Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
      Comprehensive formal verification of an OS microkernel
    • Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick and Gerwin Klein
      seL4 enforces integrity
      International Conference on Interactive Theorem Proving, pp. 325-340, Nijmegen, The Netherlands, August, 2011

      Abstract. We prove the enforcement of two high-level access control properties in the seL4 microkernel: integrity and authority confinement. Integrity provides an upper bound on write operations. Authority con- finement provides an upper bound on how authority may change. Apart from being a desirable security property in its own right, integrity can be used as a general framing property for the verification of user-level system composition. The proof is machine checked in Isabelle/HOL and the results hold via refinement for the C implementation of the kernel.

    • Robigalia is an OS "continuing the heritage of EROS and Coyotos" using seL4 and written in Rust

  • cosix is a capability-based operating system that consists of a small kernel that provides memory management and inter-process communication, and a userland that provides an IP stack and filesystems. The capability enforcing mechanism comes from implementing only CloudABI as an Application Binary Interface between the userland and the kernel.

  • Barrelfish is a research operating system motivated by two closely related trends in hardware design: the rapidly growing number of cores and the increasing diversity in computer hardware. Barrelfish uses a single model of capabilities to control access to all physical memory, kernel objects, communication end-points, and other miscellaneous access rights.

CPUs

  • CHERI is an open source capability CPU design.

    • June 2016: CHERI ISAv5 specification: improves the maturity of 128-bit capabilities, code efficiency, and description of the protection model.
    • June 2016: CHERI-JNI: Sinking the Java security model into the C, explores how CHERI capabilities can be used to support sandboxing with safe and efficient memory sharing between Java Native Interface (JNI) code and the Java Virtual Machine. ASPLOS 2017
    • May 2016: slides from the first CHERI microkernel workshop, Cambridge, UK in April 2016.

Presentations, Talks, Slides, and Videos

Articles

Peer-reviewed Articles

See also Usable Security and Capabilities bibliography.

  • D. Devriese, Birkedal, and Piessens
    Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
    1st IEEE European Symposium on Security and Privacy, Congress Center Saar, Saarbrücken, GERMANY, 2016.

  • Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
    Comprehensive formal verification of an OS microkernel
    ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014

  • S. Clebsch and S. Drossopoulou
    Fully concurrent garbage collection of actors on many-core machines
    OOPSLA 2013

  • Mark S. Miller, Tom Van Cutsem, Bill Tulloh
    Distributed Electronic Rights in JavaScript
    ESOP'13 22nd European Symposium on Programming, Springer (2013)

  • Barth, Adam, Joel Weinberger, and Dawn Song.
    Cross-Origin JavaScript Capability Leaks: Detection, Exploitation, and Defense. USENIX security symposium. 2009.

  • Close, T.: Web-key: Mashing with permission. In: W2SP’08. (2008)

  • Miller MS
    Robust composition: towards a unified approach to access control and concurrency control
    Ph.D. Thesis, Johns Hopkins University; 2006.

    When separately written programs are composed so that they may cooperate, they may instead destructively interfere in unanticipated ways. These hazards limit the scale and functionality of the software systems we can successfully compose. This dissertation presents a framework for enabling those interactions between components needed for the cooperation we intend, while minimizing the hazards of destructive interference.

    Great progress on the composition problem has been made within the object paradigm, chiefly in the context of sequential, single-machine programming among benign components. We show how to extend this success to support robust composition of concurrent and potentially malicious components distributed over potentially malicious machines. We present E, a distributed, persistent, secure programming language, and CapDesk, a virus-safe desktop built in E, as embodiments of the techniques we explain.

  • Miller, Mark S., E. Dean Tribble, and Jonathan Shapiro. Concurrency among strangers. TGC. Vol. 5. 2005.

  • Mark S. Miller, Chip Morningstar, Bill Frantz
    Capability-based Financial Instruments
    Proc. Financial Cryptography 2000, Springer-Verlag, Anguila, BWI, pp. 349-378.

    Every novel cooperative arrangement of mutually suspicious parties interacting electronically — every smart contract — effectively requires a new cryptographic protocol. However, if every new contract requires new cryptographic protocol design, our dreams of cryptographically enabled electronic commerce would be unreachable. Cryptographic protocol design is too hard and expensive, given our unlimited need for new contracts. Just as the digital logic gate abstraction allows digital circuit designers to create large analog circuits without doing analog circuit design, we present cryptographic capabilities as an abstraction allowing a similar economy of engineering effort in creating smart contracts. We explain the E system, which embodies these principles, and show a covered-call-option as a smart contract written in a simple security formalism independent of cryptography, but automatically implemented as a cryptographic protocol coordinating five mutually suspicious parties

About

Awesome Object Capabilities and Capability Security

Resources

Readme

License

Unlicense license
Activity

Stars

0 stars

Watchers

3 watching

Forks

0 forks
Report repository

Releases

No releases published

Packages

No packages published