Formal methods in action: using runtime verification to automatically address occurrences of labor exploitation crimes

Nowadays, software systems are extremely complex: they often have to acquire a myriad of heterogeneous data in a fast and secure way and must ensure that they comply with all the regulations in force for the type of use made of the software itself and of the acquired data. Verifying the software exhaustively is an extremely time-consuming practice. For this reason, faster verification methods than traditional ones have been introduced over time. Among these is runtime verification analysis to verify individual execution paths of a system at runtime. This research aims to demonstrate that runtime verification method can also be used to automatically verify the occurrences of events monitored by the system and that this approach can be extremely useful for monitoring events attributable to crimes at runtime. In particular, we evaluated the proposal on a system that monitors labor exploitation in a region of the Netherlands. This choice is a direct consequence of the lack of systems suitable for monitoring such phenomena. Research has shown that runtime verification is not only an excellent - and commonly used in critical systems - method for verifying the robustness, safety and security of a system under test, but it is also extremely useful for verifying properties of the tracked behavior. In the aforementioned application context, this translates into the possibility of identifying the occurrence of abuses. Interesting data can emerge from the properties verified, such as the correlation of criminal events in certain situations, or the creation of statistics relating to cases of exploitation in a certain geographical region. The data obtained can be used to make strategic decisions in the context in which the system operates, so that the phenomenon of labor exploitation can be hopefully drastically reduced.

Al giorno d'oggi i sistemi software sono estremamente complessi: spesso devono acquisire una miriade di dati eterogenei in modo veloce e sicuro e devono garantire che siano conformi a tutte le normative vigenti per il tipo di utilizzo che si fa del software stesso e dei dati acquisiti. Verificare un software è una pratica estremamente dispendiosa in termini di tempo. Per questo motivo nel tempo sono stati introdotti metodi di verifica più rapidi rispetto a quelli tradizionali. Tra questi c'è l'analisi di verifica a runtime per verificare i singoli percorsi di esecuzione di un sistema in fase di esecuzione. Questa ricerca mira a dimostrare che il metodo di verifica a runtime può essere utilizzato anche per individuare automaticamente il verificarsi di eventi monitorati dal sistema e che questo approccio può essere estremamente utile per monitorare eventi riconducibili a reati a runtime. In particolare, abbiamo valutato la proposta su un sistema di monitoraggio dello sfruttamento lavorativo in una regione dei Paesi Bassi. Questa scelta è una diretta conseguenza della mancanza di sistemi idonei al monitoraggio di tali fenomeni. La ricerca ha dimostrato che la verifica a runtime non è solo un metodo eccellente - e comunemente utilizzato in sistemi critici - per verificare la robustezza, la safety e la sicurezza di un sistema sotto test, ma è anche estremamente utile per verificare le proprietà del comportamento tracciato. Nel contesto applicativo citato, ciò si traduce nella possibilità di individuare il verificarsi di abusi. Dalle proprietà verificate possono emergere dati interessanti, come la correlazione di eventi criminosi in determinate situazioni, o la creazione di statistiche relative a casi di sfruttamento in una determinata regione geografica. I dati ottenuti potranno essere utilizzati per prendere decisioni strategiche nel contesto in cui opera il sistema, affinché si possa ridurre drasticamente il fenomeno dello sfruttamento del lavoro.