Secure Programming via Game-based Synthesis
William R. Harris
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.
(Click here to access the dissertation:
PDF.)
University of Wisconsin