Skip to content

ukstv/awesome-ocap

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

11 Commits
 
 

Repository files navigation

Awesome Object Capabilities and Capability-based Security

Capability-based security enables the concise composition of powerful patterns of cooperation without vulnerability.

Application Hosting

Libraries and Frameworks

  • Caja is a compiler for making third-party HTML, CSS and JavaScript safe for embedding. Caja safely supports mashups and extends JSON with code.

  • Cap’n Proto is an open source serialization and RPC protocol with distributed and persistent capabilities and promise pipelining.

  • Secure EcmaScript (SES) is a fail-stop subset of ES5. SES should compatibly run all ES5 code that follows recognized ES5 best practices. The SES restrictions support the writing of defensively consistent abstractions -- object abstractions that can defend their integrity while being exposed to untrusted but confined objects.

  • Capper is web application server with built-in object capability security built on Node.js/Express

  • Network protocols, sans I/O supports object capability discipline by letting the caller handle network access.

  • Shill: Shill is a shell scripting language designed to make it easy to follow the Principle of Least Privilege. It runs on FreeBSD and is developed in Racket.

  • 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.

Operating Systems

  • 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 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.

    • Genode OS Framework release 16.08 Aug 31, 2016

      Genode 16.08 makes the entirety of the framework's drivers, protocol stacks, and libraries available on the seL4 kernel, brings VirtualBox 4 to the Muen separation kernel, and hosts VirtualBox 5 on top of the NOVA kernel. Further highlights are virtual networking and TOR, profound Zynq board support, and tools for statistical profiling.

  • 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.

  • 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

  • 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.

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.

Presentations, Talks, Slides, and Videos

Scholarly 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)

  • 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.

  • 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

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published