Cyber War, Formal Verification and Certified Infrastructure

Cyber war is recognized to be real. Like all wars this is bad for many people, but not for manufacturers of weapons. An attacker in cyber war can be defined as an unauthorized user process without access to physical side channels; with physical access we would be back to ordinary warfare and espionage. IT infrastructure which - by separation theorems - can be guaranteed to be immune against such attackers is therefore a defensive weapon in cyber war. The verification community is the only potential manufacturer of such infrastructure and thus has a chance to access resources vastly superior to those for ordinary research and development.

In order to develop such infrastructure, one would have to

1

develop a pervasive mathematical theory of IT infrastructure

2

formally verify it

3

convince industry and politicians, that the specifications of this theory are meaningful and

4

convince certification agencies, that all verification tools involved are sound

Problem (3) could be solved by providing standardized machine readable specifications of the usual components of IT infrastructure. Note that agreeing on standards is usually a non trivial sociological process. (1), (2) and (4) are ’ordinary’ technical problems. In the main part of this talk we will review the state of the art for these problems and estimate the resources to resolve the remaining open subproblems. The resulting costs are large compared to normal research budgets and very small compared to the cost of war.