Contractual guarantees

Contractual guarantees are more powerful than verified correctness in situations where damages can be adequately redressed in a court of law. For example, in some cases it is stronger to have a money back guarantee than a guarantee of computational correctness. The relationship between cost and security has recently been established by researchers at the Cambridge Computer Laboratory, and is reinforced by scholarly publications by over 100 researchers on the topic of "The Economics of Security."

Over the past few years, a research program on the economics of security has built many cross-disciplinary links and has produced many useful (and indeed delightful) insights from unexpected places. Many perverse aspects of information security that had long been known to practitioners but were dismissed as 'bad weather' have turned out to be quite explicable in terms of the incentives facing individuals and organizations, and in terms of different kinds of market failure.
As for the future, the work of the hundred or so researchers active in this field has started to spill over into two new domains. The first is the economics of security generally, where there is convergence with economists studying topics such as crime and warfare. ...As systems become ever more interconnected, the temptation for system owners to try to dump reliability problems on others will increase. There is thus a search beginning for network protocols and interfaces that are 'strategy-proof' - that is, designed so that the incentives of the principals are properly aligned and no one can gain by cheating. Designing bad behavior out of systems at the start is much more attractive than trying to police it afterward. ( http://www.cl.cam.ac.uk/~twm29/science-econ.pdf, p. 11)

RedPhone Security's network protocol design is based on run-time verification of this simple incentive-allocating principle: No contract, no communication™. In this case, the verifiable contract reference required by the RedPhone Security network protocol and routing system is expected to allocate incentives according to the economic principle of parties' contractual "consideration." By requiring a contract, or similar legally binding agreement for network services, users can leverage the tradition of fairness that has arisen in common law surrounding contracts and binding agreements. This tradition of fairness includes, for example, the following principles: mutual enrichment, statute of frauds, legality of the subject matter, competence of the parties, liability allocation, risk management, legal authority, etc.

Using RedPhone Security’s patent pending design, a reference to a contract (or agreement) is verified by the system's mandatory access controls, and a digital signature over that reference is also verified by the system's mandatory access controls at run-time. This approach may be seen as enhancing traditional, static, formal methods verification by using just-in-time verification. At the same time, the system addresses human incentives stated in an authorizing contract. For these reasons we believe our system addresses what one researcher believes is "urgently needed," as described below:

New methods are urgently needed for effective—and cost-effective—certification of modern systems whose innovations in function, design, or construction present challenges to traditional methods. I have outlined a "scientific" approach to certification that integrates several ideas developed by others, and suggested how it can be extended to compositional certification of component-based systems. I have also advocated consideration of systems whose behavior is partially synthesized at runtime and argued that sound monitoring or synthesis from verified models can support "just-in-time" certification.

A large benefit of the just-in-time approach is that it meshes well with modern ideas of system extent: the idea that the system boundary does not end with the hardware, but extends into the human and societal fabric in which it is located. Many failures are now attributed to the whole system rather than its components [31] and to poorly engineered human interactions (at both individual and societal level), and a failure to anticipate how introduction of a new system changes the organizational context in which it is located [40]. A whole topic of "resilience" has emerged to focus on these topics [25].  (http://www.csl.sri.com/users/rushby/papers/iceccs07.pdf , p. 8)

By linking the function of a reference monitor with a contract, we extend access control decisions, and system security, "into the human and societal fabric in which [the system] is located."