In this PhD thesis, new echniques based on Formal Methods are presented for security veriﬁcation of systems. The mosti mportant ideas of this thesis use Process Mining as a bridge to connect Formal Methods with security veriﬁcation of Business Processes. In particular, the thesis analyzes and proposes two new approaches. The ﬁrst 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 Veriﬁcation 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 veriﬁcation using formal speciﬁcation language, and a new important speciﬁcation language is also presented. ThesecondapproachusesAbstractiontechniquesbasedonover-approximationandunderapproximation for Conformance Checking of incomplete log records in order to ﬁnd security anomalies in terms of causal dependencies expressed in a speciﬁcation. Moreover, Abstraction techniques has also been deﬁned for Software Model Checking, still based on a combination of over-approximation and under-approximation techniques.
|Titolo:||Process mining and abstraction: formal methods for securing software and transactions|
|Data di pubblicazione:||2013|
|Corso di dottorato:||Scienze dell'informazione|
|Settore Scientifico Disciplinare:||Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni|
|Tipologia:||Tesi di dottorato|
|Citazione:||(2013). Process mining and abstraction: formal methods for securing software and transactions.|
|Appare nelle tipologie:||07 - Tesi di dottorato|