Formal modeling and verification of security controls for multimedia systems in the cloud

Organizations deploy the Security Information and Event Management (SIEM) systems for centralized management of security alerts for securing their multimedia content. The SIEM system not only preserves events data, generated by devices and applications, in the form of logs but also performs real-time analysis of the event data. The SIEM works as the Security Operation Centre (SOC) in an organization, therefore, errors in the SIEM may compromise the security of the organization. In addition to focusing on the architecture, features, and the performance of the SIEM, it is imperative to carry out a formal analysis to verify that the system is impeccable. The ensuing research focuses mainly on the formal verification of the OSTORM a SIEM system. We have used High-Level Petri Nets (HLPN) and Z language to model and analyze the system. Moreover, Satisfiability Modulo Theories Library (SMT-Lib) and Z3 solver are used in this research to prove the correctness of the overall working of the OSTORM system. We demonstrate the correctness of the underlying system based on four security properties, namely: a) event data confidentiality, b) authentication, c) event data integrity, and d) alarm integrity. The results reveal that the OSTORM system functions correctly.