XClose

UCL Computer Science

Home
Menu

Interface reasoning for interacting systems (IRIS)

The project will provide a systematic, rigorous theory for reasoning about how complex, large-scale systems communicate with one another.

Project summary

The IRIS project — Interface Reasoning for Interactive Systems — will provide a systematic, rigorous theory for reasoning about how complex, large-scale systems communicate with one another and do so in a way which supports the development and deployment of verification tools. IRIS builds upon recent spectacular successes, originated and led by its team, in program verification. These now enable us for the first time to address issues that present at the level of the large, complex, dynamic, highly-distributed systems that we now critically depend upon in our daily and commercial lives. IRIS will develop the techniques pioneered for programs so that they can be applied in much wider scope to deliver much more robust systems ecosystems. This will be achieved through interconnected and mutually supporting component projects, drawing upon common foundations, that span theory and application, across the range of system scales: systems security; general code interfacing; reasoning about protocols; and policy and organizational management.


About

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.

We will be using ideas from a range of disciplines, including logic, program verification, security, discrete mathematical modelling, economics, and management science.

We have a great set of industrial partners: Amazon AWS, BT, Facebook, GridPP, HP Labs, and Methods Group.

EPSRC’s page for the project, including a summary, partners, duration, and value, is at http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/R006865/1.

Back to the top


Publications and presentations

background publications
James Brotherston – UCL

An Introduction to Separation Logic, Delivered at Oracle Labs, Brisbane in Dec 2015, with accompanying slides.

YouTube Widget Placeholderhttps://www.youtube.com/watch?v=n2F994DVKWE

 
David Pym - UCL
Edmund Robinson - UCL
  • C Hermida, US Reddy, EP Robinson. Logical relations and parametricity–a Reynolds programme for category theory and programming languages Electronic Notes in Theoretical Computer Science 303, 149-180. https://doi.org/10.1016/j.entcs.2014.02.008
  • COLLINSON, M., PYM, D., & ROBINSON, E. (2008). Bunched polymorphism. Mathematical Structures in Computer Science, 18(6), 1091-1132. https://doi:10.1017/S0960129508007159
  • EP Robinson, Variations on Algebra: Monadicity and Generalisations of Equational Theories Formal Aspects of Computing (2002) 13: 308  https://doi.org/10.1007/s001650200014
  • John Power and Edmund Robinson. 2000. Logical relations, data abstraction, and structured fibrations. In Proceedings of the 2nd ACM SIGPLAN international conference on Principles and practice of declarative programming (PPDP ’00), Frank Pfenning (Ed.). ACM, New York, NY, USA, 15-23. D OI=http://dx.doi.org/10.1145/351268.351271
Alistair Donaldson – Imperial
  • A. Betts, N. Chong, A. F. Donaldson, J. Ketema, S. Qadeer, P. Thomson, and J. Wickerson. The design and implementation of a verification technique for GPU kernels. TOPLAS, 37(3):10, 2015. https://dl.acm.org/citation.cfm?doid=2743017
  • A. F. Donaldson, J. Ketema, T.Sorensen, J. Wickerson. Forward Progress on GPU Concurrency. 28th International Conference on Concurrency Theory, {CONCUR} 2017, p. 1:1–1:13.  https://doi.org/10.4230/LIPIcs.CONCUR.2017.1
  • T. Sorensen, H. Evrard and  Alastair F. Donaldson, Cooperative Kernels: GPU Multitasking for Blocking Algorithms.  Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, {ESEC/FSE} 2017, Paderborn, Germany, September 4-8, (2017),  p. 431–441. ttp://doi.acm.org/10.1145/3106237.3106265
presentations

Peter O’Hearn and Byron Cook recently presented at the plenary session of FLoC 2018.

YouTube Widget Placeholderhttps://youtu.be/JfjLKBO27nw

 

YouTube Widget Placeholderhttps://youtu.be/HW5Zq1TsQqU


People

Meet the people behind this project.

David Pym (Principal Investigator)

David is a logician, mathematician, and computer scientist. His research is mainly in logic, where he works in both pure logic and on developing logic-based methods as a mathematical modelling technology for reasoning about systems and behaviour, and in security, where he works in security policy, security economics, and systems security modelling.

His contributions have been mainly in the following areas: dependent type theory and logical frameworks, including proof theory, semantics, and unification algorithms; reductive logic and proof-search, including proof theory and semantics, for classical intuitionistic, and substructural logics; categorical models of the classical sequent calculus and its theory of reduction; the bunched logic BI and its relatives, including proof theory, semantics, algebraic theory, and computational interpretations, and their applications to program logics, including Separation Logic, and security; distributed systems modelling based on resource semantics and process algebra; modal and epistemic bunched logics and layered graph logics, with applications in access control; utility-theoretic concepts in distributed systems modelling and process algebra, with applications in systems security modelling; trust domains; information security economics; the philosophy and methodology of information security; public policy in information security, including information stewardship.

He has a broad experience of research, teaching, and management in leading universities and in industry.

Visit David's profile

George Danezis (Co-Investigator)

George Danezis is a Professor of Security and Privacy Engineering at the Department of Computer Science of University College London, and Head of the Information Security Research Group. He has been working on anonymous communications, privacy enhancing technologies (PET), and traffic analysis since 2000. He has previously been a researcher for Microsoft Research, Cambridge; a visiting fellow at K.U.Leuven (Belgium); and a research associate at the University of Cambridge (UK), where he also completed his doctoral dissertation under the supervision of Prof. R.J. Anderson.

His theoretical contributions to the Privacy Technologies field include the established information theoretic and other probabilistic metrics for anonymity and pioneering the study of statistical attacks against anonymity systems. On the practical side he is one of the lead designers of the anonymous mail system Mixminion, as well as Minx, Sphinx, Drac and Hornet; he has worked on the traffic analysis of deployed protocols such as Tor.

His current research interests focus around secure communications, high-integirty systems to support privacy, smart grid privacy, peer-to-peer and social network security, as well as the application of machine learning techniques to security problems. He has published over 70 peer-reviewed scientific papers on these topics in international conferences and journals.

He was the co-program chair of ACM Computer and Communications Security Conference in 2011 and 2012, IFCA Financial Cryptography and Data Security in 2011, the Privacy Enhancing Technologies Workshop in 2005 and 2006. He sits on the PET Symposium board and ACM CCS Steering committee and he regularly serves in program committees of leading conferences in the field of privacy and security. He is a fellow of the British Computing Society since 2014.

Visit George's profile

Peter O'Hearn (Co-Investigator)

Peter is a Research Scientist working with the Static Analysis Tools team in the Facebook London Engineering office. I came to Facebook in 2013 with the acquisition of the verification startup Monoidics, and before that he held academic positions at Syracuse University, Queen Mary University of London and University College London. He maintains a part-time Professor position at UCL.

His research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of formal proof. With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program verification. Subsequent work in academic program analysis eventually led to the the Monoidics/Facebook Infer program analyzer, which is notable for supporting deep reasoning about big code that is undergoing rapid concurrent modification. Infer currently runs in production at Facebook, where it helps thousands of bugs be fixed each month before reaching production.

He has received a number of awards for his work in verification including the 2016 CAV Award and the 2016 Godel Prize. He was elected fellow of the UK Royal Academy of Engineering in 2016.

Visit Peter's profile

Edmund Robinson (Co-Investigator)

Edmund is a mathematician and computer scientist.  He was educated at Cambridge, obtaining my PhD in mathematics in 1984. He then took a research position at the Department of Computer Science in Edinburgh, before returning to Cambridge as a research fellow. In 1987 he left his fellowship for an Assistant Professorship at Queen’s University in Canada. From there he came back to the UK in 1990 as first a lecturer, then an EPSRC Advanced Fellow and finally a Reader at the School of Cognitive and Computing Sciences in Sussex. His last move was when he came to Queen Mary as Professor in 1995. In 2002 he was appointed Head of the Department of Computer Science and then charged with its merger with Electronic Engineering to form the new School of Electronic Engineering and Computer Science, of which he was the founding Head until August 2010. Since coming to the end of his term as Head he has been on sabbatical, and filling in for Prof Ursula Martin as Acting Director of ImpactQM. For more details check his CV.

Visit Edmund's profile

James Brotherston (Co-Investigator)

James Brotherston is a Reader in Logic and Computation in the Dept. of Computing at UCL, where he is a member of the Programming Principles, Logic and Verification (PPLV) research group.  James holds a PhD from the School of Informatics, University of Edinburgh 2006; he was then a postdoctoral researcher at Imperial College London and, briefly, a lecturer at Queen Mary University of London before moving to UCL in 2012.

James’ main research interests lie in mathematical logic and its application to computer science, especially in automated program verification. He is especially well known for his pioneering work on cyclic proof, and for his work on the foundations of separation logic.

Visit James' profile

Byron Cook (Co-Investigator)

Byron Cook is Professor of Computer Science at University College London (UCL) and Director at Amazon Web Services. Byron’s interests include computer/network security, program analysis/verification, programming languages, theorem proving, logic, hardware design, operating systems, and biological systems. At Amazon Byron leads a research group focused on formal/constraint-based tools for reasoning about cloud-computing security.

Visit Byron's profile

William Venters (Co-Investigator)

Dr Will Venters is an Assistant Professor in Information Systems and Digital Innovation within the Department of Management at the London School of Economics and Political Science (LSE). His research interests include cloud computing, digital platforms and digital innovation approaches. He has a first-class degree in computer science and a PhD in information systems. His research work has been published in major refereed journals including MIS Quarterly, Journal of Information Technology, the Journal of Management Studies, and the Information Systems Journal. He co-authored the Palgrave book “Moving to the Cloud Corporation” and is the author of a blog on digital technology www.binaryblurring.com and is an associate editor of the Journal Information Technology and People. He speaks regularly at practitioner conferences on various digital business issues, particularly around Digital Ecosystems, Digital Innovation and Cloud Computing; has briefed  European government policy makers and various company executives; and has undertaken consultancy in IT strategy and Digital issues.

Visit William's profile

Alastair Donaldson (Co-Investigator)

Alastair Donaldson is a Reader and EPSRC Early Career Fellow in the Department of Computing, Imperial College London, where he leads the Multicore Programming Group, and is director of GraphicsFuzz, a spin-out company specialising in automated testing for graphics drivers. He is the recipient of the 2017 BCS Roger Needham Award for his research into many-core programming. He has published more than 70 peer-reviewed papers on programming languages, formal verification, software testing and parallel programming, and leads the GPUVerify project on automatic verification of GPU kernels – a collaboration with Microsoft Research – and the GLFuzz project on automated testing for graphics shader compilers. Alastair coordinated the FP7 project CARP: Correct and Efficient Accelerator Programming, which completed successfully in 2015. Before joining Imperial, Alastair was a Visiting Researcher at Microsoft Research Redmond, an EPSRC Postdoctoral Research Fellow at the University of Oxford and a Research Engineer at Codeplay Software Ltd. He holds a PhD from the University of Glasgow, and is a Fellow of the British Computer Society.

Visit Alastair's profile

Back to the top


Organisations and industry partners

Find out more about the organisations and industry partners involved in the IRIS project.

Organisations
industry partners

Back to the top