Interface reasoning for interacting systems (IRIS).

The smooth functioning of society is critically dependent not only on the correctness of programs, particularly of programs controlling critical and high-sensitivity core components of individual systems, but also upon correct and robust interaction between diverse information-processing ecosystems of large, complex, dynamic, highly distributed systems. Failures are common, unpredictable, highly disruptive, and span multiple organizations.

The scale of systems' interdependence will increase by orders of magnitude in the next few years. Indeed by 2020, with developments in Cloud, the Internet of Things, and Big Data, we may be faced with a world of 25 million apps, 31 billion connected devices, 1.3 trillion tags/sensors, and a data store of 50 trillion gigabytes (data: IDC, ICT Outlook: Recovering Into a New World, #DR2010_GS2_JG, March 2010). Robust interaction between systems will be critical to everyone and
every aspect of society. Although the correctness and security of complete systems in this world cannot be verified, we can hope to be able to ensure that specific systems, such as verified safety-, security-, or identity-critical modules, are correctly interfaced.

The recent success of program verification notwithstanding, there remains little prospect of verifying such ecosystems in their entireties: the scale and complexity are just too great, as are the social and managerial coordination challenges. Even being able to define what it means to verify something that is going to have an undetermined role in a larger system presents a serious challenge. It is perhaps evident that the most critical aspect of the operation of these
information-processing ecosystems lies in their interaction: even perfectly specified and implemented individual systems may be used in contexts for which they were not intended, leading to unreliable, insecure communications between them.

We contend that interfaces supporting such interactions are therefore the critical mechanism for ensuring systems behave as intended. However, the verification/modelling techniques that have been so effective in ensuring reliability of low-level features of programs, protocols, and policies (and so the of the software that drives large systems) are, essentially, not applied to reasoning about such large-scale systems and their interfaces. We intend to explore this deficiency by researching
the technical, organizational, and social challenges of specifying and verifying interfaces in system ecosystems. In so doing, we will drive the use of verification techniques and improve the reliability of large systems.

Complex systems ecosystems and their interfaces are some of the most intricate and critical information ecosystems in existence today, and are highly dynamic and constantly evolving. We aim to understand how the interfaces between the components constituting these ecosystems work, and to verify them against their intended use. This research will be
undertaken through a collection of different themes covering systems topics where interface is crucially important, including critical code, communications and security protocols, distributed systems and networks, security policies, business ecosystems, and even extending to the physical architecture of buildings and networks. These themes are representative of the problem of specifying and reasoning about the correctness of interfaces at different levels of abstraction and criticality.

Interfaces of each degree of abstraction and criticality can be studied independently, but we believe that it will be possible to develop a quite general, uniform account of specifying and reasoning about them. It is unlikely that any one level of abstraction will suggest all of the answers: we expect that the work of the themes will evolve and interact
in complex ways.

1. Who will benefit from this research? 2. How will they benefit from this research?

The beneficiaries of this research fall into the following groups: academic and industrial researchers; engineers analyzing and verifying code bases; systems architects and developers; managers with responsibility for structuring (possibly large, complex) organizations in the public and private sectors; policy-makers and regulators.

In the short term, the main beneficiaries of this research will be academic and industrial researchers in program verification, security, distributed systems, and management science. This benefit will derive from new scientific tools and methodologies and new formulations of research challenges, in which closely related problems concerned with the interfaces between communicating systems can be understood with a common conceptual framework. This impact will be achieved through the
well-established academic and scientific dissemination routes, including publications in top-rank conferences and journals and research seminars, as well as workshops with stakeholders, and other speaking opportunities. This will further reinforce the UK's leading position in verification research.

London is the global centre for the deployment of program analysis and verification techniques within the operations of the major technology companies such as Facebook and Amazon. These companies operate complex distributed systems, recognize the need to reason about their interactions, and need to employ suitably qualified staff to deliver this. IRIS will stimulate further investment in verification technologies and their deployment in London and will develop a pipeline
of researchers able to take forward a new, interdisciplinary field of systems verification, so reinforcing the UK's leading position in this important technology.

In the medium term, systems architects and developers in technology companies can hope to have system analysis tools --- for analysing and/or verifying the structure of their ecosystems via analysing and/or verifying the properties of system interfaces and the information flows across them --- of effectiveness/efficiency, and rigorous basis, that is
comparable to that of Facebook's recently open-sourced INFER tool (https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/). We anticipate also that IRIS will lead to subsequent research projects that will further develop its
ideas in its original and other directions and that these projects will train more staff, so continuing the pipeline of staff to out client technology companies.

In the long term, managers with responsibility for structuring (possibly large, complex) organizations in the public and private sectors will benefit from both improved understanding within their communities of the significance of good information-flow design for the effective operation of complex organizations and from the availability of conceptual tools
to support their decision that reflect this understanding. All of this should lead to improved efficiency and reliability of the services they offer to society, so helping to improve quality of life and commercial/creative output.

Similarly, policy-makers and regulators (especially in respect of sectors such as security and critical infrastructure) will benefit from improved understanding of the potential sources of vulnerability (to threats to efficiency, reliability, and security) in the complex ecosystems of systems upon which the smooth function of society depends. They will also benefit from conceptual tools to support their design of policy and regulatory mechanisms intended to ensure, for example,
adequate investment by the ecosystem stakeholders to ensure that systems communicate with sufficient integrity. Thus the robustness of society's critical infrastructure will be reinforced.