Declarative, Temporal, and Practical Programming with Capabilities

References:

Motivation

Network utilities process data read directly from a network connection, but execute vulnerable code (tcpdump1, wget2, etc.).

Traditional OS environment, “if a programmer wants to verify that his program is secure, he typically must first verify that the program satisfies very strong properties, such as memory safety.”

“However, recent work 3 4 5 6 has produced new operating systems that allow programmers to develop programs that execute untrusted code yet satisfy strong security requirements.”

“Moreover, programmers can develop such programs with much less effort than fully verifying the program for a traditional operating system.”

“The developers of such systems have manually modified applications to invoke security primitives so that the application satisfies strong security policies, even when the application contains untrusted code.”

Example: Capsicum 5 on FreeBSD 7.

  • “A capability is a file descriptor and an access right for the descriptor”.
  • Defines “whether a process has the privilege to grant to itself further capabilities (i.e. open more files)”. (LLM: secure???)
  • Provides each process a list of system calls that the process can invoke.
  • “Trusted code in a program can first communicate with its environment unrestricted by Capsicum, and then invoke primitives to limit itself to have only the capabilities that it needs for the remainder of its execution.”
  • “Untrusted code executes only the limitd capabilities defined by the trusted code.”
  • In practice, “it is difficult for programmers to reason about the subtle, temporal effects of the primitives”:
    • tcpdump: difficulty results from the conflicting demands of (i) using low-level primitives, (ii) ensuring that the program satisfies a strong, high-level security requirement, and (iii) preserving the core functionality of the original program.

Overview

describes capweave, a tool that

  • takes as input

    1. An LLVM Program. A program that does not invoke Capsicum primitives
    2. A declarative, temporal policy, stated in terms of the capabilities that the program should hold over the course of its execution. (of the possibly-changing capabilities that a program must hold during its execution).

  • automatically rewrites the program to use Capsicum system calls to enforce the policy. (Compartmentalizes the program and instruments it to invoke Capsicum primitives so that it satisfies the policy when executed on Capsicum).

Challenges

Two key challenges that a programmer faces when manually rewriting a program for Capsicum.

  1. To define what “secure behavior” means for his program.
  2. To write his program to be both secure and functional.

wget Separation

wget code

  • For each input URL, wget determines under what protocol the URL is addressed (line L1).
  • Then wget runs protocol-specific functions to
    • (i) open a socket to the server holding the URL (line L2),
    • (ii) download the data addressed by the URL over the socket (lines L3 and L4), and
    • (iii) write the data to a file in the file system (line L5).

Security Vulnerability in wget 2:

  • Versions through v.1.12 include a vulnerability that allows an attacker who controls a server with with which wget interacts to write data to any file on the host file system that can be written by the user who runs wget.
  • It is exposed when wget processes a particular HTTP response from the server.
    • receive a redirect response from a server (which directs wgets to download data from a different network address);
    • wget determines the path in its host file system to which it will write data directly from the information provided by the redict server.
  • A malicious server can exploit this behavior to craft a redirect response that causes wget to write data chosen by the attacker to a path in the file system chosen by the attacker2.

To defense:

  • Traditional way:
    • “formally specify that wget must not demonstrate a vul. along the lines of the one described above”
    • “rewrite wget so that it satisfies such a specification.”
    • “requires detailed knowledge of both the structure of wget and of the HTTP protocol”.
  • This paper seek for ways:
    • “a developer could define an acceptable, if perhaps weaker, specification for wget in terms of commonly-used, well-understood operating-system objects, such as file descriptors’:
    • e.g. “When wget executes read_http, it should always be able to open arbitrary files and sockets. But wget should execute write_data with the ability to open files if and only if it has not received an HTTP-redirect response”.

Evaluation

More

  1. “CVE-2007-3798,” http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2007-3798, July 2007. ↩
  2. “CVE-2004-1488,” http://cve.mitre.org/cgi-bin/cvename.cgi?name=CAN-2004-1488, Feb 2005. ↩
  3. P. Efstathopoulos, M. Krohn, S. VanDeBogart, C. Frey, D. Ziegler, E. Kohler, D. Mazières, F. Kaashoek, and R. Morris, “Labels and event processes in the Asbestos operating system,” in SOSP, 2005. ↩
  4. M. Krohn, A. Yip, M. Brodsky, N. Cliffer, M. F. Kaashoek, E. Kohler, and R. Morris, “Information flow control for standard OS abstractions,” in SOSP, 2007. ↩
  5. R. N. M. Watson, J. Anderson, B. Laurie, and K. Kennaway,“Capsicum: Practical capabilities for UNIX,” in USENIX Security, 2010. ↩
  6. N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Mazières, “Making information flow explicit in HiStar,” in OSDI, 2006. ↩
  7. “FreeBSD 9.0-RELEASE announcement,” http://www.freebsd.org/releases/9.0R/announce.html, Jan. 2012. ↩
Created Jul 13, 2021 // Last Updated Jul 13, 2021

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?