On the Behavioural Formalization of the Cognitive Middleware AWDRAT

We present our ongoing work and initial results towards the (behavioral) correctness analysis of the cognitive middleware AWDRAT. Since, the (provable) behavioral correctness of a software system is a fundamental pre-requisite of the system's security. Therefore, the goal of the work is to first formalize the behavioral semantics of the middleware as a pre-requisite for our proof of the behavioral correctness. However, in this paper, we focus only on the core and critical component of the middleware, i.e. Execution Monitor which is a part of the module "Architectural Differencer" of AWDRAT. The role of the execution monitor is to identify inconsistencies between runtime observations of the target system and predictions of the specification System Architectural Model of the system. As a starting point we have defined the formal (denotational) semantics of the observations (runtime events) and predictions (executable specifications as of System Architectural Model); then based on the aforementioned formal semantices, we have formalized the behavior of the "Execution Monitor" of the middleware.