An Algebra for the Detection and Prediction of Malicious Activity in Concurrent Systems

The specification, verification, and validation of concurrent systems pose a number of challenges that are increasingly commonplace as multi-core and multi-processor systems are becoming ubiquitous. Any such system, particularly when actively exploiting concurrency, will experience variations up to non-determinism in some aspects of its behavior such as when awaiting I/O events or interacting with operation scheduling. We argue that this also makes it easier for adversaries - including both external exploits, logic bombs, or Trojan horses - to evade detection using conventional intrusion detection and prevention mechanisms. Novel attacks and subversion attempts cannot be reliably captured using specification-based approaches, whilst statistical and machine learning approaches are hampered by the inability to establish a clear baseline under the conditions described above. Therefore, we describe an algebra useful for specifying and identifying undesirable changes in state as linearizations of concurrent processes when supported by the ability to generate concurrent cross-view and cross-sectional observations of invariant behavior at semantically significant loci. This potential is enabled by the underlying concurrency assumption and the observation that malicious activity leading to subversion is generally non-atomic. The algebraic model is instantiated for the case of a multiprocessor host operating system and a sample subsystem.