Necessity Specifications for Robustness

TL;DR

This paper introduces Necessity, a formal language and proof system for specifying and verifying robustness properties of modules against malicious inputs, with mechanization in Coq.

Contribution

It presents a novel necessity language with temporal operators and a proof logic to derive explicit robustness specifications from functional specs.

Findings

Necessity specifications can express complex robustness properties.

The proof logic is sound and mechanized in Coq.

Demonstrates the approach with an exemplar proof.

Abstract

Robust modules guarantee to do only what they are supposed to do - even in the presence of untrusted, malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.