Biblio

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.