A Rigorous and Efficient Run-time Secur...

We introduce a run-time security monitor for embedded system applications that detects both known and unknown computational cyber-attacks. Our security monitor is rigorous (i.e. sound and complete), eliminating false alarms, as well as efficient, supporting real-time detection. In contrast, conventional run-time security monitors for application software either produce (high rates of) false alarms (e.g. intrusion detection systems) or limit application performance (e.g. run-time verification systems). Such monitors are typically non-adaptive against constantly changing attacks of variable extent. Our run-time monitor detects attacks by checking the consistency between the application run-time behavior and its specified (expected) behavior model. Our specification language is based on monadic second order logic and event calculus interpreted over algebraic data structures; the application implementation can be in any programming language. Based on our defined denotational semantics of the specification language, we prove that the security monitor is sound and complete, i.e. it produces an alarm iff it detects an inconsistency between the application execution and the specified behavior. Importantly, the monitor detects not only cyber-attacks but all behavioral deviations from specification, e.g. bugs, and so, is readily applicable to the security of legacy systems. Through an application of our prototype monitor to a PID controller for a feedwater tank, we demonstrate that rigorous run-time monitors employing verification techniques are effective, efficient and readily applicable to demanding real-time critical systems, without scalability limitations.