Interface reasoning for interacting systems (IRIS).

Lead Research Organisation: University College London
Department Name: Computer Science

Abstract

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.

Planned Impact

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.

Publications

10 25 50

publication icon
Docherty S (2018) A Stone-type Duality Theorem for Separation Logic Via its Underlying Bunched Logics in Electronic Notes in Theoretical Computer Science

publication icon
Docherty S. (2018) Intuitionistic layered graph logic: Semantics and proof theory in Logical Methods in Computer Science

 
Description Cambridge University Executive Education 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact Cambridge University Executive Education: Dr. Will Venters talking about digital ecosystems / interfaces with executives.
Year(s) Of Engagement Activity 2018
 
Description Fundación Ramón Areces 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Fundación Ramón Areces (Madrid): Dr. Will Venters consulting talking about the challenges of digital interfaces.
Year(s) Of Engagement Activity 2018
 
Description Future Factory 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact Future Factory - 3 day masterclass by Dr. Will Venters on Digital Transformation talking to CDO and CIOs from major manufacturing plants about the challenges of digital interfaces.
Year(s) Of Engagement Activity 2018
 
Description IRIS @ QMUL Industry Day 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Industry/Business
Results and Impact Presentation by Prof Edmund Robinson of a poster about the IRIS project at the QMUL Industry Day.
Year(s) Of Engagement Activity 2018
 
Description Invited Lecture by Byron Cook at OOPSLA/SPLASH 2018 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Formal reasoning about the security of Amazon Web Services
Place: OOPSLA/SPLASH 2018 keynote lecture
Date: November 9, 2018
Year(s) Of Engagement Activity 2018
 
Description Keynote Lecture by David Pym at SYSMICS 2018, Vienna 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Substructural logics: semantics, proof theory, and applications
26-28 February 2018, Vienna (Austria)
Second SYSMICS Workshop

Invited Lecture: David Pym
Title: Logic as a modelling technology: resource semantics, systems modelling, and security
Abstract: The development of BI, the logic of bunched implications, together with its resource semantics, led to the formulation of Separation Logic, which forms the basis of the Infer program analyser deployed in Facebook's code production. However, this rather successful story sits within a broader, quite systematic logical context. I will review the (family of) logics, including process logics, that are supported by resource semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating their uses in a range of modelling applications, including access control, systems security, and workflow simulation.
Year(s) Of Engagement Activity 2018
URL https://sysmics.logic.at/invited
 
Description Lecture Course at SYSMICS Summer School, Les Diablerets, 2018 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Four lectures on logic as a modelling technology. Impact on PhD students.

https://www.dropbox.com/sh/jl3wr3vgx68ajvb/AAA_tT9b7tglSm0fTRHJEqNia?dl=0
Year(s) Of Engagement Activity 2018
URL https://mathsites.unibe.ch/sysmics/
 
Description Plenary Lecture by Byron Cook at FLoC 2018 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Lecture by Byron Cook.
Formal reasoning about the security of Amazon Web Services
Place: FLoC Plenary
Date: July 16, 2018
Year(s) Of Engagement Activity 2018