Biblio

Cyber-has often been considered as a coordination and control, as opposed to collaborative influence, media. This conceptual-design paper, uniquely, builds upon a number of entangled, cross disciplinary research strands – integrating engineering and conflict studies – and a detailed literature review to propose a new paradigm of assurance and deterrence models. We consider an ontology for Cyber-sûréte, which combines both the social trusts necessary for [knowledge &, information] assurance such as collaboration by social influence (CSI) and the technological controls and rules for secure information management referred as coordination by rule and control (CRC). We posit Cyber-sûréte as enabling both a 'safe-to-fail' ecology (in which learning, testing and adaptation can take place) within a fail-safe supervisory control and data acquisition (SCADA type) system, e.g. in a nuclear power plant. Building upon traditional state-based threat analysis, we consider Warning Time and the Threat equation with relation to policies for managing Cyber-Deterrence. We examine how the goods of Cyber-might be galvanised so as to encourage virtuous behaviour and deter and / or dissuade ne'er-do-wells through multiple transparencies. We consider how the Deterrence-escalator may be managed by identifying both weak influence and strong control signals so as to create a more benign and responsive cyber-ecology, in which strengths can be exploited and weaknesses identified. Finally, we consider declaratory / mutual transparencies as opposed to legalistic / controlled transparency.

We present Minesweeper, a tool to verify that a network satisfies a wide range of intended properties such as reachability or isolation among nodes, waypointing, black holes, bounded path length, load-balancing, functional equivalence of two routers, and fault-tolerance. Minesweeper translates network configuration files into a logical formula that captures the stable states to which the network forwarding will converge as a result of interactions between routing protocols such as OSPF, BGP and static routes. It then combines the formula with constraints that describe the intended property. If the combined formula is satisfiable, there exists a stable state of the network in which the property does not hold. Otherwise, no stable state (if any) violates the property. We used Minesweeper to check four properties of 152 real networks from a large cloud provider. We found 120 violations, some of which are potentially serious security vulnerabilities. We also evaluated Minesweeper on synthetic benchmarks, and found that it can verify rich properties for networks with hundreds of routers in under five minutes. This performance is due to a suite of model-slicing and hoisting optimizations that we developed, which reduce runtime by over 460x for large networks.