Secure Programming Via Game-Based Synthesis

Abstract

Interactive security systems provide powerful security primitives (i.e., security-oriented system calls) that an application can invoke at various moments during execution to control accesses to its sensitive information. Prior to the work described in this thesis, an application developer was forced to explicitly write imperative code that executes security primitives. Moreover, a developer could only reason informally about whether the code satisfied the developers intuitive notions of security and correctness.

This dissertation describes the design of policy weavers for interactive-security systems. A policy weaver allows a programmer to specify desired functionality and security guarantees of an application, and automatically obtain a modified application that satisfies such guarantees when executed on an interactive-security system. Each policy weaver consists of (i) a policy language in which the developer expresses desired guarantees, and (ii) a program instrumenter that takes as input an uninstrumented program and a policy in the language, and outputs a program that satisfies the specified policy.

We have designed and evaluated policy weavers for the Capsicum capability system and the HiStar decentralized information-flow control (DIFC) system by designing and applying a policy-weaver generator, which takes as input the semantics of the primitives of each system and outputs a weaver for the system.