Khan, Muhammad Taimoor ORCID: https://orcid.org/0000-0002-5752-6420, Serpanos, Dimitrios and Shrobe, Howard (2021) Towards scalable security of real-time applications: a formally certified approach. In: 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA ). IEEE Xplore . Institute of Electrical and Electronics Engineers (IEEE), Piscataway, New Jersey, 01-04. ISBN 978-1728129907; 978-1728129891 (doi:10.1109/ETFA45728.2021.9613489)

PDF (Accepted paper (IEEE)) 41629_KHAN_Towards_Scalable_Security_of_Real-time_Applications_A_Formally_Certified_Approach.pdf - Accepted Version Restricted to Registered users only Download (688kB) | Request a copy

Abstract

In this paper, we present our ongoing work to develop an efficient and scalable verification method to achieve runtime security of real-time applications with strict performance requirements. The method allows to specify (functional and non-functional) behaviour of a real-time application and a set of known attacks/threats. The challenge here is to prove that the runtime application execution is at the same time (i) correct w.r.t. the functional specification and (ii) protected against the specified set of attacks, without violating any non-functional specification (e.g., real-time performance). To address the challenge, first we classify the set of attacks into computational, data integrity and communication attacks. Second, we decompose each class into its declarative properties and definitive properties. A declarative property specifies an attack as a one big-step relation between initial and final state without considering intermediate states, while a definitive property specifies an attack as a composition of many small-step relations considering all intermediate states between initial and final state. Semantically, the declarative property of an attack is equivalent to its corresponding definitive property. Based on the decomposition and the adequate specification of underlying runtime environment (e.g., compiler, processor and operating system), we prove rigorously that the application execution in a particular runtime environment is protected against declarative properties without violating runtime performance specification of the application. Furthermore, from the specification, we generate a security monitor that assures that the application execution is secure against each class of attacks at runtime without hindering real-time performance of the application.

Item Type:	Conference Proceedings
Title of Proceedings:	2021 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA )
Additional Information:	2021 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA ).
Uncontrolled Keywords:	cyber security; formal analysis; real-time security
Subjects:	Q Science > QA Mathematics > QA75 Electronic computers. Computer science Q Science > QA Mathematics > QA76 Computer software
Faculty / School / Research Centre / Research Group:	Faculty of Engineering & Science Faculty of Engineering & Science > Internet of Things and Security Research Centre (ISEC) Faculty of Engineering & Science > School of Computing & Mathematical Sciences (CMS)
Last Modified:	28 Apr 2023 10:27
URI:	http://gala.gre.ac.uk/id/eprint/41629

Actions (login required)

View Item

Downloads