SUCCESS -- SecUre aCCESSibility for the internet of things

Lead Research Organisation: Middlesex University
Department Name: Faculty of Science & Technology

Abstract

The Internet of Things (IoT) denotes the combination of physical objects with a virtual representation in the Internet. It consists not only of human participants but "Things" as well. The IoT has a great potential to provide novel services to humans in critical areas for society. This innovation however requires updating our understanding of the new risks associated with the new technology so that we can deploy it with confidence and society can trust it.
Amongst the biggest threats to the trustworthiness of new technology are security issues and amongst the main triggers for security problems is human behaviour, either through genuine errors or though malicious intent. The core idea of SUCCESS is to upgrade methods and tools with a proven track record to provide a more holistic consideration of security in relation to human factors within IoT.
Our core scientific innovation will consist on the extension of well-known industry-strength methods in our priority areas. Our technological innovation will provide adequate tools to address trustworthiness within IoT in healthcare environments.
Our project will validate the scientific and technological innovation through pilots, one of which will be in collaboration with a hospital and will allow all stakeholders (e.g. physicians, hospital technicians, patients and relatives) to enjoy a safer system capable to appropriately handle highly sensitive information on vulnerable people.
This innovation will be achieved by a multi-disciplinary team of recognized experts in their fields which has significant experience in knowledge transfer to and from society.
SUCCESS will have significant impact, strengthening the interdisciplinary approach to this important challenge at the crossroads between society and technology, creating new methods for increased security in healthcare, supporting the use of these robust methods by adequate open-source tools, and educating on the use of our products through real-life working prototypes.

Planned Impact

Scientifically, the project SUCCESS will produce: extensions to important existing mechanisms such as the BIP methodology to further improve certified code generation, secure integration of IoT infrastructure, supported with quantitative model checking and with attack trees for user-aware risk analysis and models of human behaviour for security analysis in Isabelle/HOL. The application of the extended methodology to the scenario of dementia patient monitoring provides a demanding and realistic validation of our contributions to support user-aware S&P, a reproducible scientific result in itself.
The impact of the scientific and technological objectives of SUCCESS is perfectly aligned with the expected impact of this call and addresses four out of 10 challenges: - Data visualisation for increasing user awareness of privacy issues - Empowering users with risk evaluation tool for their data and contacts.
- Assistive technology/techniques to encourage more secure behaviour and awareness of users - Dynamic security to allow systems to adapt to varying users.
CHIST-ERA impact: SUCCESS "cross[es] traditional boundaries between disciplines in order to strengthen the community involved in tackling these new challenges". The "range of disciplines" our team covers "include[s] expertise and skills in hardware and software, [...] cryptography, [...] data analysis, business models, user interfaces, user behaviour and human-computer interaction".
SUCCESS will "[h]ave short-term impact on the development of designs, algorithms and prototypes" by extending formal modeling for human-centric IoT security, attack trees for IoT, quantitative model-checking, and certified code generation for BIP extended to IoT and validating these advances on our health care pilots.
These scientific and technological advances "will contribute to the longer term impact of a more user-centric and trustworthy IoT" because the focus of the scientific extensions of SUCCESS lies on user-aware S&P and human understandable risk assessment.
Scientific community impact: SUCCESS will push the importance of security and transparency of IoT higher in the agenda of research groups and companies. Our consortium wants to equip teams with a solution, an IoT security architecture which is reproducible for the community, and above this, to install in the community awareness the importance of developing IoT with user-aware security higher up in their agendas. We expect the technical advances will increase security of existing frameworks on 20% detection rate.
The economic and social impact of SUCCESS: a) Economic Impact: the overall cost for dementia care in Europe is an expected 600 billion Euro, b) Impact on Healthcare: at the present time, the expenditures on health care in the member countries of the European community account for an estimated 8.5% of the GDP and could rise up to 11.8% in 2030. SUCCESS will help this sector by facilitating the creation of automated monitoring of dementia patients, releasing time for nurses and doctors who can focus on more important tasks, c) Impact for Dementia patients: SUCCESS improves privacy for dementia patients from first diagnosis to care. It mitigates problems with insurance companies and employers of dementia patients. User-centred flexibility will be increased by 20% as judged by technical teams (in our case healthcare support). Compared to specialized installation with (specialized HW and SW) we will be able to offer same security at a reduced 20% cost.

Publications

10 25 50
 
Description The findings of the project SUCCESS have been leading to a number of follow up research outputs and increased interest in the logical framework conceived within the project that have in a first instance lead to a number of follow up projects and publications in the academic research sector and are currently leading to the definition of a new summer school in the area of research at Middlesex University. In addition, the research of the project has transgressed into teaching materials and practical case studies and labs for students. Thereby, a societal impact has been generated and the open source tools provided are further used in ongoing research projects.
First Year Of Impact 2020
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Societal

 
Description UK Research Institute in Verified Trustworthy Software Systems (https://vetss.org.uk)
Amount £50,000 (GBP)
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 10/2018 
End 04/2019
 
Title Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems 
Description Attack Trees are a well established and useful model for the construction of at- tacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we succeed in developing a generic theory of Attack Trees with a state-based semantics based on Kripke structures and CTL (see [2] for more details). The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of Attack Trees and at the same time the developed proof the- ory enables application to case studies. A central correctness and com- pleteness result proved in Isabelle establishes a connection between the notion of Attack Tree validity and CTL. The application is illustrated on the example of a healthcare IoT system and GDPR compliance ver- ification. A more detailed account of the Attack Tree formalisation is given in [3] and the case study is described in detail in [4]. [2] F. Kammüller. Isabelle modelchecking for insider threats. In Data Pri- vacy Management, DPM'16, 11th Int. Workshop, volume 9963 of LNCS. Springer, 2016. Co-located with ESORICS'16. [3] F. Kammüller. Attack trees in isabelle. In 20th International Confer- ence on Information and Communications Security, ICICS2018, volume 11149 of LNCS. Springer, 2018. [4] F. Kammüller. Formal modeling and analysis of data protection for gdpr compliance of iot healthcare systems. In IEEE Systems, Man and Cybernetics, SMC2018. IEEE, 2018. 
Type Of Material Computer model/algorithm 
Year Produced 2020 
Provided To Others? Yes  
Impact The Archive of Formal Proof is a public database of Isabelle development of wider importance and makes them available (sources and documentation) to the community. 
URL http://www.isa-afp.org/browser_info/current/AFP/Attack_Trees/document.pdf
 
Title SUCCESS Opens Source repository 
Description The software, its manuals and the related technical documentation are available on publicly accessible repositories on Github at https://github.com/success-iot/software as described in Milestone 8 (M5.2 of our project deliverables). Summarising, these Open Source tools used on the case studies of the Project but each in itself contributes a more general tool useful for a wider community. These tools are • Pilot 1 setup at MU • ATTop [4] • SBIP [5] • Plasma [1] • Isabelle Insider framework [2] [1] D. Beaulaton, I. Cristescu, A. Legay, and J. Quilbeuf. A modeling language for security threats of iot systems. In F. Howar and J. Barnat, editors, Formal Methods for Industrial Critical Systems, pages 258-268, Cham, 2018. Springer International Publishing. [2] F. Kammu ¨ller. Attack trees in isabelle. In 20th International Conference on Information and Communications Security, volume 11149 of LNCS. Springer, 2018. [4] R. Kumar, S. Schivo, E. Ruijters, B. M. Yildiz, D. Huistra, J. Brandt, A. Rensink, and M. Stoelinga. Effective analysis of attack trees: A model-driven approach. In A. Russo and A. Schu ¨rr, editors, Fundamental Approaches to Software Engineering, 21st International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings., volume 10802 of Lecture Notes in Computer Science, pages 56-73. Springer, 2018. [5] B. L. Mediouni, A. Nouri, M. Bozga, M. Dellabani, A. Legay, and S. Bensalem. S BIP 2.0: Statistical model checking stochastic real-time systems. In S. K. Lahiri and C. Wang, editors, Automated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings, volume 11138 of Lecture Notes in Computer Science, pages 536-542. Springer, 2018. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
Impact While all documents and preliminary results are kept confidential and secure, the opening of the software at the above Open Source repository increases the trust towards the security of the tools. It will also encourage the community to participate in further software improvements during and after the end of the project. The GDPR (General Data Privacy Regulation) is since 26th of May 2018 the new data protection law in Europe and also applies to all suppliers of software. As has been shown as part of this Project [3], it is possible to use the Isabelle Insider framework to prove GDPR compliance at the architectural level for the IoT healthcare case study of the project. [3] F. Kammu ¨ller. Formal modeling and analysis of data protection for gdpr compliance of iot healthcare systems. In IEEE Systems, Man, and Cybernetics, IEEE SMC'18. IEEE, 2018. 
 
Description Invitation to present at CISA seminar University of Edinburgh 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact The CISA seminar is the research meeting to the
Artificial Intelligence and its Applications Institute
AIAI https://web.inf.ed.ac.uk/aiai/events
at Unversity of Edinburgh.
They invited me to talk aboiut my finding in SUCCESS on Attack Trees in Isabelle.
Year(s) Of Engagement Activity 2018
URL https://web.inf.ed.ac.uk/aiai/events
 
Description Participation in Discussion Panel 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact The two Workshops DPM (Data Privacy Management) and CBT (Cryptocurrencies and Blockchain Technologies)
both co-located with the conference ESORICS 2020 organised a Panel on:
How cryptocurrency and blockchain technology will become a trust foundation for the New Normal while ensuring data privacy management?
They invited me to participate in the panel give a short overview talk about
the Corona-Virus-App analysis that I had presented at DPM and that was very well received.
The below link to the Workshop programme has a publicly available YouTube https://youtu.be/_9etsQsD6C4 recording of the Panel.
Year(s) Of Engagement Activity 2020
URL https://deic.uab.cat/conferences/dpm/dpm2020/program.html