Process mining and abstraction: formal methods for securing software and transactions

In this PhD thesis, new echniques based on Formal Methods are presented for security verification of systems. The mosti mportant ideas of this thesis use Process Mining as a bridge to connect Formal Methods with security verification of Business Processes. In particular, the thesis analyzes and proposes two new approaches. The first approach is proposed for Online Compliance Checking of inter-organizational high-throughput business processes, and it is based on a “silent” centralized system composed of a Validation Authority and special Software Agents installed in each involved entity, which send special observations to the Verification Authority and at the same time they take into account important privacy constraints which may be expressed by the involved organizations. The purpose is to create a merged event trace which can be analyzed for security verification using formal specification language, and a new important specification language is also presented. ThesecondapproachusesAbstractiontechniquesbasedonover-approximationandunderapproximation for Conformance Checking of incomplete log records in order to find security anomalies in terms of causal dependencies expressed in a specification. Moreover, Abstraction techniques has also been defined for Software Model Checking, still based on a combination of over-approximation and under-approximation techniques.