Journal of Computer Security

Access control is fundamental in protecting information systems but it can also pose an obstacle to achieving business objectives. We analyze this tradeoff and its avoidance in the context of systems modeled as workflows restricted by authorization constraints, including those specifying Separation of Duty (SoD) and Binding of Duty (BoD). To begin with, we present a novel approach to scoping authorization constraints within workflows with loops and conditional execution. We formalize workflows, authorization constraints, and their enforcement using the process algebra CSP and visualize our constraints by extending the workflow modeling language BPMN. Afterwards, we consider enforcement's effects on business objectives. We identify the notion of obstruction, which generalizes deadlock within a system where access control is enforced, and we formulate the existence of an obstruction-free enforcement mechanism as a decision problem. We present complexity bounds for this problem and give an approximation algorithm that performs well when authorizations are evenly distributed among users. We provide tool support for our constraints in an extension of the modeling platform Oryx and report on the performance of our algorithms' implementation.

This paper introduces YARRA, a conservative extension to C to protect applications from non-control data attacks. YARRA programmers specify their data integrity requirements by declaring critical data types and ascribing these critical types to important data structures. YARRA guarantees that such critical data is only written through pointers with the given static type. Any attempt to write to critical data through a pointer with an invalid type (perhaps because of a buffer overrun) is detected dynamically. We formalize YARRA’s semantics and prove the soundness of a program logic designed for use with the language. A key contribution is to show that YARRA's semantics are strong enough to support sound local reasoning and the use of a frame rule, even across calls to unknown, unverified code. We evaluate a prototype implementation of a compiler and runtime system for YARRA by using it to harden four common server applications against known non-control data vulnerabilities. We show that YARRA successfully defends the applications against these attacks. In our initial experiments, we find that the performance impact of YARRA is small, provided the amount of critical data is small and the application is not compute intensive.

We present StatVerif, which is an extension of the ProVerif process calculus with constructs for explicit state, in order to be able to reason about protocols that manipulate global state. Global state is required by protocols used in hardware devices (such as smart cards and the trusted platform module), as well as by protocols involving databases that store persistent information. We provide the operational semantics of StatVerif. We extend the ProVerif compiler to a compiler for StatVerif, which takes processes written in the extended process language and produces Horn clauses. Our compilation is carefully engineered to avoid many false attacks. We prove the correctness of the StatVerif compiler. We illustrate our method on two examples: a small hardware security device and a contract signing protocol. We are able to prove their desired properties automatically.

We describe how to verify security properties of C code for cryptographic protocols by using a general-purpose verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security simply by writing suitable header files and annotations in implementation files, rather than by changing VCC itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.