On Synthesis of Runtime Security Monitor for Real-time IoT Applications

We report on the evaluation of an efficient and scalable verification method that assures runtime security of real-time Internet of Things (IoT) applications with strict performance requirements. Modeling known threats at abstract but practical level is key to assure security of efficient and scalable IoT applications. To this end, the method classifies set of known attacks into computational , data integrity and communication attacks. Then, each attack class is decomposed into declarative properties and definitive properties . A declarative property specifies an attack as a single big-step relation between initial and final state by ignoring intermediate states, while a definitive property specifies an attack as a sequence of numerous small-step relations considering all intermediate states between initial and final state. Finally, the declarative properties are translated into runtime security monitor that assures protection of the application execution against known threats without defying runtime application’s performance requirements. in particular, we evaluate the methodology through its application to an energy management application of smart home.

Content

Author and article information

Contributors

Muhammad Taimoor Khan

Dimitrios Serpanos

Howard Shrobe

Conference

Publication date: September 2019

Publication date (Print): September 2019

Pages: 82-88

Affiliations

[0001]School of Computing and Mathematical Sciences

University of Greenwich, London, UK

[0002]Industrial Systems Institute, RC-ATHENA and ECE, University of Patras, Patras, Greece

[0003]CSAIL, MIT

Cambridge, USA

Article

DOI: 10.14236/ewic/icscsr19.11

SO-VID: f5e6bc26-50cd-4611-b804-24b689a3f543

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: 6th International Symposium for ICS & SCADA Cyber Security Research 2019

Conference acronym: ICS-CSR

Conference number: 6

Conference location: Athens, Greece

Conference date: 10th-12th September 2019

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Cyber Security Research

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/icscsr19.11

Self URI (journal page): https://ewic.bcs.org/

REFERENCES

W. ZhangY. MengY. LiuX. ZhangY. ZhangH. Zhu 2018 Homonit: Monitoring smart home apps from encrypted traffic Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, ser CCS ’18 New York, USA: ACM 1074 1088
M. TilocaK. NikitinS. Raza 2017 Axiom: Dtls-based secure iot group communication ACM Trans. Embed. Comput. Syst. 16 3 66 1 66 29
M. B. SoudanH. M. Al RifaieT. M. AsmarS. Majzoub 2018 Smart home energy management system: An exploration of iot use cases Advances in Science and Engineering Technology International Conferences (ASET) 1 5
M. T. KhanD. SerpanosH. Shrobe 2016 A rigorous and efficient run-time security monitor for real-time critical embedded system applications IEEE 3rd World Forum on Internet of Things (WFIoT) 100 105
I. CassarA. FrancalanzaL. AcetoA. Ingólfsdóttir 2017 A survey of runtime monitoring instrumentation techniques
N. LiA. Raghunathan 2011 Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system IEEE 13th International Conference on e-Health Networking, Applications and Services 150 156
CAPEC Online 2019 Available: https://capec.mitre.org
A. Chlipala 2016 Ur/web: A simple model for programming the web Commun. ACM 59 8 93 100
D. KästnerJ. BarrhoU. WünscheM. SchlicklingB. SchommerM. SchmidtC. FerdinandX. LeroyS. Blazy 2018 CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler ERTS2 2018 - Embedded Real Time Software and Systems Toulouse, France
A. ReidR. ChenA. DeligiannisD. GildayD. HoyesW. KeenA. PathiraneO. ShepherdP. VrabelA. Zaidi 2016 End-to-end verification of arm processors with isa-formal Computer Aided VerificationS. ChaudhuriA. Farzan Cham: Springer International Publishing 42 58
M. T. KhanD. SerpanosH. Shrobe 2018 Armet: Behavior-based secure and resilient industrial control systems Proceedings of the IEEE 106 1 129 143
M. T. KhanM. PinzgerD. SerpanosH. Shrobe 2019 Runtime protection of real-time critical control applications against known threats IEEE Design & Test no. In Review
B. DelawareC. Pit-ClaudelJ. GrossA. Chlipala 2015 Fiat: Deductive synthesis of abstract data types in a proof assistant Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL, Mumbai, India 689 700

Comments

Comment on this article

[1] W. ZhangY. MengY. LiuX. ZhangY. ZhangH. Zhu 2018 Homonit: Monitoring smart home apps from encrypted traffic Proceedings of the ACM SIGSAC Conference on Computer and Communications Security, ser CCS ’18 New York, USA: ACM 1074 1088

[2] M. TilocaK. NikitinS. Raza 2017 Axiom: Dtls-based secure iot group communication ACM Trans. Embed. Comput. Syst. 16 3 66 1 66 29

[3] M. B. SoudanH. M. Al RifaieT. M. AsmarS. Majzoub 2018 Smart home energy management system: An exploration of iot use cases Advances in Science and Engineering Technology International Conferences (ASET) 1 5

[4] M. T. KhanD. SerpanosH. Shrobe 2016 A rigorous and efficient run-time security monitor for real-time critical embedded system applications IEEE 3rd World Forum on Internet of Things (WFIoT) 100 105

[5] I. CassarA. FrancalanzaL. AcetoA. Ingólfsdóttir 2017 A survey of runtime monitoring instrumentation techniques

[6] N. LiA. Raghunathan 2011 Hijacking an insulin pump: Security attacks and defenses for a diabetes therapy system IEEE 13th International Conference on e-Health Networking, Applications and Services 150 156

[7] CAPEC Online 2019 Available: https://capec.mitre.org

[8] A. Chlipala 2016 Ur/web: A simple model for programming the web Commun. ACM 59 8 93 100

[9] D. KästnerJ. BarrhoU. WünscheM. SchlicklingB. SchommerM. SchmidtC. FerdinandX. LeroyS. Blazy 2018 CompCert: Practical Experience on Integrating and Qualifying a Formally Verified Optimizing Compiler ERTS2 2018 - Embedded Real Time Software and Systems Toulouse, France

[10] A. ReidR. ChenA. DeligiannisD. GildayD. HoyesW. KeenA. PathiraneO. ShepherdP. VrabelA. Zaidi 2016 End-to-end verification of arm processors with isa-formal Computer Aided VerificationS. ChaudhuriA. Farzan Cham: Springer International Publishing 42 58

[11] M. T. KhanD. SerpanosH. Shrobe 2018 Armet: Behavior-based secure and resilient industrial control systems Proceedings of the IEEE 106 1 129 143

[12] M. T. KhanM. PinzgerD. SerpanosH. Shrobe 2019 Runtime protection of real-time critical control applications against known threats IEEE Design & Test no. In Review

[13] B. DelawareC. Pit-ClaudelJ. GrossA. Chlipala 2015 Fiat: Deductive synthesis of abstract data types in a proof assistant Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL, Mumbai, India 689 700

Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65